Theorem ord 729

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

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

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 618  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  815  orcanai  933  ax12  1558  swopo  4396  sotritrieq  4415  suc11g  4648  ordsoexmid  4653  nnsuc  4707  sotri2  5125  nnsucsssuc  6636  nntri2  6638  nntri1  6640  nnsseleq  6645  djulclb  7218  0ct  7270  exmidomniim  7304  omniwomnimkv  7330  elni2  7497  nlt1pig  7524  nngt1ne1  9141  zleloe  9489  zapne  9517  nneo  9546  zeo2  9549  fzocatel  10400  seqf1oglem1  10736  seqf1oglem2  10737  bitsinv1lem  12467  dfphi2  12737  prmdiv  12752  odzdvds  12763  pc2dvds  12848  fldivp1  12866  pcfac  12868  1arith  12885  4sqlem10  12905  plyaddlem1  15415  plymullem1  15416  gausslemma2dlem4  15737  lgseisenlem1  15743  bj-peano4  16276