Theorem ord 725

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

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  811  orcanai  929  ax12  1523  swopo  4321  sotritrieq  4340  suc11g  4571  ordsoexmid  4576  nnsuc  4630  sotri2  5041  nnsucsssuc  6511  nntri2  6513  nntri1  6515  nnsseleq  6520  djulclb  7072  0ct  7124  exmidomniim  7157  omniwomnimkv  7183  elni2  7331  nlt1pig  7358  nngt1ne1  8972  zleloe  9318  zapne  9345  nneo  9374  zeo2  9377  fzocatel  10217  dfphi2  12238  prmdiv  12253  odzdvds  12263  pc2dvds  12347  fldivp1  12364  pcfac  12366  1arith  12383  4sqlem10  12403  lgseisenlem1  14847  bj-peano4  15104