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  1279  mtpor  1578  exmoeu  2298  moanim  2339  moexex  2358  moexexOLD  2359  mo2icl  3245  mosubopt  4698  fvrn0  5822  eliman0  5829  dff3  5966  onuninsuci  6562  omelon2  6599  infensuc  7600  rankxpsuc  8201  cardlim  8254  alephreg  8858  tskcard  9060  sinhalfpilem  22059  sltres  27950
  Copyright terms: Public domain W3C validator