Theorem simprlr 540

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 110	. 2 |- ( ( ps /\ ch ) -> ch )
2	1	ad2antrl 490	1 |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ch )

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  5437  fcof1  5955  fliftfun  5968  sbthlemi6  7231  sbthlemi8  7233  suppeqfsuppbi  7247  addcmpblnq  7681  mulcmpblnq  7682  ordpipqqs  7688  enq0tr  7748  addcmpblnq0  7757  mulcmpblnq0  7758  nnnq0lem1  7760  addnq0mo  7761  mulnq0mo  7762  prarloclemcalc  7816  addlocpr  7850  distrlem4prl  7898  distrlem4pru  7899  addcmpblnr  8053  mulcmpblnrlemg  8054  mulcmpblnr  8055  prsrlem1  8056  addsrmo  8057  mulsrmo  8058  ltsrprg  8061  apreap  8860  apreim  8876  aptap  8923  divdivdivap  8986  divsubdivap  9001  ledivdiv  9163  lediv12a  9167  exbtwnz  10609  seq3caopr  10856  seqcaoprg  10857  leexp2r  10954  hashfibclem  11202  zfz1iso  11209  wrd2ind  11411  swrdccat  11423  recvguniq  11676  rsqrmo  11708  summodclem2  12064  prodmodclem2  12259  prodmodc  12260  qredeu  12790  pw2dvdseu  12861  pcadd  13034  mhmpropd  13671  grprcan  13742  isnsg3  13916  ghmpreima  13975  rngpropd  14091  ringpropd  14174  islmodd  14433  lmodprop2d  14488  lss1d  14523  epttop  14947  txdis1cn  15135  metequiv2  15353  cncfmptc  15453  cncfmptid  15454  addccncf  15457  negcncf  15462  dedekindicclemicc  15489  mpodvdsmulf1o  15850  2sqlem5  15984  2sqlem9  15989