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

Theorem orri 378
Description: Infer disjunction from implication. (Contributed by NM, 11-Jun-1994.)
Hypothesis
Ref Expression
orri.1  |-  ( -. 
ph  ->  ps )
Assertion
Ref Expression
orri  |-  ( ph  \/  ps )

Proof of Theorem orri
StepHypRef Expression
1 orri.1 . 2  |-  ( -. 
ph  ->  ps )
2 df-or 372 . 2  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
31, 2mpbir 213 1  |-  ( ph  \/  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 370
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 189  df-or 372
This theorem is referenced by:  orci  392  olci  393  pm2.25  406  exmid  417  pm2.13  420  pm3.12  503  pm5.11  895  pm5.12  896  pm5.14  897  pm5.15  900  pm5.55  908  pm5.54  913  rb-ax2  1636  rb-ax3  1637  rb-ax4  1638  exmo  2324  axi12  2429  axbnd  2430  exmidne  2633  abvor0  3750  ifeqor  3925  fvbr0  5886  letrii  9759  numclwwlkdisj  25808  poimirlem26  31966  tsim2  32373  tsbi3  32377  tsan2  32384  tsan3  32385
  Copyright terms: Public domain W3C validator