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  4427  sotritrieq  4446  suc11g  4679  ordsoexmid  4684  nnsuc  4738  sotri2  5160  nnsucsssuc  6725  nntri2  6727  nntri1  6729  nnsseleq  6734  djulclb  7346  0ct  7398  exmidomniim  7432  omniwomnimkv  7458  elni2  7629  nlt1pig  7656  nngt1ne1  9272  zleloe  9624  zapne  9652  nneo  9681  zeo2  9684  fzocatel  10544  seqf1oglem1  10881  seqf1oglem2  10882  bitsinv1lem  12647  dfphi2  12917  prmdiv  12932  odzdvds  12943  pc2dvds  13028  fldivp1  13046  pcfac  13048  1arith  13065  4sqlem10  13085  plyaddlem1  15612  plymullem1  15613  gausslemma2dlem4  15937  lgseisenlem1  15943  bj-peano4  16725