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  1772  nelneq  2853  nelneq2  2854  nelss  4014  dtruALT2  5327  dtruOLD  5403  sofld  6162  card2inf  9514  gchen1  10584  gchen2  10585  bcpasc  14292  fiinfnf1o  14321  hashfn  14346  swrdnd2  14626  swrdccat  14706  nnoddn2prmb  16790  pcprod  16872  lubval  18321  glbval  18334  mplmonmul  21949  regr1lem  23632  blcld  24399  stdbdxmet  24409  itgss  25719  isosctrlem2  26735  isppw2  27031  dchrelbas3  27155  lgsdir  27249  2lgslem2  27312  2lgs  27324  rplogsum  27444  nb3grprlem2  29314  orngsqr  33288  qqhval2lem  33977  qqhf  33982  esumpinfval  34069  spthcycl  35116  lindsenlbs  37604  poimirlem24  37633  isfldidl  38057  lssat  39004  paddasslem1  39809  lcfrlem21  41552  hdmap10lem  41828  hdmap11lem2  41831  fsuppssind  42574  jm2.23  42978  ntrneiel2  44068  ntrneik4w  44082  cncfiooicclem1  45884  fourierdlem81  46178