Theorem ord 732

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

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

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 620  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  818  orcanai  936  ax12  1561  swopo  4432  sotritrieq  4451  suc11g  4684  ordsoexmid  4689  nnsuc  4743  sotri2  5165  nnsucsssuc  6738  nntri2  6740  nntri1  6742  nnsseleq  6747  djulclb  7359  0ct  7411  exmidomniim  7445  omniwomnimkv  7471  elni2  7645  nlt1pig  7672  nngt1ne1  9289  zleloe  9641  zapne  9669  nneo  9699  zeo2  9702  fzocatel  10566  seqf1oglem1  10905  seqf1oglem2  10906  bitsinv1lem  12672  dfphi2  12942  prmdiv  12957  odzdvds  12968  pc2dvds  13053  fldivp1  13071  pcfac  13073  1arith  13090  4sqlem10  13110  plyaddlem1  15738  plymullem1  15739  gausslemma2dlem4  16063  lgseisenlem1  16069  bj-peano4  16851