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

Theorem ori 375
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 370 . 2  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
31, 2mpbi 208 1  |-  ( -. 
ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368
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 370
This theorem is referenced by:  3ori  1283  mtpor  1582  exmoeu  2304  moanim  2345  moexex  2364  moexexOLD  2365  mo2icl  3275  mosubopt  4738  fvrn0  5879  eliman0  5886  dff3  6025  onuninsuci  6646  omelon2  6683  infensuc  7685  rankxpsuc  8289  cardlim  8342  alephreg  8946  tskcard  9148  sinhalfpilem  22582  sltres  28987
  Copyright terms: Public domain W3C validator