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

Theorem bnj153 29228
 Description: Technical lemma for bnj852 29269. 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
bnj153.1
bnj153.2
bnj153.3
bnj153.4
bnj153.5
Assertion
Ref Expression
bnj153
Distinct variable groups:   ,,,,,   ,,,,,   ,
Allowed substitution hints:   (,,,,,)   (,,,,,)   (,,,,,)   (,,,,,)   ()   (,,,,,)   ()

Proof of Theorem bnj153
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bnj153.1 . 2
2 bnj153.2 . 2
3 bnj153.3 . 2
4 bnj153.4 . 2
5 bnj153.5 . 2
6 biid 227 . 2
7 biid 227 . . . 4
81, 7bnj118 29217 . . 3
98bicomi 193 . 2
10 biid 227 . . . 4
11 bnj105 29066 . . . . 5
122, 11bnj92 29210 . . . 4
1310, 12bitri 240 . . 3
1413bicomi 193 . 2
15 biid 227 . 2
16 biid 227 . 2
17 biid 227 . 2
18 biid 227 . . . . 5
196, 18, 7, 10bnj121 29218 . . . 4
208anbi2i 675 . . . . . . 7
2120, 13anbi12i 678 . . . . . 6
22 df-3an 936 . . . . . 6
23 df-3an 936 . . . . . 6
2421, 22, 233bitr4i 268 . . . . 5
2524imbi2i 303 . . . 4
2619, 25bitri 240 . . 3
2726bicomi 193 . 2
28 eqid 2296 . 2
29 biid 227 . 2
30 biid 227 . 2
31 snex 4232 . . . 4
3227, 31bnj524 29082 . . 3
33 biid 227 . . . . 5
34 biid 227 . . . . 5
35 biid 227 . . . . 5
3628, 33, 34, 35, 19bnj124 29219 . . . 4
371, 7, 33, 28bnj125 29220 . . . . . . . 8
3837anbi2i 675 . . . . . . 7
392, 10, 34, 28bnj126 29221 . . . . . . 7
4038, 39anbi12i 678 . . . . . 6
41 df-3an 936 . . . . . 6
42 df-3an 936 . . . . . 6
4340, 41, 423bitr4i 268 . . . . 5
4443imbi2i 303 . . . 4
4536, 44bitri 240 . . 3
4632, 45bitr2i 241 . 2
47 biid 227 . 2
48 biid 227 . . . . 5
49 biid 227 . . . . 5
50 biid 227 . . . . 5
51 biid 227 . . . . 5
5248, 49, 50, 51bnj156 29072 . . . 4
5350, 8bnj154 29226 . . . . . . 7
5453anbi2i 675 . . . . . 6
5551, 13bnj155 29227 . . . . . 6
5654, 55anbi12i 678 . . . . 5
57 df-3an 936 . . . . 5
58 df-3an 936 . . . . 5
5956, 57, 583bitr4i 268 . . . 4
6052, 59bitri 240 . . 3
6120, 12anbi12i 678 . . . . 5
6261, 22, 233bitr4i 268 . . . 4
6362sbcbii 3059 . . 3
6460, 63bitr3i 242 . 2
65 biid 227 . 2
66 biid 227 . 2
671, 2, 3, 4, 5, 6, 9, 14, 15, 16, 17, 27, 28, 29, 30, 46, 47, 64, 65, 66bnj151 29225 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934  wex 1531   wceq 1632   wcel 1696  weu 2156  wmo 2157  wral 2556  wsbc 3004   cdif 3162  c0 3468  csn 3653  cop 3656  ciun 3921   class class class wbr 4039   cep 4319   csuc 4410  com 4672   wfn 5266  cfv 5271  c1o 6488   c-bnj14 29029   w-bnj15 29033 This theorem is referenced by:  bnj852  29269 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-suc 4414  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-1o 6495  df-bnj13 29032  df-bnj15 29034
 Copyright terms: Public domain W3C validator