Theorem con3dimp 398

Description: Variant of con3d 150 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 150	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	imp 396	1 ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)

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

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 199  df-an 386

This theorem is referenced by:  stoic1a  1868  nelneq  2900  nelneq2  2901  nelss  3858  dtru  5038  sofld  5796  2f1fvneq  6743  card2inf  8700  gchen1  9733  gchen2  9734  bcpasc  13357  fiinfnf1o  13386  hashfn  13410  swrdnd2  13681  swrdccat  13796  swrdccatOLD  13797  nnoddn2prmb  15848  pcprod  15929  lubval  17296  glbval  17309  mplmonmul  19784  regr1lem  21868  blcld  22635  stdbdxmet  22645  itgss  23916  isosctrlem2  24898  isppw2  25190  dchrelbas3  25312  lgsdir  25406  2lgslem2  25469  2lgs  25481  rplogsum  25565  nb3grprlem2  26617  orngsqr  30312  qqhval2lem  30533  qqhf  30538  esumpinfval  30643  bj-dtru  33285  lindsenlbs  33885  poimirlem24  33914  isfldidl  34346  lssat  35029  paddasslem1  35833  lcfrlem21  37576  hdmap10lem  37852  hdmap11lem2  37855  jm2.23  38336  ntrneiel2  39154  ntrneik4w  39168  cncfiooicclem1  40838  fourierdlem81  41135