ax-ge-le - brismu bridi

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

Axiom ax-ge-le 34

Description: Elimination of {ge} on the left. Curry of the left-hand projection. Axiom ax-ia1 in [ILE] p. 0.

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

This axiom is referenced by: ge-lei 37 ge-led 38 cur 44 ge-idem 113 subeq-lem2 354 mapti-ckini 581