Theorem simprlr 504

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 108	. 2 |- ( ( ps /\ ch ) -> ch )
2	1	ad2antrl 473	1 |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  imain  5001  fcof1  5443  fliftfun  5456  addcmpblnq  6557  mulcmpblnq  6558  ordpipqqs  6564  enq0tr  6624  addcmpblnq0  6633  mulcmpblnq0  6634  nnnq0lem1  6636  addnq0mo  6637  mulnq0mo  6638  prarloclemcalc  6692  addlocpr  6726  distrlem4prl  6774  distrlem4pru  6775  addcmpblnr  6916  mulcmpblnrlemg  6917  mulcmpblnr  6918  prsrlem1  6919  addsrmo  6920  mulsrmo  6921  ltsrprg  6924  apreap  7687  apreim  7703  divdivdivap  7801  divsubdivap  7816  ledivdiv  7968  lediv12a  7972  qbtwnz  9260  iseqcaopr  9462  leexp2r  9530  recvguniq  9881  rsqrmo  9913  qredeu  10479  pw2dvdseu  10546