Theorem con3dimp 409

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

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

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 208  df-an 397

This theorem is referenced by:  stoic1a  1779  nelneq  2864  nelneq2  2865  nelss  3987  dtruALT2  5306  sofld  6145  card2inf  9467  elirrvOLD  9510  gchen1  10546  gchen2  10547  bcpasc  14281  fiinfnf1o  14310  hashfn  14335  swrdnd2  14616  swrdccat  14695  nnoddn2prmb  16782  pcprod  16864  lubval  18318  glbval  18331  orngsqr  20845  mplmonmul  22019  regr1lem  23729  blcld  24495  stdbdxmet  24505  itgss  25804  isosctrlem2  26808  isppw2  27103  dchrelbas3  27226  lgsdir  27320  2lgslem2  27383  2lgs  27395  rplogsum  27515  nb3grprlem2  29475  psrmonmul  33741  qqhval2lem  34172  qqhf  34177  esumpinfval  34264  spthcycl  35364  lindsenlbs  37989  poimirlem24  38018  isfldidl  38442  lssat  39515  paddasslem1  40319  lcfrlem21  42062  hdmap10lem  42338  hdmap11lem2  42341  fsuppssind  43050  jm2.23  43448  ntrneiel2  44537  ntrneik4w  44551  cncfiooicclem1  46343  fourierdlem81  46637