New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ceqsex8v GIF version

Theorem ceqsex8v 2900
 Description: Elimination of eight existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.)
Hypotheses
Ref Expression
ceqsex8v.1 A V
ceqsex8v.2 B V
ceqsex8v.3 C V
ceqsex8v.4 D V
ceqsex8v.5 E V
ceqsex8v.6 F V
ceqsex8v.7 G V
ceqsex8v.8 H V
ceqsex8v.9 (x = A → (φψ))
ceqsex8v.10 (y = B → (ψχ))
ceqsex8v.11 (z = C → (χθ))
ceqsex8v.12 (w = D → (θτ))
ceqsex8v.13 (v = E → (τη))
ceqsex8v.14 (u = F → (ηζ))
ceqsex8v.15 (t = G → (ζσ))
ceqsex8v.16 (s = H → (σρ))
Assertion
Ref Expression
ceqsex8v (xyzwvuts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H)) φ) ↔ ρ)
Distinct variable groups:   x,y,z,w,v,u,t,s,A   x,B,y,z,w,v,u,t,s   x,C,y,z,w,v,u,t,s   x,D,y,z,w,v,u,t,s   x,E,y,z,w,v,u,t,s   x,F,y,z,w,v,u,t,s   x,G,y,z,w,v,u,t,s   x,H,y,z,w,v,u,t,s   ψ,x   χ,y   θ,z   τ,w   η,v   ζ,u   σ,t   ρ,s
Allowed substitution hints:   φ(x,y,z,w,v,u,t,s)   ψ(y,z,w,v,u,t,s)   χ(x,z,w,v,u,t,s)   θ(x,y,w,v,u,t,s)   τ(x,y,z,v,u,t,s)   η(x,y,z,w,u,t,s)   ζ(x,y,z,w,v,t,s)   σ(x,y,z,w,v,u,s)   ρ(x,y,z,w,v,u,t)

Proof of Theorem ceqsex8v
StepHypRef Expression
1 19.42vv 1907 . . . . . . 7 (ts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H) φ)) ↔ (((x = A y = B) (z = C w = D)) ts((v = E u = F) (t = G s = H) φ)))
212exbii 1583 . . . . . 6 (vuts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H) φ)) ↔ vu(((x = A y = B) (z = C w = D)) ts((v = E u = F) (t = G s = H) φ)))
3 19.42vv 1907 . . . . . 6 (vu(((x = A y = B) (z = C w = D)) ts((v = E u = F) (t = G s = H) φ)) ↔ (((x = A y = B) (z = C w = D)) vuts((v = E u = F) (t = G s = H) φ)))
42, 3bitri 240 . . . . 5 (vuts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H) φ)) ↔ (((x = A y = B) (z = C w = D)) vuts((v = E u = F) (t = G s = H) φ)))
5 3anass 938 . . . . . . . 8 ((((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H)) φ) ↔ (((x = A y = B) (z = C w = D)) (((v = E u = F) (t = G s = H)) φ)))
6 df-3an 936 . . . . . . . . 9 (((v = E u = F) (t = G s = H) φ) ↔ (((v = E u = F) (t = G s = H)) φ))
76anbi2i 675 . . . . . . . 8 ((((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H) φ)) ↔ (((x = A y = B) (z = C w = D)) (((v = E u = F) (t = G s = H)) φ)))
85, 7bitr4i 243 . . . . . . 7 ((((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H)) φ) ↔ (((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H) φ)))
982exbii 1583 . . . . . 6 (ts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H)) φ) ↔ ts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H) φ)))
1092exbii 1583 . . . . 5 (vuts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H)) φ) ↔ vuts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H) φ)))
11 df-3an 936 . . . . 5 (((x = A y = B) (z = C w = D) vuts((v = E u = F) (t = G s = H) φ)) ↔ (((x = A y = B) (z = C w = D)) vuts((v = E u = F) (t = G s = H) φ)))
124, 10, 113bitr4i 268 . . . 4 (vuts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H)) φ) ↔ ((x = A y = B) (z = C w = D) vuts((v = E u = F) (t = G s = H) φ)))
13122exbii 1583 . . 3 (zwvuts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H)) φ) ↔ zw((x = A y = B) (z = C w = D) vuts((v = E u = F) (t = G s = H) φ)))
14132exbii 1583 . 2 (xyzwvuts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H)) φ) ↔ xyzw((x = A y = B) (z = C w = D) vuts((v = E u = F) (t = G s = H) φ)))
15 ceqsex8v.1 . . . 4 A V
16 ceqsex8v.2 . . . 4 B V
17 ceqsex8v.3 . . . 4 C V
18 ceqsex8v.4 . . . 4 D V
19 ceqsex8v.9 . . . . . 6 (x = A → (φψ))
20193anbi3d 1258 . . . . 5 (x = A → (((v = E u = F) (t = G s = H) φ) ↔ ((v = E u = F) (t = G s = H) ψ)))
21204exbidv 1630 . . . 4 (x = A → (vuts((v = E u = F) (t = G s = H) φ) ↔ vuts((v = E u = F) (t = G s = H) ψ)))
22 ceqsex8v.10 . . . . . 6 (y = B → (ψχ))
23223anbi3d 1258 . . . . 5 (y = B → (((v = E u = F) (t = G s = H) ψ) ↔ ((v = E u = F) (t = G s = H) χ)))
24234exbidv 1630 . . . 4 (y = B → (vuts((v = E u = F) (t = G s = H) ψ) ↔ vuts((v = E u = F) (t = G s = H) χ)))
25 ceqsex8v.11 . . . . . 6 (z = C → (χθ))
26253anbi3d 1258 . . . . 5 (z = C → (((v = E u = F) (t = G s = H) χ) ↔ ((v = E u = F) (t = G s = H) θ)))
27264exbidv 1630 . . . 4 (z = C → (vuts((v = E u = F) (t = G s = H) χ) ↔ vuts((v = E u = F) (t = G s = H) θ)))
28 ceqsex8v.12 . . . . . 6 (w = D → (θτ))
29283anbi3d 1258 . . . . 5 (w = D → (((v = E u = F) (t = G s = H) θ) ↔ ((v = E u = F) (t = G s = H) τ)))
30294exbidv 1630 . . . 4 (w = D → (vuts((v = E u = F) (t = G s = H) θ) ↔ vuts((v = E u = F) (t = G s = H) τ)))
3115, 16, 17, 18, 21, 24, 27, 30ceqsex4v 2898 . . 3 (xyzw((x = A y = B) (z = C w = D) vuts((v = E u = F) (t = G s = H) φ)) ↔ vuts((v = E u = F) (t = G s = H) τ))
32 ceqsex8v.5 . . . 4 E V
33 ceqsex8v.6 . . . 4 F V
34 ceqsex8v.7 . . . 4 G V
35 ceqsex8v.8 . . . 4 H V
36 ceqsex8v.13 . . . 4 (v = E → (τη))
37 ceqsex8v.14 . . . 4 (u = F → (ηζ))
38 ceqsex8v.15 . . . 4 (t = G → (ζσ))
39 ceqsex8v.16 . . . 4 (s = H → (σρ))
4032, 33, 34, 35, 36, 37, 38, 39ceqsex4v 2898 . . 3 (vuts((v = E u = F) (t = G s = H) τ) ↔ ρ)
4131, 40bitri 240 . 2 (xyzw((x = A y = B) (z = C w = D) vuts((v = E u = F) (t = G s = H) φ)) ↔ ρ)
4214, 41bitri 240 1 (xyzwvuts(((x = A y = B) (z = C w = D)) ((v = E u = F) (t = G s = H)) φ) ↔ ρ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   ∧ w3a 934  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator