Metamath Proof Explorer

Theorem 2uasbanhVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2uasbanh is 2uasbanhVD without virtual deductions and was automatically derived from 2uasbanhVD . (Contributed by Alan Sare, 31-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)

h1:: |- ( ch <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
100:1: |- ( ch -> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
2:100: |- (. ch ->. ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) ).
3:2: |- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ph ) ).
4:3: |- (. ch ->. E. x E. y ( x = u /\ y = v ) ).
5:4: |- (. ch ->. ( -. A. x x = y \/ u = v ) ).
6:5: |- (. ch ->. ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ).
7:3,6: |- (. ch ->. [ u / x ] [ v / y ] ph ).
8:2: |- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ps ) ).
9:5: |- (. ch ->. ( [ u / x ] [ v / y ] ps <-> E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) ).
10:8,9: |- (. ch ->. [ u / x ] [ v / y ] ps ).
101:: |- ( [ v / y ] ( ph /\ ps ) <-> ( [ v / y ] ph /\ [ v / y ] ps ) )
102:101: |- ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) )
103:: |- ( [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
104:102,103: |- ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
11:7,10,104: |- (. ch ->. [ u / x ] [ v / y ] ( ph /\ ps ) ).
110:5: |- (. ch ->. ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) ).
12:11,110: |- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ).
120:12: |- ( ch -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) )
13:1,120: |- ( ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) )
14:: |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ).
15:14: |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( x = u /\ y = v ) ).
16:14: |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ph /\ ps ) ).
17:16: |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ph ).
18:15,17: |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
19:18: |- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ph ) )
20:19: |- ( E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. y ( ( x = u /\ y = v ) /\ ph ) )
21:20: |- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
22:16: |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ps ).
23:15,22: |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ps ) ).
24:23: |- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ps ) )
25:24: |- ( E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. y ( ( x = u /\ y = v ) /\ ps ) )
26:25: |- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ps ) )
27:21,26: |- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
qed:13,27: |- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )

Ref Expression
Hypothesis 2uasbanhVD.1 
|- ( ch <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
Assertion 2uasbanhVD 
|- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 2uasbanhVD.1 
 |-  ( ch <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
2 idn1 
 |-  (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ).
3 simpl 
 |-  ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( x = u /\ y = v ) )
4 2 3 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( x = u /\ y = v ) ).
5 simpr 
 |-  ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ph /\ ps ) )
6 2 5 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ph /\ ps ) ).
7 simpl 
 |-  ( ( ph /\ ps ) -> ph )
8 6 7 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ph ).
9 pm3.2 
 |-  ( ( x = u /\ y = v ) -> ( ph -> ( ( x = u /\ y = v ) /\ ph ) ) )
10 4 8 9 e11 
 |-  (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
11 10 in1 
 |-  ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ph ) )
12 11 eximi 
 |-  ( E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. y ( ( x = u /\ y = v ) /\ ph ) )
13 12 eximi 
 |-  ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
14 simpr 
 |-  ( ( ph /\ ps ) -> ps )
15 6 14 e1a 
 |-  (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ps ).
16 pm3.2 
 |-  ( ( x = u /\ y = v ) -> ( ps -> ( ( x = u /\ y = v ) /\ ps ) ) )
17 4 15 16 e11 
 |-  (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ps ) ).
18 17 in1 
 |-  ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ps ) )
19 18 eximi 
 |-  ( E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. y ( ( x = u /\ y = v ) /\ ps ) )
20 19 eximi 
 |-  ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ps ) )
21 13 20 jca 
 |-  ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
22 1 biimpi 
 |-  ( ch -> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
23 22 dfvd1ir 
 |-  (. ch ->. ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) ).
24 simpl 
 |-  ( ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
25 23 24 e1a 
 |-  (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ph ) ).
26 simpl 
 |-  ( ( ( x = u /\ y = v ) /\ ph ) -> ( x = u /\ y = v ) )
27 26 2eximi 
 |-  ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) -> E. x E. y ( x = u /\ y = v ) )
28 25 27 e1a 
 |-  (. ch ->. E. x E. y ( x = u /\ y = v ) ).
29 ax6e2ndeq 
 |-  ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
30 29 biimpri 
 |-  ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) )
31 28 30 e1a 
 |-  (. ch ->. ( -. A. x x = y \/ u = v ) ).
32 2sb5nd 
 |-  ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
33 31 32 e1a 
 |-  (. ch ->. ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ).
34 biimpr 
 |-  ( ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) -> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) -> [ u / x ] [ v / y ] ph ) )
35 34 com12 
 |-  ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) -> ( ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) -> [ u / x ] [ v / y ] ph ) )
36 25 33 35 e11 
 |-  (. ch ->. [ u / x ] [ v / y ] ph ).
37 simpr 
 |-  ( ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ps ) )
38 23 37 e1a 
 |-  (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ps ) ).
39 2sb5nd 
 |-  ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ps <-> E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
40 31 39 e1a 
 |-  (. ch ->. ( [ u / x ] [ v / y ] ps <-> E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) ).
41 biimpr 
 |-  ( ( [ u / x ] [ v / y ] ps <-> E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) -> ( E. x E. y ( ( x = u /\ y = v ) /\ ps ) -> [ u / x ] [ v / y ] ps ) )
42 41 com12 
 |-  ( E. x E. y ( ( x = u /\ y = v ) /\ ps ) -> ( ( [ u / x ] [ v / y ] ps <-> E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) -> [ u / x ] [ v / y ] ps ) )
43 38 40 42 e11 
 |-  (. ch ->. [ u / x ] [ v / y ] ps ).
44 sban 
 |-  ( [ v / y ] ( ph /\ ps ) <-> ( [ v / y ] ph /\ [ v / y ] ps ) )
45 44 sbbii 
 |-  ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) )
46 sban 
 |-  ( [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
47 45 46 bitri 
 |-  ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
48 simplbi2comt 
 |-  ( ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) ) -> ( [ u / x ] [ v / y ] ps -> ( [ u / x ] [ v / y ] ph -> [ u / x ] [ v / y ] ( ph /\ ps ) ) ) )
49 48 com13 
 |-  ( [ u / x ] [ v / y ] ph -> ( [ u / x ] [ v / y ] ps -> ( ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) ) -> [ u / x ] [ v / y ] ( ph /\ ps ) ) ) )
50 36 43 47 49 e110 
 |-  (. ch ->. [ u / x ] [ v / y ] ( ph /\ ps ) ).
51 2sb5nd 
 |-  ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) )
52 31 51 e1a 
 |-  (. ch ->. ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) ).
53 biimp 
 |-  ( ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) -> ( [ u / x ] [ v / y ] ( ph /\ ps ) -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) )
54 53 com12 
 |-  ( [ u / x ] [ v / y ] ( ph /\ ps ) -> ( ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) )
55 50 52 54 e11 
 |-  (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ).
56 55 in1 
 |-  ( ch -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) )
57 1 56 sylbir 
 |-  ( ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) )
58 21 57 impbii 
 |-  ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )