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

Theorem orci 379
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 136 . 2  |-  ( -. 
ph  ->  ps )
32orri 365 1  |-  ( ph  \/  ps )
Colors of variables: wff set class
Syntax hints:    \/ wo 357
This theorem is referenced by:  truorfal  1331  prid1g  3732  isso2i  4346  0wdom  7284  nneo  10095  mnfltpnf  10465  bcpasc  11333  isumless  12304  srabase  15931  sraaddg  15932  sramulr  15933  fctop  16741  cctop  16743  ovoliunnul  18866  vitalilem5  18967  logtayl  20007  bpos1  20522  pfsubkl  26047  pgapspf2  26053  usgraex0elv  28128  usgraex1elv  28129  usgraex2elv  28130  usgraex3elv  28131  usgraexmpldifpr  28132
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 177  df-or 359
  Copyright terms: Public domain W3C validator