Theorem con3dimp 408

Description: Variant of con3d 152 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
con3dimp.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
con3dimp	⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)

Proof of Theorem con3dimp

Step	Hyp	Ref	Expression
1		con3dimp.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	con3d 152	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	imp 406	1 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  stoic1a  1773  nelneq  2855  nelneq2  2856  nelss  4000  dtruALT2  5308  sofld  6134  card2inf  9441  elirrv  9483  gchen1  10513  gchen2  10514  bcpasc  14225  fiinfnf1o  14254  hashfn  14279  swrdnd2  14560  swrdccat  14639  nnoddn2prmb  16722  pcprod  16804  lubval  18257  glbval  18270  orngsqr  20779  mplmonmul  21969  regr1lem  23652  blcld  24418  stdbdxmet  24428  itgss  25738  isosctrlem2  26754  isppw2  27050  dchrelbas3  27174  lgsdir  27268  2lgslem2  27331  2lgs  27343  rplogsum  27463  nb3grprlem2  29357  qqhval2lem  33989  qqhf  33994  esumpinfval  34081  spthcycl  35161  lindsenlbs  37654  poimirlem24  37683  isfldidl  38107  lssat  39054  paddasslem1  39858  lcfrlem21  41601  hdmap10lem  41877  hdmap11lem2  41880  fsuppssind  42625  jm2.23  43028  ntrneiel2  44118  ntrneik4w  44132  cncfiooicclem1  45930  fourierdlem81  46224