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  1526  swopo  4342  sotritrieq  4361  suc11g  4594  ordsoexmid  4599  nnsuc  4653  sotri2  5068  nnsucsssuc  6559  nntri2  6561  nntri1  6563  nnsseleq  6568  djulclb  7130  0ct  7182  exmidomniim  7216  omniwomnimkv  7242  elni2  7400  nlt1pig  7427  nngt1ne1  9044  zleloe  9392  zapne  9419  nneo  9448  zeo2  9451  fzocatel  10294  seqf1oglem1  10630  seqf1oglem2  10631  bitsinv1lem  12145  dfphi2  12415  prmdiv  12430  odzdvds  12441  pc2dvds  12526  fldivp1  12544  pcfac  12546  1arith  12563  4sqlem10  12583  plyaddlem1  15091  plymullem1  15092  gausslemma2dlem4  15413  lgseisenlem1  15419  bj-peano4  15709