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  2884  nelneq2  2885  nelss  3997  dtruALT2  5335  sofld  6180  card2inf  9527  elirrvOLD  9570  gchen1  10634  gchen2  10635  bcpasc  14385  fiinfnf1o  14414  hashfn  14439  swrdnd2  14725  swrdccat  14804  nnoddn2prmb  16905  pcprod  16987  lubval  18442  glbval  18455  orngsqr  21032  lindsenlbs  22064  mplmonmul  22252  regr1lem  23965  blcld  24731  stdbdxmet  24741  itgss  26039  isosctrlem2  27056  isppw2  27351  dchrelbas3  27474  lgsdir  27568  2lgslem2  27631  2lgs  27643  rplogsum  27763  nb3grprlem2  29841  spthcycl  30271  psrmonmul  34060  qqhval2lem  34491  qqhf  34496  esumpinfval  34583  poimirlem24  38393  isfldidl  38818  lssat  39889  paddasslem1  40693  lcfrlem21  42436  hdmap10lem  42712  hdmap11lem2  42715  fsuppssind  43439  jm2.23  43837  ntrneiel2  44926  ntrneik4w  44940  cncfiooicclem1  46721  fourierdlem81  47015