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

Theorem orri 889
Description: Infer disjunction from implication. (Contributed by NM, 11-Jun-1994.)
Hypothesis
Ref Expression
orri.1 𝜑𝜓)
Assertion
Ref Expression
orri (𝜑𝜓)

Proof of Theorem orri
StepHypRef Expression
1 orri.1 . 2 𝜑𝜓)
2 df-or 875 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
31, 2mpbir 223 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 874
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 199  df-or 875
This theorem is referenced by:  orci  892  olci  893  pm2.25  914  curryax  918  exmid  919  pm2.13  922  pm5.11  968  pm5.12  969  pm5.14  970  pm5.55  972  pm3.12  1017  pm5.15  1037  pm5.54  1042  4exmid  1075  rb-ax2  1849  rb-ax3  1850  rb-ax4  1851  exmo  2602  exmoOLD  2637  axi12  2775  axbnd  2776  exmidne  2981  ifeqor  4326  fvbr0  6438  letrii  10452  clwwlknondisj  27451  clwwlknondisjOLD  27456  poimirlem26  33924  tsbi3  34428  tsan2  34435  tsan3  34436  clsk1indlem2  39122
  Copyright terms: Public domain W3C validator