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  5443  fcof1  5962  fliftfun  5975  sbthlemi6  7245  sbthlemi8  7247  suppeqfsuppbi  7261  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  enq0tr  7765  addcmpblnq0  7774  mulcmpblnq0  7775  nnnq0lem1  7777  addnq0mo  7778  mulnq0mo  7779  prarloclemcalc  7833  addlocpr  7867  distrlem4prl  7915  distrlem4pru  7916  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  prsrlem1  8073  addsrmo  8074  mulsrmo  8075  ltsrprg  8078  apreap  8878  apreim  8894  aptap  8941  divdivdivap  9004  divsubdivap  9019  ledivdiv  9181  lediv12a  9185  exbtwnz  10634  seq3caopr  10881  seqcaoprg  10882  leexp2r  10979  hashfibclem  11231  zfz1iso  11238  wrd2ind  11440  swrdccat  11452  recvguniq  11705  rsqrmo  11737  summodclem2  12093  prodmodclem2  12288  prodmodc  12289  qredeu  12819  pw2dvdseu  12890  pcadd  13063  ballotfilemfc0  13176  ballotfilemfcc  13177  mhmpropd  13763  grprcan  13834  isnsg3  14008  ghmpreima  14067  rngpropd  14183  ringpropd  14266  islmodd  14553  lmodprop2d  14608  lss1d  14643  epttop  15067  txdis1cn  15255  metequiv2  15473  cncfmptc  15573  cncfmptid  15574  addccncf  15577  negcncf  15582  dedekindicclemicc  15609  mpodvdsmulf1o  15970  2sqlem5  16104  2sqlem9  16109