Theorem con3dimp 412

Description: Variant of con3d 155 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 155	. 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 210  df-an 400

This theorem is referenced by:  stoic1a  1774  nelneq  2914  nelneq2  2915  nelss  3978  dtru  5236  sofld  6011  2f1fvneq  6996  card2inf  9003  gchen1  10036  gchen2  10037  bcpasc  13677  fiinfnf1o  13706  hashfn  13732  swrdnd2  14008  swrdccat  14088  nnoddn2prmb  16140  pcprod  16221  lubval  17586  glbval  17599  mplmonmul  20704  regr1lem  22344  blcld  23112  stdbdxmet  23122  itgss  24415  isosctrlem2  25405  isppw2  25700  dchrelbas3  25822  lgsdir  25916  2lgslem2  25979  2lgs  25991  rplogsum  26111  nb3grprlem2  27171  orngsqr  30928  qqhval2lem  31332  qqhf  31337  esumpinfval  31442  spthcycl  32489  bj-dtru  34254  lindsenlbs  35052  poimirlem24  35081  isfldidl  35506  lssat  36312  paddasslem1  37116  lcfrlem21  38859  hdmap10lem  39135  hdmap11lem2  39138  fsuppssind  39459  jm2.23  39937  ntrneiel2  40789  ntrneik4w  40803  cncfiooicclem1  42535  fourierdlem81  42829