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

Theorem orci 861
 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 858 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   ∨ wo 843 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 209  df-or 844 This theorem is referenced by:  truorfal  1571  trunortruOLD  1583  trunorfalOLD  1585  prid1g  4695  isso2i  5507  mpo0v  7237  0wdom  9033  nneo  12065  mnfltpnf  12520  bcpasc  13680  isumless  15199  binomfallfaclem2  15393  lcmfunsnlem2lem1  15981  srabase  19949  sraaddg  19950  sramulr  19951  m2detleib  21239  fctop  21611  cctop  21613  ovoliunnul  24107  vitalilem5  24212  logtayl  25242  bpos1  25858  usgrexmpldifpr  27039  cffldtocusgr  27228  pthdlem2  27548  inindif  30277  disjunsn  30343  circlemethhgt  31914  fmla0disjsuc  32645  ifpimimb  39868  ifpimim  39873  binomcxplemnn0  40679  binomcxplemnotnn0  40686  salexct  42616  onenotinotbothi  43168  twonotinotbothi  43169  clifte  43170  cliftet  43171  paireqne  43672  sbgoldbo  43951  zlmodzxzldeplem  44552  ldepslinc  44563  line2x  44740  inlinecirc02plem  44772  alimp-surprise  44880  aacllem  44901
 Copyright terms: Public domain W3C validator