Theorem con3dimp 414

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  stoic1a  1805  nelneq  2888  nelneq2  2889  nelss  3979  dtruALT2  5336  sofld  6191  card2inf  9576  elirrvOLD  9619  gchen1  10737  gchen2  10738  bcpasc  14492  fiinfnf1o  14521  hashfn  14546  swrdnd2  14833  swrdccat  14912  nnoddn2prmb  17020  pcprod  17102  lubval  18557  glbval  18570  orngsqr  21153  lindsenlbs  22187  mplmonmul  22375  regr1lem  24088  blcld  24854  stdbdxmet  24864  itgss  26162  isosctrlem2  27177  isppw2  27472  dchrelbas3  27595  lgsdir  27689  2lgslem2  27752  2lgs  27764  rplogsum  27884  nb3grprlem2  29992  spthcycl  30422  psrmonmul  34252  qqhval2lem  34683  qqhf  34688  esumpinfval  34775  poimirlem24  38754  isfldidl  39194  lssat  40265  paddasslem1  41069  lcfrlem21  42812  hdmap10lem  43088  hdmap11lem2  43091  fsuppssind  43814  jm2.23  44196  ntrneiel2  45278  ntrneik4w  45292  cncfiooicclem1  47108  fourierdlem81  47402