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  2852  nelneq2  2853  nelss  4012  dtruALT2  5325  dtruOLD  5401  sofld  6160  card2inf  9508  gchen1  10578  gchen2  10579  bcpasc  14286  fiinfnf1o  14315  hashfn  14340  swrdnd2  14620  swrdccat  14700  nnoddn2prmb  16784  pcprod  16866  lubval  18315  glbval  18328  mplmonmul  21943  regr1lem  23626  blcld  24393  stdbdxmet  24403  itgss  25713  isosctrlem2  26729  isppw2  27025  dchrelbas3  27149  lgsdir  27243  2lgslem2  27306  2lgs  27318  rplogsum  27438  nb3grprlem2  29308  orngsqr  33282  qqhval2lem  33971  qqhf  33976  esumpinfval  34063  spthcycl  35116  lindsenlbs  37609  poimirlem24  37638  isfldidl  38062  lssat  39009  paddasslem1  39814  lcfrlem21  41557  hdmap10lem  41833  hdmap11lem2  41836  fsuppssind  42581  jm2.23  42985  ntrneiel2  44075  ntrneik4w  44089  cncfiooicclem1  45891  fourierdlem81  46185