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  1535  swopo  4353  sotritrieq  4372  suc11g  4605  ordsoexmid  4610  nnsuc  4664  sotri2  5080  nnsucsssuc  6578  nntri2  6580  nntri1  6582  nnsseleq  6587  djulclb  7157  0ct  7209  exmidomniim  7243  omniwomnimkv  7269  elni2  7427  nlt1pig  7454  nngt1ne1  9071  zleloe  9419  zapne  9447  nneo  9476  zeo2  9479  fzocatel  10328  seqf1oglem1  10664  seqf1oglem2  10665  bitsinv1lem  12272  dfphi2  12542  prmdiv  12557  odzdvds  12568  pc2dvds  12653  fldivp1  12671  pcfac  12673  1arith  12690  4sqlem10  12710  plyaddlem1  15219  plymullem1  15220  gausslemma2dlem4  15541  lgseisenlem1  15547  bj-peano4  15891