Theorem con3dimp 456

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

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

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 196  df-an 385

This theorem is referenced by:  stoic1a  1688  nelneq  2712  nelneq2  2713  nelss  3627  dtru  4783  sofld  5500  card2inf  8343  gchen1  9326  gchen2  9327  bcpasc  12970  fiinfnf1o  13000  hashfn  13025  swrdnd2  13285  swrdccat  13344  nnoddn2prmb  15356  pcprod  15437  lubval  16807  glbval  16820  mplmonmul  19285  regr1lem  21352  blcld  22120  stdbdxmet  22130  itgss  23384  isosctrlem2  24349  isppw2  24641  dchrelbas3  24763  lgsdir  24857  2lgslem2  24920  2lgs  24932  rplogsum  25016  nb3graprlem2  25981  orngsqr  29135  qqhval2lem  29353  qqhf  29358  esumpinfval  29462  bj-dtru  31985  lindsenlbs  32574  poimirlem24  32603  isfldidl  33037  lssat  33321  paddasslem1  34124  lcfrlem21  35870  hdmap10lem  36149  hdmap11lem2  36152  jm2.23  36581  ntrneiel2  37404  ntrneik4w  37418  cncfiooicclem1  38779  fourierdlem81  39080  2f1fvneq  40322  nb3grprlem2  40609