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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  imain  5463  fcof1  5989  mpo0  6158  eroveu  6900  sbthlemi6  7279  sbthlemi8  7281  suppeqfsuppbi  7295  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  addcmpblnq0  7810  mulcmpblnq0  7811  nnnq0lem1  7813  prarloclemcalc  7869  addlocpr  7903  distrlem4prl  7951  distrlem4pru  7952  ltpopr  7962  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  prsrlem1  8109  ltsrprg  8114  apreap  8915  apreim  8931  aptap  8978  divdivdivap  9043  divmuleqap  9047  divadddivap  9057  divsubdivap  9058  ledivdiv  9220  lediv12a  9224  exbtwnz  10685  seq3caopr  10932  seqcaoprg  10933  leexp2r  11030  hashf1lem1  11285  hashf1lem2  11286  zfz1iso  11293  ccatsymb  11370  wrd2ind  11495  swrdccat  11507  recvguniq  11761  rsqrmo  11793  summodclem2  12149  prodmodc  12345  qredeu  12875  pw2dvdseu  12946  pcadd  13119  mhmpropd  13773  issubmd  13781  grprcan  13842  isnsg3  14010  ghmpreima  14069  rngpropd  14254  ringpropd  14343  lmodvsmmulgdi  14660  lmodprop2d  14685  lss1d  14720  assamulgscmlem2  15042  epttop  15191  txdis1cn  15379  metequiv2  15597  mulc1cncf  15690  cncfmptc  15697  cncfmptid  15698  addccncf  15701  negcncf  15706  dedekindicclemicc  15733  mpodvdsmulf1o  16104  2sqlem5  16238  2sqlem9  16243