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  1774  nelneq  2860  nelneq2  2861  nelss  3987  dtruALT2  5312  sofld  6151  card2inf  9470  elirrv  9512  gchen1  10548  gchen2  10549  bcpasc  14283  fiinfnf1o  14312  hashfn  14337  swrdnd2  14618  swrdccat  14697  nnoddn2prmb  16784  pcprod  16866  lubval  18320  glbval  18333  orngsqr  20843  mplmonmul  22014  regr1lem  23704  blcld  24470  stdbdxmet  24480  itgss  25779  isosctrlem2  26783  isppw2  27078  dchrelbas3  27201  lgsdir  27295  2lgslem2  27358  2lgs  27370  rplogsum  27490  nb3grprlem2  29450  psrmonmul  33694  qqhval2lem  34125  qqhf  34130  esumpinfval  34217  spthcycl  35311  lindsenlbs  37936  poimirlem24  37965  isfldidl  38389  lssat  39462  paddasslem1  40266  lcfrlem21  42009  hdmap10lem  42285  hdmap11lem2  42288  fsuppssind  43026  jm2.23  43424  ntrneiel2  44513  ntrneik4w  44527  cncfiooicclem1  46321  fourierdlem81  46615