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  4409  sotritrieq  4428  suc11g  4661  ordsoexmid  4666  nnsuc  4720  sotri2  5141  nnsucsssuc  6703  nntri2  6705  nntri1  6707  nnsseleq  6712  djulclb  7297  0ct  7349  exmidomniim  7383  omniwomnimkv  7409  elni2  7577  nlt1pig  7604  nngt1ne1  9220  zleloe  9570  zapne  9598  nneo  9627  zeo2  9630  fzocatel  10490  seqf1oglem1  10827  seqf1oglem2  10828  bitsinv1lem  12585  dfphi2  12855  prmdiv  12870  odzdvds  12881  pc2dvds  12966  fldivp1  12984  pcfac  12986  1arith  13003  4sqlem10  13023  plyaddlem1  15541  plymullem1  15542  gausslemma2dlem4  15866  lgseisenlem1  15872  bj-peano4  16654