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

Theorem orci 380
Description: Deduction introducing a disjunct. (Contributed by NM, 19-Jan-2008.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
Hypothesis
Ref Expression
orci.1  |-  ph
Assertion
Ref Expression
orci  |-  ( ph  \/  ps )

Proof of Theorem orci
StepHypRef Expression
1 orci.1 . . 3  |-  ph
21pm2.24i 138 . 2  |-  ( -. 
ph  ->  ps )
32orri 366 1  |-  ( ph  \/  ps )
Colors of variables: wff set class
Syntax hints:    \/ wo 358
This theorem is referenced by:  truorfal  1347  prid1g  3854  isso2i  4477  0wdom  7472  nneo  10286  mnfltpnf  10656  bcpasc  11540  isumless  12553  srabase  16178  sraaddg  16179  sramulr  16180  fctop  16992  cctop  16994  ovoliunnul  19271  vitalilem5  19372  logtayl  20419  bpos1  20935  usgraexmpldifpr  21286
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator