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

Theorem ori 364
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 359 . 2  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
31, 2mpbi 199 1  |-  ( -. 
ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357
This theorem is referenced by:  3ori  1242  mtp-or  1528  moexex  2225  mo2icl  2957  mosubopt  4280  onuninsuci  4647  omelon2  4684  fvrn0  5566  dff3  5689  tfrlem14  6423  infensuc  7055  rankxpsuc  7568  cardlim  7621  cardom  7635  unialeph  7744  brdom3  8169  alephreg  8220  tskcard  8419  sinhalfpilem  19850  sltres  24389  mof  24921
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator