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

Theorem ori 389
 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 384 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
31, 2mpbi 220 1 𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382 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 384 This theorem is referenced by:  3ori  1501  mtpor  1808  exmoeu  2604  moanim  2631  moexex  2643  mo2icl  3491  mosubopt  5076  fvrn0  6329  eliman0  6336  dff3  6487  onuninsuci  7157  omelon2  7194  infensuc  8254  rankxpsuc  8858  cardlim  8911  alephreg  9517  tskcard  9716  sinhalfpilem  24335  sltres  32042
 Copyright terms: Public domain W3C validator