ax-qi1 - brismu bridi

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

Axiom ax-qi1 185

Description: Axiom of quantified implication: if {ganai broda gi brode} under some universal quantifier, then the universal quantification of {broda} implies the universal quantification of {brode}. Relationally, the tuples of the consequent might not have the same data as the tuples of the antecedent; we only know that they exist, not that they are related. Axiom ax-5 in [ILE] p. 0.

**Assertion**
Ref	Expression
ax-qi1	⊢ ganai ro da zo'u ganai broda gi brode gi ganai ro da zo'u broda gi ro da zo'u brode

This axiom is referenced by: qi1i 186

W3C validator