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  9341  zleloe  9695  zapne  9723  nneo  9753  zeo2  9756  fzocatel  10627  seqf1oglem1  10969  seqf1oglem2  10970  bitsinv1lem  12744  dfphi2  13018  prmdiv  13033  odzdvds  13044  pc2dvds  13129  fldivp1  13147  pcfac  13149  1arith  13166  4sqlem10  13186  plyaddlem1  15897  plymullem1  15898  gausslemma2dlem4  16281  lgseisenlem1  16287  bj-peano4  17079