Theorem con3dimp 413

Description: Variant of con3d 153 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 153	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	imp 411	1 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)

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

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 210  df-an 401

This theorem is referenced by:  stoic1a  1802  nelneq  2887  nelneq2  2888  nelss  4004  dtruALT2  5343  sofld  6187  card2inf  9518  elirrvOLD  9561  gchen1  10611  gchen2  10612  bcpasc  14359  fiinfnf1o  14388  hashfn  14413  swrdnd2  14695  swrdccat  14774  nnoddn2prmb  16874  pcprod  16956  lubval  18411  glbval  18424  orngsqr  20950  mplmonmul  22168  regr1lem  23877  blcld  24643  stdbdxmet  24653  itgss  25952  isosctrlem2  26962  isppw2  27257  dchrelbas3  27380  lgsdir  27474  2lgslem2  27537  2lgs  27549  rplogsum  27669  nb3grprlem2  29709  psrmonmul  33918  qqhval2lem  34349  qqhf  34354  esumpinfval  34441  spthcycl  35599  lindsenlbs  38244  poimirlem24  38273  isfldidl  38697  lssat  39768  paddasslem1  40572  lcfrlem21  42315  hdmap10lem  42591  hdmap11lem2  42594  fsuppssind  43305  jm2.23  43703  ntrneiel2  44792  ntrneik4w  44806  cncfiooicclem1  46587  fourierdlem81  46881