Theorem pimexeqed ≪ | index | src | ≫ 

theorem pimexeqed (G: wff) {x y: nat} (a: nat) (p: wff x y) (q: wff x)
  (p2 q2: wff y):
  $ G /\ x = a -> (p <-> p2) $ >
  $ G /\ x = a -> (q <-> q2) $ >
  $ G -> ((P. x E. y (x = a /\ p) -> q) <-> (P. y p2 -> q2)) $;
StepHypRefExpression
1 excomb 
E. x E. y (x = a /\ p) <-> E. y E. x (x = a /\ p)
2 hyp e1 
G /\ x = a -> (p <-> p2)
3 2 exeqed 
G -> (E. x (x = a /\ p) <-> p2)
4 3 exeqd 
G -> (E. y E. x (x = a /\ p) <-> E. y p2)
5 1, 4 syl5bb 
G -> (E. x E. y (x = a /\ p) <-> E. y p2)
6 eexb 
E. y (x = a /\ p) -> q <-> A. y (x = a /\ p -> q)
7 6 aleqi 
A. x (E. y (x = a /\ p) -> q) <-> A. x A. y (x = a /\ p -> q)
8 alcomb 
A. x A. y (x = a /\ p -> q) <-> A. y A. x (x = a /\ p -> q)
9 impexp 
x = a /\ p -> q <-> x = a -> p -> q
10 9 aleqi 
A. x (x = a /\ p -> q) <-> A. x (x = a -> p -> q)
11 hyp e2 
G /\ x = a -> (q <-> q2)
12 2, 11 imeqd 
G /\ x = a -> (p -> q <-> p2 -> q2)
13 12 aleqed 
G -> (A. x (x = a -> p -> q) <-> p2 -> q2)
14 10, 13 syl5bb 
G -> (A. x (x = a /\ p -> q) <-> p2 -> q2)
15 14 aleqd 
G -> (A. y A. x (x = a /\ p -> q) <-> A. y (p2 -> q2))
16 8, 15 syl5bb 
G -> (A. x A. y (x = a /\ p -> q) <-> A. y (p2 -> q2))
17 7, 16 syl5bb 
G -> (A. x (E. y (x = a /\ p) -> q) <-> A. y (p2 -> q2))
18 5, 17 aneqd 
G -> (E. x E. y (x = a /\ p) /\ A. x (E. y (x = a /\ p) -> q) <-> E. y p2 /\ A. y (p2 -> q2))
19 18 conv pim 
G -> ((P. x E. y (x = a /\ p) -> q) <-> (P. y p2 -> q2))

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12)