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  4001  dtruALT2  5317  sofld  6153  card2inf  9472  elirrv  9514  gchen1  10548  gchen2  10549  bcpasc  14256  fiinfnf1o  14285  hashfn  14310  swrdnd2  14591  swrdccat  14670  nnoddn2prmb  16753  pcprod  16835  lubval  18289  glbval  18302  orngsqr  20811  mplmonmul  22003  regr1lem  23695  blcld  24461  stdbdxmet  24471  itgss  25781  isosctrlem2  26797  isppw2  27093  dchrelbas3  27217  lgsdir  27311  2lgslem2  27374  2lgs  27386  rplogsum  27506  nb3grprlem2  29466  psrmonmul  33726  qqhval2lem  34158  qqhf  34163  esumpinfval  34250  spthcycl  35342  lindsenlbs  37860  poimirlem24  37889  isfldidl  38313  lssat  39386  paddasslem1  40190  lcfrlem21  41933  hdmap10lem  42209  hdmap11lem2  42212  fsuppssind  42945  jm2.23  43347  ntrneiel2  44436  ntrneik4w  44450  cncfiooicclem1  46245  fourierdlem81  46539