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  5298  fcof1  5783  fliftfun  5796  sbthlemi6  6960  sbthlemi8  6962  addcmpblnq  7365  mulcmpblnq  7366  ordpipqqs  7372  enq0tr  7432  addcmpblnq0  7441  mulcmpblnq0  7442  nnnq0lem1  7444  addnq0mo  7445  mulnq0mo  7446  prarloclemcalc  7500  addlocpr  7534  distrlem4prl  7582  distrlem4pru  7583  addcmpblnr  7737  mulcmpblnrlemg  7738  mulcmpblnr  7739  prsrlem1  7740  addsrmo  7741  mulsrmo  7742  ltsrprg  7745  apreap  8543  apreim  8559  aptap  8606  divdivdivap  8669  divsubdivap  8684  ledivdiv  8846  lediv12a  8850  exbtwnz  10250  seq3caopr  10482  leexp2r  10573  zfz1iso  10820  recvguniq  11003  rsqrmo  11035  summodclem2  11389  prodmodclem2  11584  prodmodc  11585  qredeu  12096  pw2dvdseu  12167  pcadd  12338  mhmpropd  12856  grprcan  12909  isnsg3  13065  ringpropd  13215  islmodd  13381  epttop  13560  txdis1cn  13748  metequiv2  13966  cncfmptc  14052  cncfmptid  14053  addccncf  14056  negcncf  14058  dedekindicclemicc  14080  2sqlem5  14436  2sqlem9  14441