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  4453  sotritrieq  4472  suc11g  4706  ordsoexmid  4711  nnsuc  4765  sotri2  5188  nnsucsssuc  6770  nntri2  6772  nntri1  6774  nnsseleq  6779  djulclb  7401  0ct  7453  exmidomniim  7487  omniwomnimkv  7513  elni2  7687  nlt1pig  7714  nngt1ne1  9348  zleloe  9700  zapne  9728  nneo  9759  zeo2  9762  fzocatel  10633  seqf1oglem1  10976  seqf1oglem2  10977  bitsinv1lem  12752  dfphi2  13026  prmdiv  13041  odzdvds  13052  pc2dvds  13137  fldivp1  13155  pcfac  13157  1arith  13174  4sqlem10  13194  plyaddlem1  15990  plymullem1  15991  gausslemma2dlem4  16405  lgseisenlem1  16411  bj-peano4  17203