ax-ge-in - brismu bridi

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

Axiom ax-ge-in 50

Description: Introduction of {ge}. Curry of the I combinator.

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

This axiom is referenced by: ge-ini 55 ancl 56 ge-in-swap12 58 uncur 61 ge-prod 69 ge-diag 144 foml19.29 429