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  1769  nelneq  2937  nelneq2  2938  nelss  4029  eldifsnneqOLD  4717  dtru  5263  sofld  6038  2f1fvneq  7012  card2inf  9013  gchen1  10041  gchen2  10042  bcpasc  13675  fiinfnf1o  13704  hashfn  13730  swrdnd2  14011  swrdccat  14091  nnoddn2prmb  16144  pcprod  16225  lubval  17588  glbval  17601  mplmonmul  20239  regr1lem  22341  blcld  23109  stdbdxmet  23119  itgss  24406  isosctrlem2  25391  isppw2  25686  dchrelbas3  25808  lgsdir  25902  2lgslem2  25965  2lgs  25977  rplogsum  26097  nb3grprlem2  27157  orngsqr  30872  qqhval2lem  31217  qqhf  31222  esumpinfval  31327  spthcycl  32371  bj-dtru  34134  lindsenlbs  34881  poimirlem24  34910  isfldidl  35340  lssat  36146  paddasslem1  36950  lcfrlem21  38693  hdmap10lem  38969  hdmap11lem2  38972  jm2.23  39586  ntrneiel2  40429  ntrneik4w  40443  cncfiooicclem1  42169  fourierdlem81  42466