Theorem 2uasbanhVD 39147

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 38785) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2uasbanh 38777 is 2uasbanhVD 39147 without virtual deductions and was automatically derived from 2uasbanhVD 39147. (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 ) ) )

Hypothesis

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

Assertion

Ref	Expression
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 ) ) )

Distinct variable groups:   x, u   y, u   x, v   y, v

Allowed substitution hints:   ph( x, y, v, u)   ps( x, y, v, u)   ch( x, y, v, u)

Proof of Theorem 2uasbanhVD

Step	Hyp	Ref	Expression
1		idn1 38790	. . . . . . . 8 |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ).
2		simpl 473	. . . . . . . 8 |- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( x = u /\ y = v ) )
3	1, 2	e1a 38852	. . . . . . 7 |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( x = u /\ y = v ) ).
4		simpr 477	. . . . . . . . 9 |- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ph /\ ps ) )
5	1, 4	e1a 38852	. . . . . . . 8 |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ph /\ ps ) ).
6		simpl 473	. . . . . . . 8 |- ( ( ph /\ ps ) -> ph )
7	5, 6	e1a 38852	. . . . . . 7 |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ph ).
8		pm3.2 463	. . . . . . 7 |- ( ( x = u /\ y = v ) -> ( ph -> ( ( x = u /\ y = v ) /\ ph ) ) )
9	3, 7, 8	e11 38913	. . . . . 6 |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
10	9	in1 38787	. . . . 5 |- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ph ) )
11	10	eximi 1762	. . . 4 |- ( E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. y ( ( x = u /\ y = v ) /\ ph ) )
12	11	eximi 1762	. . 3 |- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
13		simpr 477	. . . . . . . 8 |- ( ( ph /\ ps ) -> ps )
14	5, 13	e1a 38852	. . . . . . 7 |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ps ).
15		pm3.2 463	. . . . . . 7 |- ( ( x = u /\ y = v ) -> ( ps -> ( ( x = u /\ y = v ) /\ ps ) ) )
16	3, 14, 15	e11 38913	. . . . . 6 |- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ps ) ).
17	16	in1 38787	. . . . 5 |- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ps ) )
18	17	eximi 1762	. . . 4 |- ( E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. y ( ( x = u /\ y = v ) /\ ps ) )
19	18	eximi 1762	. . 3 |- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ps ) )
20	12, 19	jca 554	. 2 |- ( 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 ) ) )
21		2uasbanhVD.1	. . 3 |- ( ch <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
22	21	biimpi 206	. . . . . . . . 9 |- ( ch -> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
23	22	dfvd1ir 38789	. . . . . . . 8 |- (. ch ->. ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) ).
24		simpl 473	. . . . . . . 8 |- ( ( 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 38852	. . . . . . 7 |- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ph ) ).
26		simpl 473	. . . . . . . . . . 11 |- ( ( ( x = u /\ y = v ) /\ ph ) -> ( x = u /\ y = v ) )
27	26	2eximi 1763	. . . . . . . . . 10 |- ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) -> E. x E. y ( x = u /\ y = v ) )
28	25, 27	e1a 38852	. . . . . . . . 9 |- (. ch ->. E. x E. y ( x = u /\ y = v ) ).
29		ax6e2ndeq 38775	. . . . . . . . . 10 |- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
30	29	biimpri 218	. . . . . . . . 9 |- ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) )
31	28, 30	e1a 38852	. . . . . . . 8 |- (. ch ->. ( -. A. x x = y \/ u = v ) ).
32		2sb5nd 38776	. . . . . . . 8 |- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
33	31, 32	e1a 38852	. . . . . . 7 |- (. ch ->. ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ).
34		biimpr 210	. . . . . . . 8 |- ( ( [ 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 32	. . . . . . 7 |- ( 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 38913	. . . . . 6 |- (. ch ->. [ u / x ] [ v / y ] ph ).
37		simpr 477	. . . . . . . 8 |- ( ( 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 38852	. . . . . . 7 |- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ps ) ).
39		2sb5nd 38776	. . . . . . . 8 |- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ps <-> E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
40	31, 39	e1a 38852	. . . . . . 7 |- (. ch ->. ( [ u / x ] [ v / y ] ps <-> E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) ).
41		biimpr 210	. . . . . . . 8 |- ( ( [ 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 32	. . . . . . 7 |- ( 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 38913	. . . . . 6 |- (. ch ->. [ u / x ] [ v / y ] ps ).
44		sban 2399	. . . . . . . 8 |- ( [ v / y ] ( ph /\ ps ) <-> ( [ v / y ] ph /\ [ v / y ] ps ) )
45	44	sbbii 1887	. . . . . . 7 |- ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) )
46		sban 2399	. . . . . . 7 |- ( [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
47	45, 46	bitri 264	. . . . . 6 |- ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
48		simplbi2comt 656	. . . . . . 7 |- ( ( [ 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 88	. . . . . 6 |- ( [ 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 38901	. . . . 5 |- (. ch ->. [ u / x ] [ v / y ] ( ph /\ ps ) ).
51		2sb5nd 38776	. . . . . 6 |- ( ( -. 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 38852	. . . . 5 |- (. ch ->. ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) ).
53		biimp 205	. . . . . 6 |- ( ( [ 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 32	. . . . 5 |- ( [ 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 38913	. . . 4 |- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ).
56	55	in1 38787	. . 3 |- ( ch -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) )
57	21, 56	sylbir 225	. 2 |- ( ( 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	20, 57	impbii 199	1 |- ( 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 ) ) )

Syntax hints:   -. wn 3   <-> wb 196   \/ wo 383   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   [wsb 1880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ne 2795  df-v 3202  df-vd1 38786

This theorem is referenced by: (None)