Theorem con3dimp 407

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

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

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 395

This theorem is referenced by:  stoic1a  1772  nelneq  2855  nelneq2  2856  nelss  4046  dtruALT2  5367  dtruOLD  5440  sofld  6185  2f1fvneq  7261  card2inf  9552  gchen1  10622  gchen2  10623  bcpasc  14285  fiinfnf1o  14314  hashfn  14339  swrdnd2  14609  swrdccat  14689  nnoddn2prmb  16750  pcprod  16832  lubval  18313  glbval  18326  mplmonmul  21810  regr1lem  23463  blcld  24234  stdbdxmet  24244  itgss  25561  isosctrlem2  26560  isppw2  26855  dchrelbas3  26977  lgsdir  27071  2lgslem2  27134  2lgs  27146  rplogsum  27266  nb3grprlem2  28905  orngsqr  32692  qqhval2lem  33259  qqhf  33264  esumpinfval  33369  spthcycl  34418  lindsenlbs  36786  poimirlem24  36815  isfldidl  37239  lssat  38189  paddasslem1  38994  lcfrlem21  40737  hdmap10lem  41013  hdmap11lem2  41016  fsuppssind  41467  jm2.23  42037  ntrneiel2  43139  ntrneik4w  43153  cncfiooicclem1  44907  fourierdlem81  45201