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

Metamath Proof Explorer

Theorem ceqsex8v

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

Ref Expression
Hypotheses ceqsex8v.1 
|- A e. _V
ceqsex8v.2 
|- B e. _V
ceqsex8v.3 
|- C e. _V
ceqsex8v.4 
|- D e. _V
ceqsex8v.5 
|- E e. _V
ceqsex8v.6 
|- F e. _V
ceqsex8v.7 
|- G e. _V
ceqsex8v.8 
|- H e. _V
ceqsex8v.9 
|- ( x = A -> ( ph <-> ps ) )
ceqsex8v.10 
|- ( y = B -> ( ps <-> ch ) )
ceqsex8v.11 
|- ( z = C -> ( ch <-> th ) )
ceqsex8v.12 
|- ( w = D -> ( th <-> ta ) )
ceqsex8v.13 
|- ( v = E -> ( ta <-> et ) )
ceqsex8v.14 
|- ( u = F -> ( et <-> ze ) )
ceqsex8v.15 
|- ( t = G -> ( ze <-> si ) )
ceqsex8v.16 
|- ( s = H -> ( si <-> rh ) )
Assertion ceqsex8v 
|- ( E. x E. y E. z E. w E. v E. u E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) <-> rh )

Proof

Step Hyp Ref Expression
1 ceqsex8v.1 
 |-  A e. _V
2 ceqsex8v.2 
 |-  B e. _V
3 ceqsex8v.3 
 |-  C e. _V
4 ceqsex8v.4 
 |-  D e. _V
5 ceqsex8v.5 
 |-  E e. _V
6 ceqsex8v.6 
 |-  F e. _V
7 ceqsex8v.7 
 |-  G e. _V
8 ceqsex8v.8 
 |-  H e. _V
9 ceqsex8v.9 
 |-  ( x = A -> ( ph <-> ps ) )
10 ceqsex8v.10 
 |-  ( y = B -> ( ps <-> ch ) )
11 ceqsex8v.11 
 |-  ( z = C -> ( ch <-> th ) )
12 ceqsex8v.12 
 |-  ( w = D -> ( th <-> ta ) )
13 ceqsex8v.13 
 |-  ( v = E -> ( ta <-> et ) )
14 ceqsex8v.14 
 |-  ( u = F -> ( et <-> ze ) )
15 ceqsex8v.15 
 |-  ( t = G -> ( ze <-> si ) )
16 ceqsex8v.16 
 |-  ( s = H -> ( si <-> rh ) )
17 19.42vv 
 |-  ( E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) <-> ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) )
18 17 2exbii 
 |-  ( E. v E. u E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) <-> E. v E. u ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) )
19 19.42vv 
 |-  ( E. v E. u ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) <-> ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) )
20 18 19 bitri 
 |-  ( E. v E. u E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) <-> ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) )
21 3anass 
 |-  ( ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) <-> ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) ) )
22 df-3an 
 |-  ( ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) <-> ( ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) )
23 22 anbi2i 
 |-  ( ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) <-> ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) ) )
24 21 23 bitr4i 
 |-  ( ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) <-> ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) )
25 24 2exbii 
 |-  ( E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) <-> E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) )
26 25 2exbii 
 |-  ( E. v E. u E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) <-> E. v E. u E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) )
27 df-3an 
 |-  ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) <-> ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) )
28 20 26 27 3bitr4i 
 |-  ( E. v E. u E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) <-> ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) )
29 28 2exbii 
 |-  ( E. z E. w E. v E. u E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) <-> E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) )
30 29 2exbii 
 |-  ( E. x E. y E. z E. w E. v E. u E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) <-> E. x E. y E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) )
31 9 3anbi3d 
 |-  ( x = A -> ( ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) <-> ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ps ) ) )
32 31 4exbidv 
 |-  ( x = A -> ( E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) <-> E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ps ) ) )
33 10 3anbi3d 
 |-  ( y = B -> ( ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ps ) <-> ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ch ) ) )
34 33 4exbidv 
 |-  ( y = B -> ( E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ps ) <-> E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ch ) ) )
35 11 3anbi3d 
 |-  ( z = C -> ( ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ch ) <-> ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ th ) ) )
36 35 4exbidv 
 |-  ( z = C -> ( E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ch ) <-> E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ th ) ) )
37 12 3anbi3d 
 |-  ( w = D -> ( ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ th ) <-> ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ta ) ) )
38 37 4exbidv 
 |-  ( w = D -> ( E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ th ) <-> E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ta ) ) )
39 1 2 3 4 32 34 36 38 ceqsex4v 
 |-  ( E. x E. y E. z E. w ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) /\ E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ph ) ) <-> E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ta ) )
40 5 6 7 8 13 14 15 16 ceqsex4v 
 |-  ( E. v E. u E. t E. s ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) /\ ta ) <-> rh )
41 30 39 40 3bitri 
 |-  ( E. x E. y E. z E. w E. v E. u E. t E. s ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ( ( v = E /\ u = F ) /\ ( t = G /\ s = H ) ) /\ ph ) <-> rh )