Theorem con3dimp 447

Description: Variant of con3d 140 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 140	. 2 |- ( ph -> ( -. ch -> -. ps ) )
3	2	imp 435	1 |- ( ( ph /\ -. ch ) -> -. ps )

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

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 190  df-an 377

This theorem is referenced by:  nelneq  2564  nelneq2  2565  nelss  3503  dtru  4611  sofld  5306  card2inf  8101  gchen1  9081  gchen2  9082  bcpasc  12544  fiinfnf1o  12571  hashfn  12592  swrdnd2  12832  swrdccat  12892  pcprod  14895  lubval  16285  glbval  16298  mplmonmul  18743  regr1lem  20809  blcld  21575  stdbdxmet  21585  itgss  22825  isosctrlem2  23804  isppw2  24098  dchrelbas3  24222  lgsdir  24314  rplogsum  24421  nb3graprlem2  25236  orngsqr  28618  qqhval2lem  28836  qqhf  28841  esumpinfval  28945  bj-dtru  31458  poimirlem24  32010  isfldidl  32347  lssat  32628  paddasslem1  33431  lcfrlem21  35177  hdmap10lem  35456  hdmap11lem2  35459  jm2.23  35897  cncfiooicclem1  37857  fourierdlem81  38152  2f1fvneq  39150  nb3grprlem2  39601