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  8879  apreim  8895  aptap  8942  divdivdivap  9007  divsubdivap  9022  ledivdiv  9184  lediv12a  9188  exbtwnz  10637  seq3caopr  10884  seqcaoprg  10885  leexp2r  10982  hashfibclem  11234  zfz1iso  11241  wrd2ind  11443  swrdccat  11455  recvguniq  11709  rsqrmo  11741  summodclem2  12097  prodmodclem2  12292  prodmodc  12293  qredeu  12823  pw2dvdseu  12894  pcadd  13067  ballotfilemfc0  13180  ballotfilemfcc  13181  mhmpropd  13725  grprcan  13796  isnsg3  13964  ghmpreima  14023  rngpropd  14198  ringpropd  14285  islmodd  14571  lmodprop2d  14626  lss1d  14661  epttop  15085  txdis1cn  15273  metequiv2  15491  cncfmptc  15591  cncfmptid  15592  addccncf  15595  negcncf  15600  dedekindicclemicc  15627  mpodvdsmulf1o  15988  2sqlem5  16122  2sqlem9  16127