Theorem 2uasbanh 38777

Description: Distribute the unabbreviated form of proper substitution in and out of a conjunction. 2uasbanh 38777 is derived from 2uasbanhVD 39147. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

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

Assertion

Ref	Expression
2uasbanh	|- ( 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 2uasbanh

Step	Hyp	Ref	Expression
1		simpl 473	. . . . 5 |- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( x = u /\ y = v ) )
2		simprl 794	. . . . 5 |- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ph )
3	1, 2	jca 554	. . . 4 |- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ph ) )
4	3	2eximi 1763	. . 3 |- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
5		simprr 796	. . . . 5 |- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ps )
6	1, 5	jca 554	. . . 4 |- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ps ) )
7	6	2eximi 1763	. . 3 |- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ps ) )
8	4, 7	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 ) ) )
9		2uasbanh.1	. . 3 |- ( ch <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
10	9	simplbi 476	. . . . . 6 |- ( ch -> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
11		simpl 473	. . . . . . . . . 10 |- ( ( ( x = u /\ y = v ) /\ ph ) -> ( x = u /\ y = v ) )
12	11	2eximi 1763	. . . . . . . . 9 |- ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) -> E. x E. y ( x = u /\ y = v ) )
13	10, 12	syl 17	. . . . . . . 8 |- ( ch -> E. x E. y ( x = u /\ y = v ) )
14		ax6e2ndeq 38775	. . . . . . . 8 |- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )
15	13, 14	sylibr 224	. . . . . . 7 |- ( ch -> ( -. A. x x = y \/ u = v ) )
16		2sb5nd 38776	. . . . . . 7 |- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
17	15, 16	syl 17	. . . . . 6 |- ( ch -> ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) )
18	10, 17	mpbird 247	. . . . 5 |- ( ch -> [ u / x ] [ v / y ] ph )
19	9	simprbi 480	. . . . . 6 |- ( ch -> E. x E. y ( ( x = u /\ y = v ) /\ ps ) )
20		2sb5nd 38776	. . . . . . 7 |- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ps <-> E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
21	15, 20	syl 17	. . . . . 6 |- ( ch -> ( [ u / x ] [ v / y ] ps <-> E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
22	19, 21	mpbird 247	. . . . 5 |- ( ch -> [ u / x ] [ v / y ] ps )
23		sban 2399	. . . . . . 7 |- ( [ v / y ] ( ph /\ ps ) <-> ( [ v / y ] ph /\ [ v / y ] ps ) )
24	23	sbbii 1887	. . . . . 6 |- ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) )
25		sban 2399	. . . . . 6 |- ( [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
26	24, 25	bitri 264	. . . . 5 |- ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
27	18, 22, 26	sylanbrc 698	. . . 4 |- ( ch -> [ u / x ] [ v / y ] ( ph /\ ps ) )
28		2sb5nd 38776	. . . . 5 |- ( ( -. A. x x = y \/ u = v ) -> ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) )
29	15, 28	syl 17	. . . 4 |- ( ch -> ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) )
30	27, 29	mpbid 222	. . 3 |- ( ch -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) )
31	9, 30	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 ) ) )
32	8, 31	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   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

This theorem is referenced by:  2uasban  38778