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  5466  fcof1  5992  mpo0  6161  eroveu  6904  sbthlemi6  7284  sbthlemi8  7286  suppeqfsuppbi  7300  addcmpblnq  7740  mulcmpblnq  7741  ordpipqqs  7747  addcmpblnq0  7816  mulcmpblnq0  7817  nnnq0lem1  7819  prarloclemcalc  7875  addlocpr  7909  distrlem4prl  7957  distrlem4pru  7958  ltpopr  7968  addcmpblnr  8112  mulcmpblnrlemg  8113  mulcmpblnr  8114  prsrlem1  8115  ltsrprg  8120  apreap  8923  apreim  8939  aptap  8986  divdivdivap  9051  divmuleqap  9055  divadddivap  9065  divsubdivap  9066  ledivdiv  9228  lediv12a  9232  exbtwnz  10702  seq3caopr  10953  seqcaoprg  10954  leexp2r  11051  hashf1lem1  11307  hashf1lem2  11308  zfz1iso  11315  ccatsymb  11392  wrd2ind  11517  swrdccat  11529  recvguniq  11783  rsqrmo  11815  summodclem2  12174  prodmodc  12370  qredeu  12900  pwbdvdseu  12972  pcadd  13148  mhmpropd  13832  issubmd  13840  grprcan  13901  isnsg3  14069  ghmpreima  14128  rngpropd  14361  ringpropd  14450  lmodvsmmulgdi  14769  lmodprop2d  14794  lss1d  14829  assamulgscmlem2  15151  epttop  15316  txdis1cn  15504  metequiv2  15722  mulc1cncf  15815  cncfmptc  15822  cncfmptid  15823  addccncf  15826  negcncf  15831  dedekindicclemicc  15858  mpodvdsmulf1o  16284  2sqlem5  16443  2sqlem9  16448