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

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

Proof of Theorem ori
StepHypRef Expression
1 ori.1 . 2  |-  ( ph  \/  ps )
2 df-or 368 . 2  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
31, 2mpbi 208 1  |-  ( -. 
ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ 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:  3ori  1290  mtpor  1623  exmoeu  2272  moanim  2301  moexex  2314  mo2icl  3228  mosubopt  4688  fvrn0  5871  eliman0  5878  dff3  6022  onuninsuci  6658  omelon2  6695  infensuc  7733  rankxpsuc  8332  cardlim  8385  alephreg  8989  tskcard  9189  sinhalfpilem  23148  sltres  30124
  Copyright terms: Public domain W3C validator