ax-ro1-com - brismu bridi

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

Axiom ax-ro1-com 247

Description: First-order universal quantifiers commute.

**Assertion**
Ref	Expression
ax-ro1-com	⊢ ganai ro da zo'u ro de zo'u broda gi ro de zo'u ro da zo'u broda

Distinct variable group: da , de

This axiom is referenced by: ro1-coms 248