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

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

Proof of Theorem orci
StepHypRef Expression
1 orci.1 . . 3 𝜑
21pm2.24i 146 . 2 𝜑𝜓)
32orri 391 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wo 383
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 385
This theorem is referenced by:  truorfal  1509  prid1g  4286  isso2i  5057  0wdom  8460  nneo  11446  mnfltpnf  11945  bcpasc  13091  isumless  14558  binomfallfaclem2  14752  lcmfunsnlem2lem1  15332  srabase  19159  sraaddg  19160  sramulr  19161  m2detleib  20418  fctop  20789  cctop  20791  ovoliunnul  23256  vitalilem5  23362  logtayl  24387  bpos1  24989  usgrexmpldifpr  26131  cffldtocusgr  26324  pthdlem2  26645  inindif  29325  disjunsn  29379  circlemethhgt  30695  ifpimimb  37668  ifpimim  37673  binomcxplemnn0  38368  binomcxplemnotnn0  38375  salexct  40315  onenotinotbothi  40863  twonotinotbothi  40864  clifte  40865  cliftet  40866  sbgoldbo  41440  zlmodzxzldeplem  42052  ldepslinc  42063  alimp-surprise  42291  aacllem  42312
  Copyright terms: Public domain W3C validator