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 150 . 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 206  df-or 847
This theorem is referenced by:  truorfal  1580  prid1g  4762  isso2i  5621  mpo0v  7487  0wdom  9560  nneo  12641  mnfltpnf  13101  bcpasc  14276  isumless  15786  binomfallfaclem2  15979  lcmfunsnlem2lem1  16570  srabaseOLD  20780  sraaddgOLD  20782  sramulrOLD  20784  m2detleib  22114  fctop  22488  cctop  22490  ovoliunnul  25005  vitalilem5  25110  logtayl  26149  bpos1  26765  0slt1s  27309  usgrexmpldifpr  28494  cffldtocusgr  28683  pthdlem2  29004  inindif  31731  disjunsn  31802  circlemethhgt  33592  fmla0disjsuc  34326  disjressuc2  37195  ifpimimb  42187  ifpimim  42192  binomcxplemnn0  43040  binomcxplemnotnn0  43047  salexct  44984  onenotinotbothi  45577  twonotinotbothi  45578  clifte  45579  cliftet  45580  paireqne  46113  sbgoldbo  46389  zlmodzxzldeplem  47080  ldepslinc  47091  line2x  47341  inlinecirc02plem  47373  alimp-surprise  47728  aacllem  47749
  Copyright terms: Public domain W3C validator