Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  olci Unicode version

Theorem olci 391
 Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
Hypothesis
Ref Expression
orci.1
Assertion
Ref Expression
olci

Proof of Theorem olci
StepHypRef Expression
1 orci.1 . . 3
21a1i 11 . 2
32orri 376 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  \/wo 368 This theorem is referenced by:  falortru  1425  sucidg  4961  kmlem2  8552  sornom  8678  leid  9701  xrleid  11385  xmul01  11488  bcn1  12391  odd2np1lem  14045  prmrec  14440  sratset  17830  srads  17832  m2detleib  19133  itg0  22186  itgz  22187  coemullem  22647  ftalem5  23350  chp1  23441  prmorcht  23452  pclogsum  23490  logexprlim  23500  bpos1  23558  pntpbnd1  23771  axlowdimlem16  24260  usgraexmpldifpr  24400  cusgrasizeindb1  24471  vdgrf  24898  ex-or  25142  plymulx0  28504  mblfinlem2  30052  volsupnfl  30059  lcm0val  31200  icccncfext  31690  fourierdlem103  31992  fourierdlem104  31993  etransclem24  32041  etransclem35  32052  abnotataxb  32112  dandysum2p2e4  32170  zlmodzxzldeplem  33099  aacllem  33216  bj-0eltag  34536  bj-inftyexpidisj  34613  bj-ifid2  37711  bj-ifim1  37712  bj-ifim2  37713  bj-ifim1g  37714  bj-ifnot  37717  bj-ifdfor  37722 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 185  df-or 370
 Copyright terms: Public domain W3C validator