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  1773  nelneq  2860  nelneq2  2861  nelss  3999  dtruALT2  5315  sofld  6145  card2inf  9460  elirrv  9502  gchen1  10536  gchen2  10537  bcpasc  14244  fiinfnf1o  14273  hashfn  14298  swrdnd2  14579  swrdccat  14658  nnoddn2prmb  16741  pcprod  16823  lubval  18277  glbval  18290  orngsqr  20799  mplmonmul  21991  regr1lem  23683  blcld  24449  stdbdxmet  24459  itgss  25769  isosctrlem2  26785  isppw2  27081  dchrelbas3  27205  lgsdir  27299  2lgslem2  27362  2lgs  27374  rplogsum  27494  nb3grprlem2  29454  qqhval2lem  34138  qqhf  34143  esumpinfval  34230  spthcycl  35323  lindsenlbs  37812  poimirlem24  37841  isfldidl  38265  lssat  39272  paddasslem1  40076  lcfrlem21  41819  hdmap10lem  42095  hdmap11lem2  42098  fsuppssind  42832  jm2.23  43234  ntrneiel2  44323  ntrneik4w  44337  cncfiooicclem1  46133  fourierdlem81  46427