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

Theorem orci 864
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
orci (𝜑𝜓)

Proof of Theorem orci
StepHypRef Expression
1 orci.1 . . 3 𝜑
21pm2.24i 153 . 2 𝜑𝜓)
32orri 861 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  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 210  df-or 847
This theorem is referenced by:  truorfal  1580  trunortruOLD  1592  trunorfalOLD  1594  prid1g  4651  isso2i  5477  mpo0v  7252  0wdom  9107  nneo  12147  mnfltpnf  12604  bcpasc  13773  isumless  15293  binomfallfaclem2  15486  lcmfunsnlem2lem1  16079  srabase  20069  sraaddg  20070  sramulr  20071  m2detleib  21382  fctop  21755  cctop  21757  ovoliunnul  24259  vitalilem5  24364  logtayl  25403  bpos1  26019  usgrexmpldifpr  27200  cffldtocusgr  27389  pthdlem2  27709  inindif  30437  disjunsn  30507  circlemethhgt  32193  fmla0disjsuc  32931  0slt1s  33664  ifpimimb  40665  ifpimim  40670  binomcxplemnn0  41505  binomcxplemnotnn0  41512  salexct  43415  onenotinotbothi  43967  twonotinotbothi  43968  clifte  43969  cliftet  43970  paireqne  44497  sbgoldbo  44773  zlmodzxzldeplem  45373  ldepslinc  45384  line2x  45634  inlinecirc02plem  45666  alimp-surprise  45937  aacllem  45958
  Copyright terms: Public domain W3C validator