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  4338  sotritrieq  4357  suc11g  4590  ordsoexmid  4595  nnsuc  4649  sotri2  5064  nnsucsssuc  6547  nntri2  6549  nntri1  6551  nnsseleq  6556  djulclb  7116  0ct  7168  exmidomniim  7202  omniwomnimkv  7228  elni2  7376  nlt1pig  7403  nngt1ne1  9019  zleloe  9367  zapne  9394  nneo  9423  zeo2  9426  fzocatel  10269  seqf1oglem1  10593  seqf1oglem2  10594  dfphi2  12361  prmdiv  12376  odzdvds  12386  pc2dvds  12471  fldivp1  12489  pcfac  12491  1arith  12508  4sqlem10  12528  plyaddlem1  14926  plymullem1  14927  gausslemma2dlem4  15221  lgseisenlem1  15227  bj-peano4  15517