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

Theorem ceqsex8v 2900
Description: Elimination of eight existential quantifiers, using implicit substitution. (Contributed by NM, 23-Sep-2011.)
Hypotheses
Ref Expression
ceqsex8v.1
ceqsex8v.2
ceqsex8v.3
ceqsex8v.4
ceqsex8v.5
ceqsex8v.6
ceqsex8v.7
ceqsex8v.8
ceqsex8v.9
ceqsex8v.10
ceqsex8v.11
ceqsex8v.12
ceqsex8v.13
ceqsex8v.14
ceqsex8v.15
ceqsex8v.16
Assertion
Ref Expression
ceqsex8v
Distinct variable groups:   ,,,,,,,,   ,,,,,,,,   ,,,,,,,,   ,,,,,,,,   ,,,,,,,,   ,,,,,,,,   ,,,,,,,,   ,,,,,,,,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)   (,,,,,,)

Proof of Theorem ceqsex8v
StepHypRef Expression
1 19.42vv 1907 . . . . . . 7
212exbii 1583 . . . . . 6
3 19.42vv 1907 . . . . . 6
42, 3bitri 240 . . . . 5
5 3anass 938 . . . . . . . 8
6 df-3an 936 . . . . . . . . 9
76anbi2i 675 . . . . . . . 8
85, 7bitr4i 243 . . . . . . 7
982exbii 1583 . . . . . 6
1092exbii 1583 . . . . 5
11 df-3an 936 . . . . 5
124, 10, 113bitr4i 268 . . . 4
13122exbii 1583 . . 3
14132exbii 1583 . 2
15 ceqsex8v.1 . . . 4
16 ceqsex8v.2 . . . 4
17 ceqsex8v.3 . . . 4
18 ceqsex8v.4 . . . 4
19 ceqsex8v.9 . . . . . 6
20193anbi3d 1258 . . . . 5
21204exbidv 1630 . . . 4
22 ceqsex8v.10 . . . . . 6
23223anbi3d 1258 . . . . 5
24234exbidv 1630 . . . 4
25 ceqsex8v.11 . . . . . 6
26253anbi3d 1258 . . . . 5
27264exbidv 1630 . . . 4
28 ceqsex8v.12 . . . . . 6
29283anbi3d 1258 . . . . 5
30294exbidv 1630 . . . 4
3115, 16, 17, 18, 21, 24, 27, 30ceqsex4v 2898 . . 3
32 ceqsex8v.5 . . . 4
33 ceqsex8v.6 . . . 4
34 ceqsex8v.7 . . . 4
35 ceqsex8v.8 . . . 4
36 ceqsex8v.13 . . . 4
37 ceqsex8v.14 . . . 4
38 ceqsex8v.15 . . . 4
39 ceqsex8v.16 . . . 4
4032, 33, 34, 35, 36, 37, 38, 39ceqsex4v 2898 . . 3
4131, 40bitri 240 . 2
4214, 41bitri 240 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176   wa 358   w3a 934  wex 1541   wceq 1642   wcel 1710  cvv 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