ax-ge-in - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > ax-ge-in

Axiom ax-ge-in 36

Description: Introduction of {ge}. Curry of the I combinator. Axiom ax-ia3 in [ILE] p. 0.

**Assertion**
Ref	Expression
ax-ge-in	⊢ ganai broda gi ganai brode gi ge broda gi brode

This axiom is referenced by: ge-ini 41 ge-in-swap12 43 uncur 45 jca 46 ge-diag 112