ax-ro-int - brismu bridi

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

Axiom ax-ro-int 229

Description: First-order universal quantifier introduction with a scope gadget.

**Assertion**
Ref	Expression
ax-ro-int	⊢ ga ro di zo'u di du da gi ga ro di zo'u di du de gi ro di zo'u ganai da du de gi ro di zo'u da du de

Distinct variable group: da ,de ,di

This axiom is referenced by: (None)