Theorem con3dimp 457

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

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

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 197  df-an 386

This theorem is referenced by:  stoic1a  1697  nelneq  2725  nelneq2  2726  nelss  3664  dtru  4857  sofld  5581  2f1fvneq  6517  card2inf  8460  gchen1  9447  gchen2  9448  bcpasc  13108  fiinfnf1o  13138  hashfn  13164  swrdnd2  13433  swrdccat  13493  nnoddn2prmb  15518  pcprod  15599  lubval  16984  glbval  16997  mplmonmul  19464  regr1lem  21542  blcld  22310  stdbdxmet  22320  itgss  23578  isosctrlem2  24549  isppw2  24841  dchrelbas3  24963  lgsdir  25057  2lgslem2  25120  2lgs  25132  rplogsum  25216  nb3grprlem2  26283  orngsqr  29804  qqhval2lem  30025  qqhf  30030  esumpinfval  30135  bj-dtru  32797  lindsenlbs  33404  poimirlem24  33433  isfldidl  33867  lssat  34303  paddasslem1  35106  lcfrlem21  36852  hdmap10lem  37131  hdmap11lem2  37134  jm2.23  37563  ntrneiel2  38384  ntrneik4w  38398  cncfiooicclem1  40106  fourierdlem81  40404