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  2886  nelneq2  2887  nelss  4000  dtruALT2  5339  sofld  6184  card2inf  9531  elirrvOLD  9574  gchen1  10638  gchen2  10639  bcpasc  14389  fiinfnf1o  14418  hashfn  14443  swrdnd2  14729  swrdccat  14808  nnoddn2prmb  16911  pcprod  16993  lubval  18448  glbval  18461  orngsqr  21038  lindsenlbs  22070  mplmonmul  22258  regr1lem  23971  blcld  24737  stdbdxmet  24747  itgss  26046  isosctrlem2  27064  isppw2  27359  dchrelbas3  27482  lgsdir  27576  2lgslem2  27639  2lgs  27651  rplogsum  27771  nb3grprlem2  29849  spthcycl  30279  psrmonmul  34068  qqhval2lem  34499  qqhf  34504  esumpinfval  34591  poimirlem24  38401  isfldidl  38826  lssat  39897  paddasslem1  40701  lcfrlem21  42444  hdmap10lem  42720  hdmap11lem2  42723  fsuppssind  43447  jm2.23  43845  ntrneiel2  44934  ntrneik4w  44948  cncfiooicclem1  46729  fourierdlem81  47023