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

Theorem ori 887
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 874 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
31, 2mpbi 221 1 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 873
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 198  df-or 874
This theorem is referenced by:  3ori  1548  mtpor  1865  exmoeuOLD  2623  moanim  2651  moexex  2663  mo2icl  3546  mosubopt  5133  fvrn0  6407  eliman0  6415  dff3  6566  onuninsuci  7242  omelon2  7279  infensuc  8349  rankxpsuc  8964  cardlim  9053  alephreg  9661  tskcard  9860  sinhalfpilem  24521  sltres  32280
  Copyright terms: Public domain W3C validator