Theorem con3dimp 407

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 405	1 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)

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

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 206  df-an 395

This theorem is referenced by:  stoic1a  1766  nelneq  2849  nelneq2  2850  nelss  4043  dtruALT2  5369  dtruOLD  5442  sofld  6191  2f1fvneq  7268  card2inf  9578  gchen1  10648  gchen2  10649  bcpasc  14312  fiinfnf1o  14341  hashfn  14366  swrdnd2  14637  swrdccat  14717  nnoddn2prmb  16781  pcprod  16863  lubval  18347  glbval  18360  mplmonmul  21981  regr1lem  23673  blcld  24444  stdbdxmet  24454  itgss  25771  isosctrlem2  26781  isppw2  27077  dchrelbas3  27201  lgsdir  27295  2lgslem2  27358  2lgs  27370  rplogsum  27490  nb3grprlem2  29250  orngsqr  33079  qqhval2lem  33652  qqhf  33657  esumpinfval  33762  spthcycl  34809  lindsenlbs  37158  poimirlem24  37187  isfldidl  37611  lssat  38557  paddasslem1  39362  lcfrlem21  41105  hdmap10lem  41381  hdmap11lem2  41384  fsuppssind  41891  jm2.23  42482  ntrneiel2  43581  ntrneik4w  43595  cncfiooicclem1  45344  fourierdlem81  45638