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

Theorem orci 390
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 144 . 2  |-  ( -. 
ph  ->  ps )
32orri 376 1  |-  ( ph  \/  ps )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368
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 185  df-or 370
This theorem is referenced by:  truorfal  1399  prid1g  4082  isso2i  4774  0wdom  7889  nneo  10829  mnfltpnf  11210  bcpasc  12207  isumless  13419  srabase  17374  sraaddg  17375  sramulr  17376  m2detleib  18562  fctop  18733  cctop  18735  ovoliunnul  21115  vitalilem5  21218  logtayl  22231  bpos1  22748  usgraexmpldifpr  23463  inindif  26042  disjunsn  26080  binomfallfaclem2  27680  zlmodzxzldeplem  31150  ldepslinc  31161  alimp-surprise  31435
  Copyright terms: Public domain W3C validator