Theorem simprlr 505

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 474	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  5033  fcof1  5475  fliftfun  5488  addcmpblnq  6655  mulcmpblnq  6656  ordpipqqs  6662  enq0tr  6722  addcmpblnq0  6731  mulcmpblnq0  6732  nnnq0lem1  6734  addnq0mo  6735  mulnq0mo  6736  prarloclemcalc  6790  addlocpr  6824  distrlem4prl  6872  distrlem4pru  6873  addcmpblnr  7014  mulcmpblnrlemg  7015  mulcmpblnr  7016  prsrlem1  7017  addsrmo  7018  mulsrmo  7019  ltsrprg  7022  apreap  7790  apreim  7806  divdivdivap  7904  divsubdivap  7919  ledivdiv  8071  lediv12a  8075  exbtwnz  9373  iseqcaopr  9594  leexp2r  9663  recvguniq  10066  rsqrmo  10098  qredeu  10670  pw2dvdseu  10737