Theorem con3dimp 409

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

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

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 206  df-an 397

This theorem is referenced by:  stoic1a  1775  nelneq  2863  nelneq2  2864  nelss  3984  dtruALT2  5293  dtru  5359  sofld  6090  2f1fvneq  7133  card2inf  9314  gchen1  10381  gchen2  10382  bcpasc  14035  fiinfnf1o  14064  hashfn  14090  swrdnd2  14368  swrdccat  14448  nnoddn2prmb  16514  pcprod  16596  lubval  18074  glbval  18087  mplmonmul  21237  regr1lem  22890  blcld  23661  stdbdxmet  23671  itgss  24976  isosctrlem2  25969  isppw2  26264  dchrelbas3  26386  lgsdir  26480  2lgslem2  26543  2lgs  26555  rplogsum  26675  nb3grprlem2  27748  orngsqr  31503  qqhval2lem  31931  qqhf  31936  esumpinfval  32041  spthcycl  33091  bj-dtru  34999  lindsenlbs  35772  poimirlem24  35801  isfldidl  36226  lssat  37030  paddasslem1  37834  lcfrlem21  39577  hdmap10lem  39853  hdmap11lem2  39856  fsuppssind  40282  jm2.23  40818  ntrneiel2  41696  ntrneik4w  41710  cncfiooicclem1  43434  fourierdlem81  43728