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  7398  nlt1pig  7425  nngt1ne1  9042  zleloe  9390  zapne  9417  nneo  9446  zeo2  9449  fzocatel  10292  seqf1oglem1  10628  seqf1oglem2  10629  bitsinv1lem  12143  dfphi2  12413  prmdiv  12428  odzdvds  12439  pc2dvds  12524  fldivp1  12542  pcfac  12544  1arith  12561  4sqlem10  12581  plyaddlem1  15067  plymullem1  15068  gausslemma2dlem4  15389  lgseisenlem1  15395  bj-peano4  15685