Metamath Proof Explorer

Theorem pm11.71

Description: Theorem *11.71 in WhiteheadRussell p. 166. (Contributed by Andrew Salmon, 24-May-2011)

Ref Expression
Assertion pm11.71 
|- ( ( E. x ph /\ E. y ch ) -> ( ( A. x ( ph -> ps ) /\ A. y ( ch -> th ) ) <-> A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ y ( ph -> ps )
2 nfv 
 |-  F/ x ( ch -> th )
3 1 2 aaan 
 |-  ( A. x A. y ( ( ph -> ps ) /\ ( ch -> th ) ) <-> ( A. x ( ph -> ps ) /\ A. y ( ch -> th ) ) )
4 anim12 
 |-  ( ( ( ph -> ps ) /\ ( ch -> th ) ) -> ( ( ph /\ ch ) -> ( ps /\ th ) ) )
5 4 2alimi 
 |-  ( A. x A. y ( ( ph -> ps ) /\ ( ch -> th ) ) -> A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) )
6 3 5 sylbir 
 |-  ( ( A. x ( ph -> ps ) /\ A. y ( ch -> th ) ) -> A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) )
7 nfv 
 |-  F/ x ch
8 7 nfex 
 |-  F/ x E. y ch
9 exim 
 |-  ( A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( E. y ( ph /\ ch ) -> E. y ( ps /\ th ) ) )
10 19.42v 
 |-  ( E. y ( ph /\ ch ) <-> ( ph /\ E. y ch ) )
11 19.42v 
 |-  ( E. y ( ps /\ th ) <-> ( ps /\ E. y th ) )
12 9 10 11 3imtr3g 
 |-  ( A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( ( ph /\ E. y ch ) -> ( ps /\ E. y th ) ) )
13 pm3.21 
 |-  ( E. y ch -> ( ph -> ( ph /\ E. y ch ) ) )
14 simpl 
 |-  ( ( ps /\ E. y th ) -> ps )
15 14 imim2i 
 |-  ( ( ( ph /\ E. y ch ) -> ( ps /\ E. y th ) ) -> ( ( ph /\ E. y ch ) -> ps ) )
16 13 15 syl9 
 |-  ( E. y ch -> ( ( ( ph /\ E. y ch ) -> ( ps /\ E. y th ) ) -> ( ph -> ps ) ) )
17 12 16 syl5 
 |-  ( E. y ch -> ( A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( ph -> ps ) ) )
18 8 17 alimd 
 |-  ( E. y ch -> ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. x ( ph -> ps ) ) )
19 18 adantl 
 |-  ( ( E. x ph /\ E. y ch ) -> ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. x ( ph -> ps ) ) )
20 ax-11 
 |-  ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. y A. x ( ( ph /\ ch ) -> ( ps /\ th ) ) )
21 nfv 
 |-  F/ y ph
22 21 nfex 
 |-  F/ y E. x ph
23 exim 
 |-  ( A. x ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( E. x ( ph /\ ch ) -> E. x ( ps /\ th ) ) )
24 19.41v 
 |-  ( E. x ( ph /\ ch ) <-> ( E. x ph /\ ch ) )
25 19.41v 
 |-  ( E. x ( ps /\ th ) <-> ( E. x ps /\ th ) )
26 23 24 25 3imtr3g 
 |-  ( A. x ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( ( E. x ph /\ ch ) -> ( E. x ps /\ th ) ) )
27 pm3.2 
 |-  ( E. x ph -> ( ch -> ( E. x ph /\ ch ) ) )
28 simpr 
 |-  ( ( E. x ps /\ th ) -> th )
29 28 imim2i 
 |-  ( ( ( E. x ph /\ ch ) -> ( E. x ps /\ th ) ) -> ( ( E. x ph /\ ch ) -> th ) )
30 27 29 syl9 
 |-  ( E. x ph -> ( ( ( E. x ph /\ ch ) -> ( E. x ps /\ th ) ) -> ( ch -> th ) ) )
31 26 30 syl5 
 |-  ( E. x ph -> ( A. x ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( ch -> th ) ) )
32 22 31 alimd 
 |-  ( E. x ph -> ( A. y A. x ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. y ( ch -> th ) ) )
33 20 32 syl5 
 |-  ( E. x ph -> ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. y ( ch -> th ) ) )
34 33 adantr 
 |-  ( ( E. x ph /\ E. y ch ) -> ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> A. y ( ch -> th ) ) )
35 19 34 jcad 
 |-  ( ( E. x ph /\ E. y ch ) -> ( A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) -> ( A. x ( ph -> ps ) /\ A. y ( ch -> th ) ) ) )
36 6 35 impbid2 
 |-  ( ( E. x ph /\ E. y ch ) -> ( ( A. x ( ph -> ps ) /\ A. y ( ch -> th ) ) <-> A. x A. y ( ( ph /\ ch ) -> ( ps /\ th ) ) ) )