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

Step	Hyp	Ref	Expression
1		orri.1	. 2 ⊢ (¬ 𝜑 → 𝜓)
2		df-or 875	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
3	1, 2	mpbir 223	1 ⊢ (𝜑 ∨ 𝜓)

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