Theorem con3dimp 412

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 410	1 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  stoic1a  1791  nelneq  2885  nelneq2  2886  nelss  4002  dtruALT2  5326  sofld  6169  card2inf  9500  elirrvOLD  9543  gchen1  10580  gchen2  10581  bcpasc  14331  fiinfnf1o  14360  hashfn  14385  swrdnd2  14666  swrdccat  14745  nnoddn2prmb  16832  pcprod  16914  lubval  18369  glbval  18382  orngsqr  20895  mplmonmul  22069  regr1lem  23779  blcld  24545  stdbdxmet  24555  itgss  25854  isosctrlem2  26861  isppw2  27156  dchrelbas3  27279  lgsdir  27373  2lgslem2  27436  2lgs  27448  rplogsum  27568  nb3grprlem2  29528  psrmonmul  33808  qqhval2lem  34239  qqhf  34244  esumpinfval  34331  spthcycl  35443  lindsenlbs  38078  poimirlem24  38107  isfldidl  38531  lssat  39604  paddasslem1  40408  lcfrlem21  42151  hdmap10lem  42427  hdmap11lem2  42430  fsuppssind  43139  jm2.23  43537  ntrneiel2  44626  ntrneik4w  44640  cncfiooicclem1  46431  fourierdlem81  46725