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 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))

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

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 624  ax-io 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  822  orcanai  940  ax12  1565  swopo  4446  sotritrieq  4465  suc11g  4699  ordsoexmid  4704  nnsuc  4758  sotri2  5180  nnsucsssuc  6755  nntri2  6757  nntri1  6759  nnsseleq  6764  djulclb  7385  0ct  7437  exmidomniim  7471  omniwomnimkv  7497  elni2  7671  nlt1pig  7698  nngt1ne1  9318  zleloe  9670  zapne  9698  nneo  9728  zeo2  9731  fzocatel  10595  seqf1oglem1  10934  seqf1oglem2  10935  bitsinv1lem  12706  dfphi2  12976  prmdiv  12991  odzdvds  13002  pc2dvds  13087  fldivp1  13105  pcfac  13107  1arith  13124  4sqlem10  13144  plyaddlem1  15771  plymullem1  15772  gausslemma2dlem4  16097  lgseisenlem1  16103  bj-peano4  16895