MPE Home 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 219 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 196  df-or 384
This theorem is referenced by:  3ori  1380  mtpor  1686  exmoeu  2490  moanim  2517  moexex  2529  mo2icl  3352  mosubopt  4897  fvrn0  6126  eliman0  6133  dff3  6280  onuninsuci  6932  omelon2  6969  infensuc  8023  rankxpsuc  8628  cardlim  8681  alephreg  9283  tskcard  9482  sinhalfpilem  24019  sltres  31061
  Copyright terms: Public domain W3C validator