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

Theorem orci 388
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 374 1  |-  ( ph  \/  ps )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 366
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 368
This theorem is referenced by:  truorfal  1427  prid1g  4122  isso2i  4821  0wdom  7988  nneo  10942  mnfltpnf  11338  bcpasc  12381  isumless  13739  srabase  18019  sraaddg  18020  sramulr  18021  m2detleib  19300  fctop  19672  cctop  19674  ovoliunnul  22084  vitalilem5  22187  logtayl  23209  bpos1  23756  usgraexmpldifpr  24602  inindif  27613  disjunsn  27664  binomfallfaclem2  29403  binomcxplemnn0  31495  binomcxplemnotnn0  31502  zlmodzxzldeplem  33353  ldepslinc  33364  alimp-surprise  33583  aacllem  33604  ifpimimb  38116  ifpimim  38117
  Copyright terms: Public domain W3C validator