Theorem simprlr 538

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  5399  fcof1  5900  fliftfun  5913  sbthlemi6  7117  sbthlemi8  7119  addcmpblnq  7542  mulcmpblnq  7543  ordpipqqs  7549  enq0tr  7609  addcmpblnq0  7618  mulcmpblnq0  7619  nnnq0lem1  7621  addnq0mo  7622  mulnq0mo  7623  prarloclemcalc  7677  addlocpr  7711  distrlem4prl  7759  distrlem4pru  7760  addcmpblnr  7914  mulcmpblnrlemg  7915  mulcmpblnr  7916  prsrlem1  7917  addsrmo  7918  mulsrmo  7919  ltsrprg  7922  apreap  8722  apreim  8738  aptap  8785  divdivdivap  8848  divsubdivap  8863  ledivdiv  9025  lediv12a  9029  exbtwnz  10457  seq3caopr  10704  seqcaoprg  10705  leexp2r  10802  zfz1iso  11050  wrd2ind  11241  swrdccat  11253  recvguniq  11492  rsqrmo  11524  summodclem2  11879  prodmodclem2  12074  prodmodc  12075  qredeu  12605  pw2dvdseu  12676  pcadd  12849  mhmpropd  13485  grprcan  13556  isnsg3  13730  ghmpreima  13789  rngpropd  13904  ringpropd  13987  islmodd  14242  lmodprop2d  14297  lss1d  14332  epttop  14749  txdis1cn  14937  metequiv2  15155  cncfmptc  15255  cncfmptid  15256  addccncf  15259  negcncf  15264  dedekindicclemicc  15291  mpodvdsmulf1o  15649  2sqlem5  15783  2sqlem9  15788