Theorem excomb ≪ | index | src | ≫ 

theorem excomb {x y: nat} (a: wff x y): $ E. x E. y a <-> E. y E. x a $;
StepHypRefExpression
1 noteq 
(A. x ~E. y a <-> A. y ~E. x a) -> (~A. x ~E. y a <-> ~A. y ~E. x a)
2 1 conv ex 
(A. x ~E. y a <-> A. y ~E. x a) -> (E. x E. y a <-> E. y E. x a)
3 bitr3 
(A. x A. y ~a <-> A. x ~E. y a) -> (A. x A. y ~a <-> A. y ~E. x a) -> (A. x ~E. y a <-> A. y ~E. x a)
4 alnex 
A. y ~a <-> ~E. y a
5 4 aleqi 
A. x A. y ~a <-> A. x ~E. y a
6 3, 5 ax_mp 
(A. x A. y ~a <-> A. y ~E. x a) -> (A. x ~E. y a <-> A. y ~E. x a)
7 bitr 
(A. x A. y ~a <-> A. y A. x ~a) -> (A. y A. x ~a <-> A. y ~E. x a) -> (A. x A. y ~a <-> A. y ~E. x a)
8 alcomb 
A. x A. y ~a <-> A. y A. x ~a
9 7, 8 ax_mp 
(A. y A. x ~a <-> A. y ~E. x a) -> (A. x A. y ~a <-> A. y ~E. x a)
10 alnex 
A. x ~a <-> ~E. x a
11 10 aleqi 
A. y A. x ~a <-> A. y ~E. x a
12 9, 11 ax_mp 
A. x A. y ~a <-> A. y ~E. x a
13 6, 12 ax_mp 
A. x ~E. y a <-> A. y ~E. x a
14 2, 13 ax_mp 
E. x E. y a <-> E. y E. x a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_11)