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

Theorem orri 858
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 844 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
31, 2mpbir 233 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 843
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 209  df-or 844
This theorem is referenced by:  orci  861  olci  862  pm2.25  886  curryax  890  exmid  891  pm2.13  894  pm5.11g  940  pm5.12  942  pm5.14  943  pm5.55  945  pm3.12  990  pm5.15  1009  pm5.54  1014  4exmid  1046  rb-ax2  1753  rb-ax3  1754  rb-ax4  1755  exmo  2623  axi12  2792  axi12OLD  2793  axbndOLD  2795  exmidne  3029  ifeqor  4519  fvbr0  6700  letrii  10768  clwwlknondisj  27893  poimirlem26  34922  tsbi3  35417  tsan2  35424  tsan3  35425  clsk1indlem2  40398
  Copyright terms: Public domain W3C validator