Theorem simprlr 490

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

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  imain  4981  fcof1  5423  fliftfun  5436  addcmpblnq  6465  mulcmpblnq  6466  ordpipqqs  6472  enq0tr  6532  addcmpblnq0  6541  mulcmpblnq0  6542  nnnq0lem1  6544  addnq0mo  6545  mulnq0mo  6546  prarloclemcalc  6600  addlocpr  6634  distrlem4prl  6682  distrlem4pru  6683  addcmpblnr  6824  mulcmpblnrlemg  6825  mulcmpblnr  6826  prsrlem1  6827  addsrmo  6828  mulsrmo  6829  ltsrprg  6832  apreap  7578  apreim  7594  divdivdivap  7689  divsubdivap  7704  ledivdiv  7856  lediv12a  7860  qbtwnz  9106  iseqcaopr  9242  leexp2r  9308  recvguniq  9593  rsqrmo  9625