Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj917 Structured version   Unicode version

Theorem bnj917 34135
 Description: Technical lemma for bnj69 34209. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj917.1
bnj917.2
bnj917.3
bnj917.4
bnj917.5
Assertion
Ref Expression
bnj917
Distinct variable groups:   ,,,,   ,   ,,,,   ,,,,   ,
Allowed substitution hints:   (,,)   (,,,)   (,,,)   (,,,)   (,,)

Proof of Theorem bnj917
StepHypRef Expression
1 bnj917.1 . . 3
2 bnj917.2 . . 3
3 bnj917.3 . . 3
4 bnj917.4 . . 3
5 biid 236 . . 3
61, 2, 3, 4, 5bnj916 34134 . 2
7 bnj917.5 . . . . . 6
8 bnj252 33898 . . . . . 6
97, 8bitri 249 . . . . 5
1093anbi1i 1187 . . . 4
11 bnj253 33899 . . . 4
1210, 11bitr4i 252 . . 3
13123exbii 1670 . 2
146, 13sylibr 212 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 973   wceq 1395  wex 1613   wcel 1819  cab 2442  wral 2807  wrex 2808   cdif 3468  c0 3793  csn 4032  ciun 4332   csuc 4889   wfn 5589  cfv 5594  com 6699   w-bnj17 33881   c-bnj14 33883   c-bnj18 33889 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-iun 4334  df-fn 5597  df-bnj17 33882  df-bnj18 33890 This theorem is referenced by:  bnj981  34151  bnj996  34156
 Copyright terms: Public domain W3C validator