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  2544  nelneq2  2545  nelss  3427  dtru  4495  posn  4919  frsn  4921  relimasn  5204  sofld  5298  nssdmovg  6257  card2inf  7782  gchen1  8804  gchen2  8805  bcpasc  12109  fiinfnf1o  12133  hashfn  12150  hashdomi  12155  swrdvalodm2  12345  swrdvalodm  12346  swrdccat  12396  pcprod  13969  lubval  15166  glbval  15179  mplmonmul  17555  regr1lem  19324  blcld  20092  stdbdxmet  20102  iblss  21294  itgss  21301  isosctrlem2  22229  isppw2  22465  dchrelbas3  22589  lgsdir  22681  rplogsum  22788  nb3graprlem2  23372  xaddeq0  26058  xrge0npcan  26169  qqhval2lem  26422  qqhf  26427  esumpinfval  26534  hfext  28233  itg2addnclem2  28456  dvasin  28492  isfldidl  28880  jm2.23  29357  2f1fvneq  30155  bj-dtru  32330  lssat  32673  paddasslem1  33476  lcfrlem21  35220  hdmap10lem  35499  hdmap11lem2  35502