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  4401  sotritrieq  4420  suc11g  4653  ordsoexmid  4658  nnsuc  4712  sotri2  5132  nnsucsssuc  6655  nntri2  6657  nntri1  6659  nnsseleq  6664  djulclb  7245  0ct  7297  exmidomniim  7331  omniwomnimkv  7357  elni2  7524  nlt1pig  7551  nngt1ne1  9168  zleloe  9516  zapne  9544  nneo  9573  zeo2  9576  fzocatel  10434  seqf1oglem1  10771  seqf1oglem2  10772  bitsinv1lem  12512  dfphi2  12782  prmdiv  12797  odzdvds  12808  pc2dvds  12893  fldivp1  12911  pcfac  12913  1arith  12930  4sqlem10  12950  plyaddlem1  15461  plymullem1  15462  gausslemma2dlem4  15783  lgseisenlem1  15789  bj-peano4  16486