Theorem con3dimp 411

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

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

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 399

This theorem is referenced by:  stoic1a  1773  nelneq  2937  nelneq2  2938  nelss  4030  eldifsnneqOLD  4724  dtru  5271  sofld  6044  2f1fvneq  7018  card2inf  9019  gchen1  10047  gchen2  10048  bcpasc  13682  fiinfnf1o  13711  hashfn  13737  swrdnd2  14017  swrdccat  14097  nnoddn2prmb  16150  pcprod  16231  lubval  17594  glbval  17607  mplmonmul  20245  regr1lem  22347  blcld  23115  stdbdxmet  23125  itgss  24412  isosctrlem2  25397  isppw2  25692  dchrelbas3  25814  lgsdir  25908  2lgslem2  25971  2lgs  25983  rplogsum  26103  nb3grprlem2  27163  orngsqr  30877  qqhval2lem  31222  qqhf  31227  esumpinfval  31332  spthcycl  32376  bj-dtru  34139  lindsenlbs  34902  poimirlem24  34931  isfldidl  35361  lssat  36167  paddasslem1  36971  lcfrlem21  38714  hdmap10lem  38990  hdmap11lem2  38993  jm2.23  39613  ntrneiel2  40456  ntrneik4w  40470  cncfiooicclem1  42196  fourierdlem81  42492