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  5297  fcof1  5781  fliftfun  5794  sbthlemi6  6958  sbthlemi8  6960  addcmpblnq  7363  mulcmpblnq  7364  ordpipqqs  7370  enq0tr  7430  addcmpblnq0  7439  mulcmpblnq0  7440  nnnq0lem1  7442  addnq0mo  7443  mulnq0mo  7444  prarloclemcalc  7498  addlocpr  7532  distrlem4prl  7580  distrlem4pru  7581  addcmpblnr  7735  mulcmpblnrlemg  7736  mulcmpblnr  7737  prsrlem1  7738  addsrmo  7739  mulsrmo  7740  ltsrprg  7743  apreap  8540  apreim  8556  aptap  8603  divdivdivap  8666  divsubdivap  8681  ledivdiv  8843  lediv12a  8847  exbtwnz  10246  seq3caopr  10478  leexp2r  10569  zfz1iso  10814  recvguniq  10997  rsqrmo  11029  summodclem2  11383  prodmodclem2  11578  prodmodc  11579  qredeu  12089  pw2dvdseu  12160  pcadd  12331  mhmpropd  12789  grprcan  12842  isnsg3  12998  ringpropd  13148  epttop  13461  txdis1cn  13649  metequiv2  13867  cncfmptc  13953  cncfmptid  13954  addccncf  13957  negcncf  13959  dedekindicclemicc  13981  2sqlem5  14326  2sqlem9  14331