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

Theorem ori 375
Description: Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.)
Hypothesis
Ref Expression
ori.1
Assertion
Ref Expression
ori

Proof of Theorem ori
StepHypRef Expression
1 ori.1 . 2
2 df-or 370 . 2
31, 2mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 368
This theorem is referenced by:  3ori  1288  mtpor  1603  exmoeu  2316  moanim  2350  moexex  2363  mo2icl  3278  mosubopt  4750  fvrn0  5893  eliman0  5900  dff3  6044  onuninsuci  6675  omelon2  6712  infensuc  7715  rankxpsuc  8321  cardlim  8374  alephreg  8978  tskcard  9180  sinhalfpilem  22856  sltres  29424
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
  Copyright terms: Public domain W3C validator