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  5412  fcof1  5924  fliftfun  5937  sbthlemi6  7161  sbthlemi8  7163  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  enq0tr  7654  addcmpblnq0  7663  mulcmpblnq0  7664  nnnq0lem1  7666  addnq0mo  7667  mulnq0mo  7668  prarloclemcalc  7722  addlocpr  7756  distrlem4prl  7804  distrlem4pru  7805  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  prsrlem1  7962  addsrmo  7963  mulsrmo  7964  ltsrprg  7967  apreap  8767  apreim  8783  aptap  8830  divdivdivap  8893  divsubdivap  8908  ledivdiv  9070  lediv12a  9074  exbtwnz  10511  seq3caopr  10758  seqcaoprg  10759  leexp2r  10856  zfz1iso  11106  wrd2ind  11308  swrdccat  11320  recvguniq  11560  rsqrmo  11592  summodclem2  11948  prodmodclem2  12143  prodmodc  12144  qredeu  12674  pw2dvdseu  12745  pcadd  12918  mhmpropd  13554  grprcan  13625  isnsg3  13799  ghmpreima  13858  rngpropd  13974  ringpropd  14057  islmodd  14313  lmodprop2d  14368  lss1d  14403  epttop  14820  txdis1cn  15008  metequiv2  15226  cncfmptc  15326  cncfmptid  15327  addccncf  15330  negcncf  15335  dedekindicclemicc  15362  mpodvdsmulf1o  15720  2sqlem5  15854  2sqlem9  15859