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

Axiom ax-ro1-sub 228
Description: First-order quantifier substitution.
Assertion
Ref Expression
ax-ro1-subganai ro da zo'u da du de gi ro de zo'u de du da
Distinct variable group:   da ,de

This axiom is referenced by: (None)
  Copyright terms: Public domain W3C validator