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  4397  sotritrieq  4416  suc11g  4649  ordsoexmid  4654  nnsuc  4708  sotri2  5126  nnsucsssuc  6646  nntri2  6648  nntri1  6650  nnsseleq  6655  djulclb  7233  0ct  7285  exmidomniim  7319  omniwomnimkv  7345  elni2  7512  nlt1pig  7539  nngt1ne1  9156  zleloe  9504  zapne  9532  nneo  9561  zeo2  9564  fzocatel  10417  seqf1oglem1  10753  seqf1oglem2  10754  bitsinv1lem  12487  dfphi2  12757  prmdiv  12772  odzdvds  12783  pc2dvds  12868  fldivp1  12886  pcfac  12888  1arith  12905  4sqlem10  12925  plyaddlem1  15436  plymullem1  15437  gausslemma2dlem4  15758  lgseisenlem1  15764  bj-peano4  16373