Theorem con3dimp 414

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  stoic1a  1804  nelneq  2884  nelneq2  2885  nelss  3974  dtruALT2  5331  sofld  6178  card2inf  9552  elirrvOLD  9595  gchen1  10713  gchen2  10714  bcpasc  14468  fiinfnf1o  14497  hashfn  14522  swrdnd2  14809  swrdccat  14888  nnoddn2prmb  16996  pcprod  17078  lubval  18533  glbval  18546  orngsqr  21128  lindsenlbs  22162  mplmonmul  22350  regr1lem  24063  blcld  24829  stdbdxmet  24839  itgss  26137  isosctrlem2  27152  isppw2  27447  dchrelbas3  27570  lgsdir  27664  2lgslem2  27727  2lgs  27739  rplogsum  27859  nb3grprlem2  29967  spthcycl  30397  psrmonmul  34228  qqhval2lem  34659  qqhf  34664  esumpinfval  34751  poimirlem24  38655  isfldidl  39095  lssat  40166  paddasslem1  40970  lcfrlem21  42713  hdmap10lem  42989  hdmap11lem2  42992  fsuppssind  43714  jm2.23  44096  ntrneiel2  45179  ntrneik4w  45193  cncfiooicclem1  46996  fourierdlem81  47290