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

Theorem orri 377
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 371 . 2  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
31, 2mpbir 212 1  |-  ( ph  \/  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ 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:  orci  391  olci  392  pm2.25  405  exmid  416  pm2.13  419  pm3.12  502  pm5.11  892  pm5.12  893  pm5.14  894  pm5.15  897  pm5.55  905  pm5.54  910  rb-ax2  1632  rb-ax3  1633  rb-ax4  1634  exmo  2289  axi12  2396  axbnd  2397  exmidne  2627  abvor0  3777  ifeqor  3950  fvbr0  5893  letrii  9748  numclwwlkdisj  25650  poimirlem26  31670  tsim2  32077  tsbi3  32081  tsan2  32088  tsan3  32089
  Copyright terms: Public domain W3C validator