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

This theorem is referenced by:  stoic1a  1776  nelneq  2863  nelneq2  2864  nelss  3980  dtru  5288  sofld  6079  2f1fvneq  7114  card2inf  9244  gchen1  10312  gchen2  10313  bcpasc  13963  fiinfnf1o  13992  hashfn  14018  swrdnd2  14296  swrdccat  14376  nnoddn2prmb  16442  pcprod  16524  lubval  17989  glbval  18002  mplmonmul  21147  regr1lem  22798  blcld  23567  stdbdxmet  23577  itgss  24881  isosctrlem2  25874  isppw2  26169  dchrelbas3  26291  lgsdir  26385  2lgslem2  26448  2lgs  26460  rplogsum  26580  nb3grprlem2  27651  orngsqr  31405  qqhval2lem  31831  qqhf  31836  esumpinfval  31941  spthcycl  32991  bj-dtru  34926  lindsenlbs  35699  poimirlem24  35728  isfldidl  36153  lssat  36957  paddasslem1  37761  lcfrlem21  39504  hdmap10lem  39780  hdmap11lem2  39783  fsuppssind  40205  jm2.23  40734  ntrneiel2  41585  ntrneik4w  41599  cncfiooicclem1  43324  fourierdlem81  43618