Theorem ord 714

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 712	. 2 ⊢ ((𝜓 ∨ 𝜒) → (¬ 𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.8  800  orcanai  914  ax12  1492  swopo  4269  sotritrieq  4288  suc11g  4519  ordsoexmid  4524  nnsuc  4578  sotri2  4986  nnsucsssuc  6442  nntri2  6444  nntri1  6446  nnsseleq  6451  djulclb  7002  0ct  7054  exmidomniim  7087  omniwomnimkv  7113  elni2  7237  nlt1pig  7264  nngt1ne1  8874  zleloe  9220  zapne  9244  nneo  9273  zeo2  9276  fzocatel  10108  dfphi2  12111  prmdiv  12126  odzdvds  12136  bj-peano4  13627