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  2534  nelneq2  2535  nelss  3523  dtru  4615  sofld  5303  card2inf  8079  gchen1  9057  gchen2  9058  bcpasc  12512  fiinfnf1o  12539  hashfn  12560  swrdnd2  12791  swrdccat  12851  pcprod  14839  lubval  16229  glbval  16242  mplmonmul  18687  regr1lem  20752  blcld  21518  stdbdxmet  21528  itgss  22767  isosctrlem2  23746  isppw2  24040  dchrelbas3  24164  lgsdir  24256  rplogsum  24363  nb3graprlem2  25178  orngsqr  28575  qqhval2lem  28793  qqhf  28798  esumpinfval  28902  bj-dtru  31382  poimirlem24  31928  isfldidl  32265  lssat  32551  paddasslem1  33354  lcfrlem21  35100  hdmap10lem  35379  hdmap11lem2  35382  jm2.23  35821  cncfiooicclem1  37711  fourierdlem81  37991  2f1fvneq  38877  nb3grprlem2  39215