Theorem simprrr 530

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 109	. 2 |- ( ( ch /\ th ) -> th )
2	1	ad2antll 483	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  fliftfun  5763  grpridd  6034  tfrlemisucaccv  6289  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  addcmpblnq  7304  mulcmpblnq  7305  ordpipqqs  7311  nqnq0pi  7375  addcmpblnq0  7380  mulcmpblnq0  7381  addnq0mo  7384  mulnq0mo  7385  prarloclemcalc  7439  prarloc  7440  nqprl  7488  mullocpr  7508  distrlem4prl  7521  distrlem4pru  7522  ltprordil  7526  ltexprlemlol  7539  ltexprlemopu  7540  ltexprlemupu  7541  ltexprlemru  7549  cauappcvgprlemopl  7583  cauappcvgprlem2  7597  caucvgprlemopl  7606  caucvgprlem2  7617  caucvgprprlemexbt  7643  caucvgprprlem2  7647  suplocexprlemloc  7658  suplocexprlemub  7660  suplocexprlemlub  7661  addcmpblnr  7676  mulcmpblnrlemg  7677  mulcmpblnr  7678  prsrlem1  7679  addsrmo  7680  mulsrmo  7681  ltsrprg  7684  axmulcl  7803  recriota  7827  ltmul1  8486  divdivdivap  8605  divsubdivap  8620  ledivdiv  8781  lediv12a  8785  exbtwnz  10182  qbtwnre  10188  ioom  10192  seq3caopr  10414  leexp2r  10505  hashunlem  10713  recvguniq  10933  rsqrmo  10965  fsum2dlemstep  11371  expcnvre  11440  fprod2dlemstep  11559  suprzcl2dc  11884  bezout  11940  qredeu  12025  pw2dvdseu  12096  oddpwdclemndvds  12099  pcqmul  12231  pcadd  12267  pockthg  12283  epttop  12690  restbasg  12768  iscnp4  12818  cnptopco  12822  blssps  13027  blss  13028  metequiv2  13096  xmetxpbl  13108  suplociccex  13203  dedekindicc  13211  limcimolemlt  13233  2sqlem5  13555