Metamath Proof Explorer

Theorem 2uasbanh

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

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

Proof

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