Theorem con3dimp 399

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

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

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 199  df-an 387

This theorem is referenced by:  stoic1a  1816  nelneq  2883  nelneq2  2884  nelss  3883  dtru  5082  sofld  5835  2f1fvneq  6789  card2inf  8749  gchen1  9782  gchen2  9783  bcpasc  13426  fiinfnf1o  13455  hashfn  13479  swrdnd2  13750  swrdccat  13865  swrdccatOLD  13866  nnoddn2prmb  15922  pcprod  16003  lubval  17370  glbval  17383  mplmonmul  19861  regr1lem  21951  blcld  22718  stdbdxmet  22728  itgss  24015  isosctrlem2  24997  isppw2  25293  dchrelbas3  25415  lgsdir  25509  2lgslem2  25572  2lgs  25584  rplogsum  25668  nb3grprlem2  26729  orngsqr  30366  qqhval2lem  30623  qqhf  30628  esumpinfval  30733  bj-dtru  33373  eldifsnneq  33732  lindsenlbs  34030  poimirlem24  34059  isfldidl  34491  lssat  35170  paddasslem1  35974  lcfrlem21  37717  hdmap10lem  37993  hdmap11lem2  37996  jm2.23  38522  ntrneiel2  39340  ntrneik4w  39354  cncfiooicclem1  41034  fourierdlem81  41331