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  1795  nelneq  2889  nelneq2  2890  nelss  4005  dtruALT2  5332  sofld  6177  card2inf  9505  elirrvOLD  9548  gchen1  10598  gchen2  10599  bcpasc  14348  fiinfnf1o  14377  hashfn  14402  swrdnd2  14683  swrdccat  14762  nnoddn2prmb  16863  pcprod  16945  lubval  18400  glbval  18413  orngsqr  20938  mplmonmul  22147  regr1lem  23857  blcld  24623  stdbdxmet  24633  itgss  25932  isosctrlem2  26942  isppw2  27237  dchrelbas3  27360  lgsdir  27454  2lgslem2  27517  2lgs  27529  rplogsum  27649  nb3grprlem2  29640  psrmonmul  33857  qqhval2lem  34288  qqhf  34293  esumpinfval  34380  spthcycl  35492  lindsenlbs  38126  poimirlem24  38155  isfldidl  38579  lssat  39652  paddasslem1  40456  lcfrlem21  42199  hdmap10lem  42475  hdmap11lem2  42478  fsuppssind  43187  jm2.23  43585  ntrneiel2  44674  ntrneik4w  44688  cncfiooicclem1  46465  fourierdlem81  46759