This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ceqsex4v

Description: Elimination of four existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011)

Ref Expression
Hypotheses ceqsex4v.1 
|- A e. _V
ceqsex4v.2 
|- B e. _V
ceqsex4v.3 
|- C e. _V
ceqsex4v.4 
|- D e. _V
ceqsex4v.7 
|- ( x = A -> ( ph <-> ps ) )
ceqsex4v.8 
|- ( y = B -> ( ps <-> ch ) )
ceqsex4v.9 
|- ( z = C -> ( ch <-> th ) )
ceqsex4v.10 
|- ( w = D -> ( th <-> ta ) )
Assertion ceqsex4v 
|- ( E. x E. y E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ ph ) <-> ta )

Proof

Step Hyp Ref Expression
1 ceqsex4v.1 
 |-  A e. _V
2 ceqsex4v.2 
 |-  B e. _V
3 ceqsex4v.3 
 |-  C e. _V
4 ceqsex4v.4 
 |-  D e. _V
5 ceqsex4v.7 
 |-  ( x = A -> ( ph <-> ps ) )
6 ceqsex4v.8 
 |-  ( y = B -> ( ps <-> ch ) )
7 ceqsex4v.9 
 |-  ( z = C -> ( ch <-> th ) )
8 ceqsex4v.10 
 |-  ( w = D -> ( th <-> ta ) )
9 19.42vv 
 |-  ( E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D /\ ph ) ) <-> ( ( x = A /\ y = B ) /\ E. z E. w ( z = C /\ w = D /\ ph ) ) )
10 3anass 
 |-  ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ ph ) <-> ( ( x = A /\ y = B ) /\ ( ( z = C /\ w = D ) /\ ph ) ) )
11 df-3an 
 |-  ( ( z = C /\ w = D /\ ph ) <-> ( ( z = C /\ w = D ) /\ ph ) )
12 11 anbi2i 
 |-  ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D /\ ph ) ) <-> ( ( x = A /\ y = B ) /\ ( ( z = C /\ w = D ) /\ ph ) ) )
13 10 12 bitr4i 
 |-  ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ ph ) <-> ( ( x = A /\ y = B ) /\ ( z = C /\ w = D /\ ph ) ) )
14 13 2exbii 
 |-  ( E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ ph ) <-> E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D /\ ph ) ) )
15 df-3an 
 |-  ( ( x = A /\ y = B /\ E. z E. w ( z = C /\ w = D /\ ph ) ) <-> ( ( x = A /\ y = B ) /\ E. z E. w ( z = C /\ w = D /\ ph ) ) )
16 9 14 15 3bitr4i 
 |-  ( E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ ph ) <-> ( x = A /\ y = B /\ E. z E. w ( z = C /\ w = D /\ ph ) ) )
17 16 2exbii 
 |-  ( E. x E. y E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ ph ) <-> E. x E. y ( x = A /\ y = B /\ E. z E. w ( z = C /\ w = D /\ ph ) ) )
18 5 3anbi3d 
 |-  ( x = A -> ( ( z = C /\ w = D /\ ph ) <-> ( z = C /\ w = D /\ ps ) ) )
19 18 2exbidv 
 |-  ( x = A -> ( E. z E. w ( z = C /\ w = D /\ ph ) <-> E. z E. w ( z = C /\ w = D /\ ps ) ) )
20 6 3anbi3d 
 |-  ( y = B -> ( ( z = C /\ w = D /\ ps ) <-> ( z = C /\ w = D /\ ch ) ) )
21 20 2exbidv 
 |-  ( y = B -> ( E. z E. w ( z = C /\ w = D /\ ps ) <-> E. z E. w ( z = C /\ w = D /\ ch ) ) )
22 1 2 19 21 ceqsex2v 
 |-  ( E. x E. y ( x = A /\ y = B /\ E. z E. w ( z = C /\ w = D /\ ph ) ) <-> E. z E. w ( z = C /\ w = D /\ ch ) )
23 3 4 7 8 ceqsex2v 
 |-  ( E. z E. w ( z = C /\ w = D /\ ch ) <-> ta )
24 17 22 23 3bitri 
 |-  ( E. x E. y E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ ph ) <-> ta )