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  1774  nelneq  2857  nelneq2  2858  nelss  4046  dtruALT2  5367  dtruOLD  5440  sofld  6183  2f1fvneq  7255  card2inf  9546  gchen1  10616  gchen2  10617  bcpasc  14277  fiinfnf1o  14306  hashfn  14331  swrdnd2  14601  swrdccat  14681  nnoddn2prmb  16742  pcprod  16824  lubval  18305  glbval  18318  mplmonmul  21582  regr1lem  23234  blcld  24005  stdbdxmet  24015  itgss  25320  isosctrlem2  26313  isppw2  26608  dchrelbas3  26730  lgsdir  26824  2lgslem2  26887  2lgs  26899  rplogsum  27019  nb3grprlem2  28627  orngsqr  32410  qqhval2lem  32949  qqhf  32954  esumpinfval  33059  spthcycl  34108  lindsenlbs  36471  poimirlem24  36500  isfldidl  36924  lssat  37874  paddasslem1  38679  lcfrlem21  40422  hdmap10lem  40698  hdmap11lem2  40701  fsuppssind  41162  jm2.23  41720  ntrneiel2  42822  ntrneik4w  42836  cncfiooicclem1  44595  fourierdlem81  44889