Theorem pimtr ≪ | index | src | ≫ 

theorem pimtr {x y: nat} (p: wff x) (q a: wff x y) (b: wff y):
  $ (P. x p -> a) -> A. x (a -> (P. y q -> b)) -> (P. y E. x (p /\ q) -> b) $;
StepHypRefExpression
1 excom 
E. x E. y (p /\ q) -> E. y E. x (p /\ q)
2 pimex12 
(P. x p -> a) -> E. x (p /\ a)
3 exim 
A. x (p /\ a -> E. y (p /\ q)) -> E. x (p /\ a) -> E. x E. y (p /\ q)
4 anl 
E. y q /\ A. y (q -> b) -> E. y q
5 4 conv pim 
(P. y q -> b) -> E. y q
6 ian 
p -> q -> p /\ q
7 6 eximd 
p -> E. y q -> E. y (p /\ q)
8 5, 7 syl5 
p -> (P. y q -> b) -> E. y (p /\ q)
9 8 imim2d 
p -> (a -> (P. y q -> b)) -> a -> E. y (p /\ q)
10 9 com12 
(a -> (P. y q -> b)) -> p -> a -> E. y (p /\ q)
11 10 impd 
(a -> (P. y q -> b)) -> p /\ a -> E. y (p /\ q)
12 11 alimi 
A. x (a -> (P. y q -> b)) -> A. x (p /\ a -> E. y (p /\ q))
13 3, 12 syl 
A. x (a -> (P. y q -> b)) -> E. x (p /\ a) -> E. x E. y (p /\ q)
14 2, 13 syl5 
A. x (a -> (P. y q -> b)) -> (P. x p -> a) -> E. x E. y (p /\ q)
15 14 impcom 
(P. x p -> a) /\ A. x (a -> (P. y q -> b)) -> E. x E. y (p /\ q)
16 1, 15 syl 
(P. x p -> a) /\ A. x (a -> (P. y q -> b)) -> E. y E. x (p /\ q)
17 anim 
((P. x p -> a) -> A. x (p -> a)) ->
  (A. x (a -> (P. y q -> b)) -> A. x (a -> A. y (q -> b))) ->
  (P. x p -> a) /\ A. x (a -> (P. y q -> b)) ->
  A. x (p -> a) /\ A. x (a -> A. y (q -> b))
18 anr 
E. x p /\ A. x (p -> a) -> A. x (p -> a)
19 18 conv pim 
(P. x p -> a) -> A. x (p -> a)
20 17, 19 ax_mp 
(A. x (a -> (P. y q -> b)) -> A. x (a -> A. y (q -> b))) -> (P. x p -> a) /\ A. x (a -> (P. y q -> b)) -> A. x (p -> a) /\ A. x (a -> A. y (q -> b))
21 anr 
E. y q /\ A. y (q -> b) -> A. y (q -> b)
22 21 conv pim 
(P. y q -> b) -> A. y (q -> b)
23 22 imim2i 
(a -> (P. y q -> b)) -> a -> A. y (q -> b)
24 23 alimi 
A. x (a -> (P. y q -> b)) -> A. x (a -> A. y (q -> b))
25 20, 24 ax_mp 
(P. x p -> a) /\ A. x (a -> (P. y q -> b)) -> A. x (p -> a) /\ A. x (a -> A. y (q -> b))
26 bitr 
(E. x (p /\ q) -> b <-> A. x (p /\ q -> b)) -> (A. x (p /\ q -> b) <-> A. x (p -> q -> b)) -> (E. x (p /\ q) -> b <-> A. x (p -> q -> b))
27 eexb 
E. x (p /\ q) -> b <-> A. x (p /\ q -> b)
28 26, 27 ax_mp 
(A. x (p /\ q -> b) <-> A. x (p -> q -> b)) -> (E. x (p /\ q) -> b <-> A. x (p -> q -> b))
29 impexp 
p /\ q -> b <-> p -> q -> b
30 29 aleqi 
A. x (p /\ q -> b) <-> A. x (p -> q -> b)
31 28, 30 ax_mp 
E. x (p /\ q) -> b <-> A. x (p -> q -> b)
32 31 aleqi 
A. y (E. x (p /\ q) -> b) <-> A. y A. x (p -> q -> b)
33 ralalcomb 
A. x (p -> A. y (q -> b)) <-> A. y A. x (p -> q -> b)
34 imim2 
(a -> A. y (q -> b)) -> (p -> a) -> p -> A. y (q -> b)
35 34 com12 
(p -> a) -> (a -> A. y (q -> b)) -> p -> A. y (q -> b)
36 35 al2imi 
A. x (p -> a) -> A. x (a -> A. y (q -> b)) -> A. x (p -> A. y (q -> b))
37 36 imp 
A. x (p -> a) /\ A. x (a -> A. y (q -> b)) -> A. x (p -> A. y (q -> b))
38 33, 37 sylib 
A. x (p -> a) /\ A. x (a -> A. y (q -> b)) -> A. y A. x (p -> q -> b)
39 32, 38 sylibr 
A. x (p -> a) /\ A. x (a -> A. y (q -> b)) -> A. y (E. x (p /\ q) -> b)
40 25, 39 rsyl 
(P. x p -> a) /\ A. x (a -> (P. y q -> b)) -> A. y (E. x (p /\ q) -> b)
41 16, 40 iand 
(P. x p -> a) /\ A. x (a -> (P. y q -> b)) -> E. y E. x (p /\ q) /\ A. y (E. x (p /\ q) -> b)
42 41 conv pim 
(P. x p -> a) /\ A. x (a -> (P. y q -> b)) -> (P. y E. x (p /\ q) -> b)
43 42 exp 
(P. x p -> a) -> A. x (a -> (P. y q -> b)) -> (P. y E. x (p /\ q) -> b)

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)