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  1774  nelneq  2861  nelneq2  2862  nelss  3988  dtruALT2  5307  sofld  6145  card2inf  9463  elirrv  9505  gchen1  10539  gchen2  10540  bcpasc  14274  fiinfnf1o  14303  hashfn  14328  swrdnd2  14609  swrdccat  14688  nnoddn2prmb  16775  pcprod  16857  lubval  18311  glbval  18324  orngsqr  20834  mplmonmul  22024  regr1lem  23714  blcld  24480  stdbdxmet  24490  itgss  25789  isosctrlem2  26796  isppw2  27092  dchrelbas3  27215  lgsdir  27309  2lgslem2  27372  2lgs  27384  rplogsum  27504  nb3grprlem2  29464  psrmonmul  33709  qqhval2lem  34141  qqhf  34146  esumpinfval  34233  spthcycl  35327  lindsenlbs  37950  poimirlem24  37979  isfldidl  38403  lssat  39476  paddasslem1  40280  lcfrlem21  42023  hdmap10lem  42299  hdmap11lem2  42302  fsuppssind  43040  jm2.23  43442  ntrneiel2  44531  ntrneik4w  44545  cncfiooicclem1  46339  fourierdlem81  46633