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

Theorem ori 390
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 385 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
31, 2mpbi 220 1 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383
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 197  df-or 385
This theorem is referenced by:  3ori  1386  mtpor  1693  exmoeu  2500  moanim  2527  moexex  2539  mo2icl  3379  mosubopt  4962  fvrn0  6203  eliman0  6210  dff3  6358  onuninsuci  7025  omelon2  7062  infensuc  8123  rankxpsuc  8730  cardlim  8783  alephreg  9389  tskcard  9588  sinhalfpilem  24196  sltres  31789
  Copyright terms: Public domain W3C validator