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  1772  nelneq  2858  nelneq2  2859  nelss  4024  dtruALT2  5340  dtruOLD  5416  sofld  6176  card2inf  9569  gchen1  10639  gchen2  10640  bcpasc  14339  fiinfnf1o  14368  hashfn  14393  swrdnd2  14673  swrdccat  14753  nnoddn2prmb  16833  pcprod  16915  lubval  18366  glbval  18379  mplmonmul  21994  regr1lem  23677  blcld  24444  stdbdxmet  24454  itgss  25765  isosctrlem2  26781  isppw2  27077  dchrelbas3  27201  lgsdir  27295  2lgslem2  27358  2lgs  27370  rplogsum  27490  nb3grprlem2  29360  orngsqr  33326  qqhval2lem  34012  qqhf  34017  esumpinfval  34104  spthcycl  35151  lindsenlbs  37639  poimirlem24  37668  isfldidl  38092  lssat  39034  paddasslem1  39839  lcfrlem21  41582  hdmap10lem  41858  hdmap11lem2  41861  fsuppssind  42616  jm2.23  43020  ntrneiel2  44110  ntrneik4w  44124  cncfiooicclem1  45922  fourierdlem81  46216