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

Theorem olci 865
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 861 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 846
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 206  df-or 847
This theorem is referenced by:  falortru  1581  opthhausdorff  5479  sucidg  6403  kmlem2  10094  sornom  10220  leid  11258  pnf0xnn0  12499  xrleid  13077  xmul01  13193  bcn1  14220  odd2np1lem  16229  lcm0val  16477  lcmfunsnlem2lem1  16521  lcmfunsnlem2  16523  coprmprod  16544  coprmproddvdslem  16545  prmrec  16801  smndex2dnrinv  18732  sratsetOLD  20668  sradsOLD  20671  m2detleib  21996  zclmncvs  24528  itg0  25160  itgz  25161  coemullem  25627  ftalem5  26442  chp1  26532  prmorcht  26543  pclogsum  26579  logexprlim  26589  bpos1  26647  addsqnreup  26807  pntpbnd1  26950  axlowdimlem16  27948  usgrexmpldifpr  28248  cusgrsizeindb1  28440  pthdlem2  28758  ex-or  29407  plymulx0  33199  signstfvn  33221  bj-0eltag  35478  bj-inftyexpidisj  35710  mblfinlem2  36145  volsupnfl  36152  12gcd5e1  40489  ifpdfor  41811  ifpim1  41815  ifpnot  41816  ifpid2  41817  ifpim2  41818  ifpim1g  41847  ifpbi1b  41849  icccncfext  44202  fourierdlem103  44524  fourierdlem104  44525  etransclem24  44573  etransclem35  44584  abnotataxb  45225  dandysum2p2e4  45307  paireqne  45777  sbgoldbo  46053  zlmodzxzldeplem  46653  line2x  46914  aacllem  47322
  Copyright terms: Public domain W3C validator