Theorem ord 726

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

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

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  812  orcanai  930  ax12  1536  swopo  4371  sotritrieq  4390  suc11g  4623  ordsoexmid  4628  nnsuc  4682  sotri2  5099  nnsucsssuc  6601  nntri2  6603  nntri1  6605  nnsseleq  6610  djulclb  7183  0ct  7235  exmidomniim  7269  omniwomnimkv  7295  elni2  7462  nlt1pig  7489  nngt1ne1  9106  zleloe  9454  zapne  9482  nneo  9511  zeo2  9514  fzocatel  10365  seqf1oglem1  10701  seqf1oglem2  10702  bitsinv1lem  12387  dfphi2  12657  prmdiv  12672  odzdvds  12683  pc2dvds  12768  fldivp1  12786  pcfac  12788  1arith  12805  4sqlem10  12825  plyaddlem1  15334  plymullem1  15335  gausslemma2dlem4  15656  lgseisenlem1  15662  bj-peano4  16090