Theorem con3dimp 410

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

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

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 206  df-an 398

This theorem is referenced by:  stoic1a  1774  nelneq  2862  nelneq2  2863  nelss  3999  dtruALT2  5318  dtruOLD  5391  sofld  6130  2f1fvneq  7194  card2inf  9417  gchen1  10487  gchen2  10488  bcpasc  14141  fiinfnf1o  14170  hashfn  14195  swrdnd2  14467  swrdccat  14547  nnoddn2prmb  16612  pcprod  16694  lubval  18172  glbval  18185  mplmonmul  21343  regr1lem  22996  blcld  23767  stdbdxmet  23777  itgss  25082  isosctrlem2  26075  isppw2  26370  dchrelbas3  26492  lgsdir  26586  2lgslem2  26649  2lgs  26661  rplogsum  26781  nb3grprlem2  28037  orngsqr  31801  qqhval2lem  32227  qqhf  32232  esumpinfval  32337  spthcycl  33388  lindsenlbs  35926  poimirlem24  35955  isfldidl  36380  lssat  37332  paddasslem1  38137  lcfrlem21  39880  hdmap10lem  40156  hdmap11lem2  40159  fsuppssind  40591  jm2.23  41130  ntrneiel2  42067  ntrneik4w  42081  cncfiooicclem1  43820  fourierdlem81  44114