ax-ro-inst-1u - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > ax-ro-inst-1u

Axiom ax-ro-inst-1u 243

Description: {ro da} may be instantiated with any sumti.

**Hypotheses**
Ref	Expression
ax-ro-inst-1u.0	sumti ko'a
ax-ro-inst-1u.1	⊢ ro da zo'u da bo'a

**Assertion**
Ref	Expression
ax-ro-inst-1u	⊢ ko'a bo'a

This axiom is referenced by: (None)