Theorem simprll 543

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprll	|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )

Proof of Theorem simprll

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	ad2antrl 494	1 |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  imain  5458  fcof1  5979  mpo0  6148  eroveu  6890  sbthlemi6  7269  sbthlemi8  7271  suppeqfsuppbi  7285  addcmpblnq  7724  mulcmpblnq  7725  ordpipqqs  7731  addcmpblnq0  7800  mulcmpblnq0  7801  nnnq0lem1  7803  prarloclemcalc  7859  addlocpr  7893  distrlem4prl  7941  distrlem4pru  7942  ltpopr  7952  addcmpblnr  8096  mulcmpblnrlemg  8097  mulcmpblnr  8098  prsrlem1  8099  ltsrprg  8104  apreap  8905  apreim  8921  aptap  8968  divdivdivap  9033  divmuleqap  9037  divadddivap  9047  divsubdivap  9048  ledivdiv  9210  lediv12a  9214  exbtwnz  10663  seq3caopr  10910  seqcaoprg  10911  leexp2r  11008  hashf1lem1  11263  hashf1lem2  11264  zfz1iso  11271  ccatsymb  11348  wrd2ind  11473  swrdccat  11485  recvguniq  11739  rsqrmo  11771  summodclem2  12127  prodmodc  12323  qredeu  12853  pw2dvdseu  12924  pcadd  13097  mhmpropd  13750  issubmd  13758  grprcan  13819  isnsg3  13987  ghmpreima  14046  rngpropd  14229  ringpropd  14316  lmodvsmmulgdi  14632  lmodprop2d  14657  lss1d  14692  epttop  15114  txdis1cn  15302  metequiv2  15520  mulc1cncf  15613  cncfmptc  15620  cncfmptid  15621  addccncf  15624  negcncf  15629  dedekindicclemicc  15656  mpodvdsmulf1o  16018  2sqlem5  16152  2sqlem9  16157