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

Theorem ori 388
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 383 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
31, 2mpbi 218 1 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 381
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 195  df-or 383
This theorem is referenced by:  3ori  1379  mtpor  1685  exmoeu  2484  moanim  2511  moexex  2523  mo2icl  3346  mosubopt  4883  fvrn0  6106  eliman0  6113  dff3  6260  onuninsuci  6904  omelon2  6941  infensuc  7995  rankxpsuc  8600  cardlim  8653  alephreg  9255  tskcard  9454  sinhalfpilem  23931  sltres  30862
  Copyright terms: Public domain W3C validator