Theorem con3dimp 441

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

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

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 185  df-an 371

This theorem is referenced by:  nelneq  2584  nelneq2  2585  nelss  3563  dtru  4638  posn  5068  frsn  5070  relimasn  5360  sofld  5455  nssdmovg  6442  card2inf  7982  gchen1  9004  gchen2  9005  bcpasc  12368  fiinfnf1o  12392  hashfn  12412  hashdomi  12417  swrdvalodm2  12630  swrdvalodm  12631  swrdccat  12684  pcprod  14276  lubval  15474  glbval  15487  mplmonmul  17937  regr1lem  20067  blcld  20835  stdbdxmet  20845  iblss  22038  itgss  22045  isosctrlem2  22978  isppw2  23214  dchrelbas3  23338  lgsdir  23430  rplogsum  23537  nb3graprlem2  24225  xaddeq0  27338  xrge0npcan  27443  qqhval2lem  27713  qqhf  27718  esumpinfval  27830  hfext  29693  itg2addnclem2  29920  dvasin  29956  isfldidl  30295  jm2.23  30769  icccncfext  31453  cncfiooicclem1  31459  dirkercncflem1  31630  fourierdlem65  31699  fourierdlem81  31715  fourierdlem97  31731  2f1fvneq  32001  bj-dtru  33681  lssat  34030  paddasslem1  34833  lcfrlem21  36577  hdmap10lem  36856  hdmap11lem2  36859