Theorem ord 736

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm2.8  822  orcanai  940  ax12  1565  swopo  4451  sotritrieq  4470  suc11g  4704  ordsoexmid  4709  nnsuc  4763  sotri2  5185  nnsucsssuc  6765  nntri2  6767  nntri1  6769  nnsseleq  6774  djulclb  7395  0ct  7447  exmidomniim  7481  omniwomnimkv  7507  elni2  7681  nlt1pig  7708  nngt1ne1  9339  zleloe  9691  zapne  9719  nneo  9749  zeo2  9752  fzocatel  10617  seqf1oglem1  10956  seqf1oglem2  10957  bitsinv1lem  12728  dfphi2  12998  prmdiv  13013  odzdvds  13024  pc2dvds  13109  fldivp1  13127  pcfac  13129  1arith  13146  4sqlem10  13166  plyaddlem1  15848  plymullem1  15849  gausslemma2dlem4  16183  lgseisenlem1  16189  bj-peano4  16981