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  4034  sotritrieq  4053  suc11g  4235  ordsoexmid  4240  nnsuc  4281  sotri2  4665  nnsucsssuc  6010  nntri2  6012  nntri1  6013  elni2  6298  nlt1pig  6325  nngt1ne1  7709  zleloe  8048  zapne  8071  nneo  8097  zeo2  8100  fzocatel  8805  bj-peano4  9389