Theorem ord 725

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 616  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  811  orcanai  929  ax12  1534  swopo  4352  sotritrieq  4371  suc11g  4604  ordsoexmid  4609  nnsuc  4663  sotri2  5079  nnsucsssuc  6577  nntri2  6579  nntri1  6581  nnsseleq  6586  djulclb  7156  0ct  7208  exmidomniim  7242  omniwomnimkv  7268  elni2  7426  nlt1pig  7453  nngt1ne1  9070  zleloe  9418  zapne  9446  nneo  9475  zeo2  9478  fzocatel  10326  seqf1oglem1  10662  seqf1oglem2  10663  bitsinv1lem  12243  dfphi2  12513  prmdiv  12528  odzdvds  12539  pc2dvds  12624  fldivp1  12642  pcfac  12644  1arith  12661  4sqlem10  12681  plyaddlem1  15190  plymullem1  15191  gausslemma2dlem4  15512  lgseisenlem1  15518  bj-peano4  15853