Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
Axiom scheme ax-11 (Quantifier Commutation)
exrot3
Next ⟩
exrot4
Metamath Proof Explorer
Ascii
Unicode
Theorem
exrot3
Description:
Rotate existential quantifiers.
(Contributed by
NM
, 17-Mar-1995)
Ref
Expression
Assertion
exrot3
⊢
∃
x
∃
y
∃
z
φ
↔
∃
y
∃
z
∃
x
φ
Proof
Step
Hyp
Ref
Expression
1
excom13
⊢
∃
x
∃
y
∃
z
φ
↔
∃
z
∃
y
∃
x
φ
2
excom
⊢
∃
z
∃
y
∃
x
φ
↔
∃
y
∃
z
∃
x
φ
3
1
2
bitri
⊢
∃
x
∃
y
∃
z
φ
↔
∃
y
∃
z
∃
x
φ