Theorem con3dimp 408

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

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

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 207  df-an 396

This theorem is referenced by:  stoic1a  1773  nelneq  2857  nelneq2  2858  nelss  3996  dtruALT2  5310  sofld  6139  card2inf  9448  elirrv  9490  gchen1  10523  gchen2  10524  bcpasc  14230  fiinfnf1o  14259  hashfn  14284  swrdnd2  14565  swrdccat  14644  nnoddn2prmb  16727  pcprod  16809  lubval  18262  glbval  18275  orngsqr  20783  mplmonmul  21972  regr1lem  23655  blcld  24421  stdbdxmet  24431  itgss  25741  isosctrlem2  26757  isppw2  27053  dchrelbas3  27177  lgsdir  27271  2lgslem2  27334  2lgs  27346  rplogsum  27466  nb3grprlem2  29361  qqhval2lem  34015  qqhf  34020  esumpinfval  34107  spthcycl  35194  lindsenlbs  37675  poimirlem24  37704  isfldidl  38128  lssat  39135  paddasslem1  39939  lcfrlem21  41682  hdmap10lem  41958  hdmap11lem2  41961  fsuppssind  42711  jm2.23  43113  ntrneiel2  44203  ntrneik4w  44217  cncfiooicclem1  46015  fourierdlem81  46309