Theorem ord 676

Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

Ref	Expression
ord.1	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Assertion

Ref	Expression
ord	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Proof of Theorem ord

Step	Hyp	Ref	Expression
1		ord.1	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
2		pm2.53 674	. 2 ⊢ ((𝜓 ∨ 𝜒) → (¬ 𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 662

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 578  ax-io 663

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm2.8  757  orcanai  871  ax-12  1443  swopo  4096  sotritrieq  4115  suc11g  4335  ordsoexmid  4340  nnsuc  4392  sotri2  4783  nnsucsssuc  6184  nntri2  6186  nntri1  6188  nnsseleq  6193  djulclb  6653  exmidomniim  6701  elni2  6775  nlt1pig  6802  nngt1ne1  8349  zleloe  8692  zapne  8716  nneo  8744  zeo2  8747  fzocatel  9498  dfphi2  10975  bj-peano4  11192