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  moexex  2212  mo2icl  2944  mosubopt  4264  onuninsuci  4631  omelon2  4668  fvrn0  5550  dff3  5673  tfrlem14  6407  infensuc  7039  rankxpsuc  7552  cardlim  7605  cardom  7619  unialeph  7728  brdom3  8153  alephreg  8204  tskcard  8403  sinhalfpilem  19834  sltres  24318  mof  24849
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