theorem rexcomb {x y: nat} (p: wff x) (q: wff y) (a: wff x y): $ E. x (p /\ E. y (q /\ a)) <-> E. y (q /\ E. x (p /\ a)) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
2 |
E. x (p /\ E. y (q /\ a)) <-> E. y E. x (p /\ (q /\ a)) |
||
5 |
p /\ (q /\ a) <-> q /\ (p /\ a) |
||
6 |
E. x (p /\ (q /\ a)) <-> E. x (q /\ (p /\ a)) |
||
8 |
E. x (q /\ (p /\ a)) <-> q /\ E. x (p /\ a) |
||
9 |
bitr* |
E. x (p /\ (q /\ a)) <-> q /\ E. x (p /\ a) |
|
10 |
E. y E. x (p /\ (q /\ a)) <-> E. y (q /\ E. x (p /\ a)) |
||
11 |
bitr* |
E. x (p /\ E. y (q /\ a)) <-> E. y (q /\ E. x (p /\ a)) |