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  5337  fcof1  5827  fliftfun  5840  sbthlemi6  7023  sbthlemi8  7025  addcmpblnq  7429  mulcmpblnq  7430  ordpipqqs  7436  enq0tr  7496  addcmpblnq0  7505  mulcmpblnq0  7506  nnnq0lem1  7508  addnq0mo  7509  mulnq0mo  7510  prarloclemcalc  7564  addlocpr  7598  distrlem4prl  7646  distrlem4pru  7647  addcmpblnr  7801  mulcmpblnrlemg  7802  mulcmpblnr  7803  prsrlem1  7804  addsrmo  7805  mulsrmo  7806  ltsrprg  7809  apreap  8608  apreim  8624  aptap  8671  divdivdivap  8734  divsubdivap  8749  ledivdiv  8911  lediv12a  8915  exbtwnz  10322  seq3caopr  10569  seqcaoprg  10570  leexp2r  10667  zfz1iso  10915  recvguniq  11142  rsqrmo  11174  summodclem2  11528  prodmodclem2  11723  prodmodc  11724  qredeu  12238  pw2dvdseu  12309  pcadd  12481  mhmpropd  13041  grprcan  13112  isnsg3  13280  ghmpreima  13339  rngpropd  13454  ringpropd  13537  islmodd  13792  lmodprop2d  13847  lss1d  13882  epttop  14269  txdis1cn  14457  metequiv2  14675  cncfmptc  14775  cncfmptid  14776  addccncf  14779  negcncf  14784  dedekindicclemicc  14811  2sqlem5  15276  2sqlem9  15281