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

Step	Hyp	Ref	Expression
1		ori.1	. 2 ⊢ (𝜑 ∨ 𝜓)
2		df-or 384	. 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓))
3	1, 2	mpbi 220	1 ⊢ (¬ 𝜑 → 𝜓)

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 197  df-or 384

This theorem is referenced by:  3ori  1501  mtpor  1808  exmoeu  2604  moanim  2631  moexex  2643  mo2icl  3491  mosubopt  5076  fvrn0  6329  eliman0  6336  dff3  6487  onuninsuci  7157  omelon2  7194  infensuc  8254  rankxpsuc  8858  cardlim  8911  alephreg  9517  tskcard  9716  sinhalfpilem  24335  sltres  32042