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  2574  nelneq2  2575  nelss  3558  dtru  4647  sofld  5461  card2inf  7999  gchen1  9020  gchen2  9021  bcpasc  12402  fiinfnf1o  12426  hashfn  12446  swrdnd2  12669  swrdccat  12730  pcprod  14426  lubval  15741  glbval  15754  mplmonmul  18253  regr1lem  20366  blcld  21134  stdbdxmet  21144  itgss  22344  isosctrlem2  23279  isppw2  23515  dchrelbas3  23639  lgsdir  23731  rplogsum  23838  nb3graprlem2  24579  orngsqr  27955  qqhval2lem  28123  qqhf  28128  esumpinfval  28245  isfldidl  30670  jm2.23  31142  cncfiooicclem1  31899  fourierdlem81  32173  2f1fvneq  32571  bj-dtru  34526  lssat  34884  paddasslem1  35687  lcfrlem21  37433  hdmap10lem  37712  hdmap11lem2  37715