Theorem con3dimp 414

Description: Variant of con3d 153 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 153	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	imp 412	1 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  stoic1a  1805  nelneq  2890  nelneq2  2891  nelss  4006  dtruALT2  5346  sofld  6190  card2inf  9527  elirrvOLD  9570  gchen1  10628  gchen2  10629  bcpasc  14377  fiinfnf1o  14406  hashfn  14431  swrdnd2  14717  swrdccat  14796  nnoddn2prmb  16898  pcprod  16980  lubval  18435  glbval  18448  orngsqr  21006  mplmonmul  22224  regr1lem  23933  blcld  24699  stdbdxmet  24709  itgss  26008  isosctrlem2  27021  isppw2  27316  dchrelbas3  27439  lgsdir  27533  2lgslem2  27596  2lgs  27608  rplogsum  27728  nb3grprlem2  29768  psrmonmul  33971  qqhval2lem  34402  qqhf  34407  esumpinfval  34494  spthcycl  35642  lindsenlbs  38307  poimirlem24  38336  isfldidl  38760  lssat  39831  paddasslem1  40635  lcfrlem21  42378  hdmap10lem  42654  hdmap11lem2  42657  fsuppssind  43366  jm2.23  43764  ntrneiel2  44853  ntrneik4w  44867  cncfiooicclem1  46648  fourierdlem81  46942