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

Theorem orci 391
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 377 1  |-  ( ph  \/  ps )
Colors of variables: wff setvar class
Syntax hints:    \/ wo 369
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 188  df-or 371
This theorem is referenced by:  truorfal  1464  prid1g  4049  isso2i  4749  0wdom  8038  nneo  10970  mnfltpnf  11379  bcpasc  12456  isumless  13846  binomfallfaclem2  14036  lcmfunsnlem2lem1  14554  srabase  18344  sraaddg  18345  sramulr  18346  m2detleib  19598  fctop  19961  cctop  19963  ovoliunnul  22402  vitalilem5  22512  logtayl  23547  bpos1  24153  usgraexmpldifpr  25069  inindif  28093  disjunsn  28150  ifpimimb  36061  ifpimim  36066  binomcxplemnn0  36611  binomcxplemnotnn0  36618  onenotinotbothi  38335  twonotinotbothi  38336  clifte  38337  cliftet  38338  zlmodzxzldeplem  39884  ldepslinc  39895  alimp-surprise  40112  aacllem  40133
  Copyright terms: Public domain W3C validator