ax-ge-re - brismu bridi

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

Axiom ax-ge-re 35

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

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

This axiom is referenced by: ge-rei 39 ge-red 40 ge-ganai 42 cur 44