Theorem ord 731

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 715

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 620  ax-io 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.8  817  orcanai  935  ax12  1560  swopo  4403  sotritrieq  4422  suc11g  4655  ordsoexmid  4660  nnsuc  4714  sotri2  5134  nnsucsssuc  6659  nntri2  6661  nntri1  6663  nnsseleq  6668  djulclb  7253  0ct  7305  exmidomniim  7339  omniwomnimkv  7365  elni2  7533  nlt1pig  7560  nngt1ne1  9177  zleloe  9525  zapne  9553  nneo  9582  zeo2  9585  fzocatel  10443  seqf1oglem1  10780  seqf1oglem2  10781  bitsinv1lem  12521  dfphi2  12791  prmdiv  12806  odzdvds  12817  pc2dvds  12902  fldivp1  12920  pcfac  12922  1arith  12939  4sqlem10  12959  plyaddlem1  15470  plymullem1  15471  gausslemma2dlem4  15792  lgseisenlem1  15798  bj-peano4  16550