Theorem ord 642

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 640	. 2 ⊢ ((ψ ∨ χ) → (¬ ψ → χ))
3	1, 2	syl 14	1 ⊢ (φ → (¬ ψ → χ))

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in2 545  ax-io 629

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm2.8  722  orcanai  836  ax-12  1399  swopo  4033  sotritrieq  4052  suc11g  4234  ordsoexmid  4239  nnsuc  4280  sotri2  4664  nnsucsssuc  6003  nntri2  6005  nntri1  6006  elni2  6291  nlt1pig  6318  nngt1ne1  7680  zleloe  8018  zapne  8041  nneo  8066  zeo2  8069  fzocatel  8771  bj-peano4  9008