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  5096  fcof1  5562  fliftfun  5575  sbthlemi6  6671  sbthlemi8  6673  addcmpblnq  6926  mulcmpblnq  6927  ordpipqqs  6933  enq0tr  6993  addcmpblnq0  7002  mulcmpblnq0  7003  nnnq0lem1  7005  addnq0mo  7006  mulnq0mo  7007  prarloclemcalc  7061  addlocpr  7095  distrlem4prl  7143  distrlem4pru  7144  addcmpblnr  7285  mulcmpblnrlemg  7286  mulcmpblnr  7287  prsrlem1  7288  addsrmo  7289  mulsrmo  7290  ltsrprg  7293  apreap  8064  apreim  8080  divdivdivap  8180  divsubdivap  8195  ledivdiv  8351  lediv12a  8355  exbtwnz  9662  iseqcaopr  9912  leexp2r  10009  zfz1iso  10246  recvguniq  10428  rsqrmo  10460  isummolem2  10772  qredeu  11357  pw2dvdseu  11424