Theorem ord 731

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  817  orcanai  935  ax12  1560  swopo  4403  sotritrieq  4422  suc11g  4655  ordsoexmid  4660  nnsuc  4714  sotri2  5134  nnsucsssuc  6660  nntri2  6662  nntri1  6664  nnsseleq  6669  djulclb  7254  0ct  7306  exmidomniim  7340  omniwomnimkv  7366  elni2  7534  nlt1pig  7561  nngt1ne1  9178  zleloe  9526  zapne  9554  nneo  9583  zeo2  9586  fzocatel  10445  seqf1oglem1  10782  seqf1oglem2  10783  bitsinv1lem  12540  dfphi2  12810  prmdiv  12825  odzdvds  12836  pc2dvds  12921  fldivp1  12939  pcfac  12941  1arith  12958  4sqlem10  12978  plyaddlem1  15490  plymullem1  15491  gausslemma2dlem4  15812  lgseisenlem1  15818  bj-peano4  16601