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  2885  nelneq2  2886  nelss  3997  dtruALT2  5332  sofld  6178  card2inf  9533  elirrvOLD  9576  gchen1  10691  gchen2  10692  bcpasc  14445  fiinfnf1o  14474  hashfn  14499  swrdnd2  14785  swrdccat  14864  nnoddn2prmb  16971  pcprod  17053  lubval  18508  glbval  18521  orngsqr  21103  lindsenlbs  22137  mplmonmul  22325  regr1lem  24038  blcld  24804  stdbdxmet  24814  itgss  26112  isosctrlem2  27129  isppw2  27424  dchrelbas3  27547  lgsdir  27641  2lgslem2  27704  2lgs  27716  rplogsum  27836  nb3grprlem2  29944  spthcycl  30374  psrmonmul  34164  qqhval2lem  34595  qqhf  34600  esumpinfval  34687  poimirlem24  38530  isfldidl  38970  lssat  40041  paddasslem1  40845  lcfrlem21  42588  hdmap10lem  42864  hdmap11lem2  42867  fsuppssind  43583  jm2.23  43956  ntrneiel2  45045  ntrneik4w  45059  cncfiooicclem1  46847  fourierdlem81  47141