Theorem simprrr 506

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrr	|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )

Proof of Theorem simprrr

Step	Hyp	Ref	Expression
1		simpr 108	. 2 |- ( ( ch /\ th ) -> th )
2	1	ad2antll 474	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )

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:  fliftfun  5456  grpridd  5717  tfrlemisucaccv  5962  addcmpblnq  6557  mulcmpblnq  6558  ordpipqqs  6564  nqnq0pi  6628  addcmpblnq0  6633  mulcmpblnq0  6634  addnq0mo  6637  mulnq0mo  6638  prarloclemcalc  6692  prarloc  6693  nqprl  6741  mullocpr  6761  distrlem4prl  6774  distrlem4pru  6775  ltprordil  6779  ltexprlemlol  6792  ltexprlemopu  6793  ltexprlemupu  6794  ltexprlemru  6802  cauappcvgprlemopl  6836  cauappcvgprlem2  6850  caucvgprlemopl  6859  caucvgprlem2  6870  caucvgprprlemexbt  6896  caucvgprprlem2  6900  addcmpblnr  6916  mulcmpblnrlemg  6917  mulcmpblnr  6918  prsrlem1  6919  addsrmo  6920  mulsrmo  6921  ltsrprg  6924  axmulcl  7034  recriota  7056  ltmul1  7692  divdivdivap  7801  divsubdivap  7816  ledivdiv  7968  lediv12a  7972  qbtwnz  9260  qbtwnre  9265  ioom  9269  iseqcaopr  9462  leexp2r  9530  recvguniq  9881  rsqrmo  9913  bezout  10400  qredeu  10479  pw2dvdseu  10546  oddpwdclemndvds  10549