MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orci Structured version   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  1350  prid1g  3902  isso2i  4527  0wdom  7530  nneo  10345  mnfltpnf  10715  bcpasc  11604  isumless  12617  srabase  16242  sraaddg  16243  sramulr  16244  fctop  17060  cctop  17062  ovoliunnul  19395  vitalilem5  19496  logtayl  20543  bpos1  21059  usgraexmpldifpr  21411  binomfallfaclem2  25348
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