Theorem simprlr 528

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

Assertion

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

Proof of Theorem simprlr

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  imain  5270  fcof1  5751  fliftfun  5764  sbthlemi6  6927  sbthlemi8  6929  addcmpblnq  7308  mulcmpblnq  7309  ordpipqqs  7315  enq0tr  7375  addcmpblnq0  7384  mulcmpblnq0  7385  nnnq0lem1  7387  addnq0mo  7388  mulnq0mo  7389  prarloclemcalc  7443  addlocpr  7477  distrlem4prl  7525  distrlem4pru  7526  addcmpblnr  7680  mulcmpblnrlemg  7681  mulcmpblnr  7682  prsrlem1  7683  addsrmo  7684  mulsrmo  7685  ltsrprg  7688  apreap  8485  apreim  8501  divdivdivap  8609  divsubdivap  8624  ledivdiv  8785  lediv12a  8789  exbtwnz  10186  seq3caopr  10418  leexp2r  10509  zfz1iso  10754  recvguniq  10937  rsqrmo  10969  summodclem2  11323  prodmodclem2  11518  prodmodc  11519  qredeu  12029  pw2dvdseu  12100  pcadd  12271  epttop  12730  txdis1cn  12918  metequiv2  13136  cncfmptc  13222  cncfmptid  13223  addccncf  13226  negcncf  13228  dedekindicclemicc  13250  2sqlem5  13595  2sqlem9  13600