Theorem con3dimp 442

Description: Variant of con3d 138 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
con3dimp.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
con3dimp	|- ( ( ph /\ -. ch ) -> -. ps )

Proof of Theorem con3dimp

Step	Hyp	Ref	Expression
1		con3dimp.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	con3d 138	. 2 |- ( ph -> ( -. ch -> -. ps ) )
3	2	imp 430	1 |- ( ( ph /\ -. ch ) -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  nelneq  2546  nelneq2  2547  nelss  3529  dtru  4616  sofld  5304  card2inf  8070  gchen1  9049  gchen2  9050  bcpasc  12503  fiinfnf1o  12530  hashfn  12551  swrdnd2  12774  swrdccat  12834  pcprod  14803  lubval  16181  glbval  16194  mplmonmul  18623  regr1lem  20685  blcld  21451  stdbdxmet  21461  itgss  22646  isosctrlem2  23613  isppw2  23905  dchrelbas3  24029  lgsdir  24121  rplogsum  24228  nb3graprlem2  25025  orngsqr  28406  qqhval2lem  28624  qqhf  28629  esumpinfval  28733  bj-dtru  31163  poimirlem24  31667  isfldidl  32004  lssat  32290  paddasslem1  33093  lcfrlem21  34839  hdmap10lem  35118  hdmap11lem2  35121  jm2.23  35556  cncfiooicclem1  37342  fourierdlem81  37618  2f1fvneq  38383