Theorem ord 736

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm2.8  822  orcanai  940  ax12  1565  swopo  4451  sotritrieq  4470  suc11g  4704  ordsoexmid  4709  nnsuc  4763  sotri2  5185  nnsucsssuc  6765  nntri2  6767  nntri1  6769  nnsseleq  6774  djulclb  7396  0ct  7448  exmidomniim  7482  omniwomnimkv  7508  elni2  7682  nlt1pig  7709  nngt1ne1  9342  zleloe  9696  zapne  9724  nneo  9754  zeo2  9757  fzocatel  10628  seqf1oglem1  10971  seqf1oglem2  10972  bitsinv1lem  12747  dfphi2  13021  prmdiv  13036  odzdvds  13047  pc2dvds  13132  fldivp1  13150  pcfac  13152  1arith  13169  4sqlem10  13189  plyaddlem1  15939  plymullem1  15940  gausslemma2dlem4  16349  lgseisenlem1  16355  bj-peano4  17147