Theorem ord 681

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 583  ax-io 668

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.8  762  orcanai  878  ax-12  1454  swopo  4157  sotritrieq  4176  suc11g  4401  ordsoexmid  4406  nnsuc  4458  sotri2  4862  nnsucsssuc  6293  nntri2  6295  nntri1  6297  nnsseleq  6302  djulclb  6827  0ct  6869  exmidomniim  6884  elni2  6970  nlt1pig  6997  nngt1ne1  8555  zleloe  8895  zapne  8919  nneo  8948  zeo2  8951  fzocatel  9759  dfphi2  11639  bj-peano4  12574