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

Theorem olci 405
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 390 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 382
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 197  df-or 384
This theorem is referenced by:  falortru  1661  opthhausdorff  5128  sucidg  5965  kmlem2  9186  sornom  9312  leid  10346  pnf0xnn0  11583  xrleid  12197  xmul01  12311  bcn1  13315  odd2np1lem  15287  lcm0val  15530  lcmfunsnlem2lem1  15574  lcmfunsnlem2  15576  coprmprod  15598  coprmproddvdslem  15599  prmrec  15849  sratset  19407  srads  19409  m2detleib  20660  zclmncvs  23169  itg0  23766  itgz  23767  coemullem  24226  ftalem5  25024  chp1  25114  prmorcht  25125  pclogsum  25161  logexprlim  25171  bpos1  25229  pntpbnd1  25496  axlowdimlem16  26058  usgrexmpldifpr  26371  cusgrsizeindb1  26578  pthdlem2  26896  clwwlkn0OLD  27179  ex-or  27611  plymulx0  30955  bj-0eltag  33291  bj-inftyexpidisj  33427  mblfinlem2  33779  volsupnfl  33786  ifpdfor  38330  ifpim1  38334  ifpnot  38335  ifpid2  38336  ifpim2  38337  ifpim1g  38367  ifpbi1b  38369  icccncfext  40622  fourierdlem103  40948  fourierdlem104  40949  etransclem24  40997  etransclem35  41008  abnotataxb  41608  dandysum2p2e4  41690  sbgoldbo  42204  zlmodzxzldeplem  42816  aacllem  43079
  Copyright terms: Public domain W3C validator