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  1772  nelneq  2852  nelneq2  2853  nelss  4003  dtruALT2  5312  dtruOLD  5388  sofld  6140  card2inf  9466  elirrv  9508  gchen1  10538  gchen2  10539  bcpasc  14246  fiinfnf1o  14275  hashfn  14300  swrdnd2  14580  swrdccat  14659  nnoddn2prmb  16743  pcprod  16825  lubval  18278  glbval  18291  orngsqr  20769  mplmonmul  21959  regr1lem  23642  blcld  24409  stdbdxmet  24419  itgss  25729  isosctrlem2  26745  isppw2  27041  dchrelbas3  27165  lgsdir  27259  2lgslem2  27322  2lgs  27334  rplogsum  27454  nb3grprlem2  29344  qqhval2lem  33947  qqhf  33952  esumpinfval  34039  spthcycl  35101  lindsenlbs  37594  poimirlem24  37623  isfldidl  38047  lssat  38994  paddasslem1  39799  lcfrlem21  41542  hdmap10lem  41818  hdmap11lem2  41821  fsuppssind  42566  jm2.23  42969  ntrneiel2  44059  ntrneik4w  44073  cncfiooicclem1  45875  fourierdlem81  46169