Theorem con3dimp 408

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

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

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 207  df-an 396

This theorem is referenced by:  stoic1a  1768  nelneq  2862  nelneq2  2863  nelss  4060  dtruALT2  5375  dtruOLD  5451  sofld  6208  2f1fvneq  7279  card2inf  9592  gchen1  10662  gchen2  10663  bcpasc  14356  fiinfnf1o  14385  hashfn  14410  swrdnd2  14689  swrdccat  14769  nnoddn2prmb  16846  pcprod  16928  lubval  18413  glbval  18426  mplmonmul  22071  regr1lem  23762  blcld  24533  stdbdxmet  24543  itgss  25861  isosctrlem2  26876  isppw2  27172  dchrelbas3  27296  lgsdir  27390  2lgslem2  27453  2lgs  27465  rplogsum  27585  nb3grprlem2  29412  orngsqr  33313  qqhval2lem  33943  qqhf  33948  esumpinfval  34053  spthcycl  35113  lindsenlbs  37601  poimirlem24  37630  isfldidl  38054  lssat  38997  paddasslem1  39802  lcfrlem21  41545  hdmap10lem  41821  hdmap11lem2  41824  fsuppssind  42579  jm2.23  42984  ntrneiel2  44075  ntrneik4w  44089  cncfiooicclem1  45848  fourierdlem81  46142