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  1770  nelneq  2868  nelneq2  2869  nelss  4074  dtruALT2  5388  dtruOLD  5461  sofld  6218  2f1fvneq  7297  card2inf  9624  gchen1  10694  gchen2  10695  bcpasc  14370  fiinfnf1o  14399  hashfn  14424  swrdnd2  14703  swrdccat  14783  nnoddn2prmb  16860  pcprod  16942  lubval  18426  glbval  18439  mplmonmul  22077  regr1lem  23768  blcld  24539  stdbdxmet  24549  itgss  25867  isosctrlem2  26880  isppw2  27176  dchrelbas3  27300  lgsdir  27394  2lgslem2  27457  2lgs  27469  rplogsum  27589  nb3grprlem2  29416  orngsqr  33299  qqhval2lem  33927  qqhf  33932  esumpinfval  34037  spthcycl  35097  lindsenlbs  37575  poimirlem24  37604  isfldidl  38028  lssat  38972  paddasslem1  39777  lcfrlem21  41520  hdmap10lem  41796  hdmap11lem2  41799  fsuppssind  42548  jm2.23  42953  ntrneiel2  44048  ntrneik4w  44062  cncfiooicclem1  45814  fourierdlem81  46108