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

Theorem ori 366
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 361 . 2  |-  ( (
ph  \/  ps )  <->  ( -.  ph  ->  ps )
)
31, 2mpbi 201 1  |-  ( -. 
ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 359
This theorem is referenced by:  3ori  1245  mtp-or  1548  moexex  2352  mo2icl  3115  mosubopt  4456  onuninsuci  4822  omelon2  4859  fvrn0  5755  dff3  5884  infensuc  7287  rankxpsuc  7808  cardlim  7861  alephreg  8459  tskcard  8658  sinhalfpilem  20376  sltres  25621
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 179  df-or 361
  Copyright terms: Public domain W3C validator