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  2865  nelneq2  2866  nelss  4049  dtruALT2  5370  dtruOLD  5446  sofld  6207  2f1fvneq  7280  card2inf  9595  gchen1  10665  gchen2  10666  bcpasc  14360  fiinfnf1o  14389  hashfn  14414  swrdnd2  14693  swrdccat  14773  nnoddn2prmb  16851  pcprod  16933  lubval  18401  glbval  18414  mplmonmul  22054  regr1lem  23747  blcld  24518  stdbdxmet  24528  itgss  25847  isosctrlem2  26862  isppw2  27158  dchrelbas3  27282  lgsdir  27376  2lgslem2  27439  2lgs  27451  rplogsum  27571  nb3grprlem2  29398  orngsqr  33334  qqhval2lem  33982  qqhf  33987  esumpinfval  34074  spthcycl  35134  lindsenlbs  37622  poimirlem24  37651  isfldidl  38075  lssat  39017  paddasslem1  39822  lcfrlem21  41565  hdmap10lem  41841  hdmap11lem2  41844  fsuppssind  42603  jm2.23  43008  ntrneiel2  44099  ntrneik4w  44113  cncfiooicclem1  45908  fourierdlem81  46202