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  3745  isso2i  4362  0wdom  7300  nneo  10111  mnfltpnf  10481  bcpasc  11349  isumless  12320  srabase  15947  sraaddg  15948  sramulr  15949  fctop  16757  cctop  16759  ovoliunnul  18882  vitalilem5  18983  logtayl  20023  bpos1  20538  pfsubkl  26150  pgapspf2  26156  usgraex0elv  28262  usgraex1elv  28263  usgraex2elv  28264  usgraex3elv  28265  usgraexmpldifpr  28266
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