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  1523  swopo  4337  sotritrieq  4356  suc11g  4589  ordsoexmid  4594  nnsuc  4648  sotri2  5063  nnsucsssuc  6545  nntri2  6547  nntri1  6549  nnsseleq  6554  djulclb  7114  0ct  7166  exmidomniim  7200  omniwomnimkv  7226  elni2  7374  nlt1pig  7401  nngt1ne1  9017  zleloe  9364  zapne  9391  nneo  9420  zeo2  9423  fzocatel  10266  seqf1oglem1  10590  seqf1oglem2  10591  dfphi2  12358  prmdiv  12373  odzdvds  12383  pc2dvds  12468  fldivp1  12486  pcfac  12488  1arith  12505  4sqlem10  12525  plyaddlem1  14893  plymullem1  14894  gausslemma2dlem4  15180  lgseisenlem1  15186  bj-peano4  15447