Theorem simprrr 535

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 488	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  5775  tfrlemisucaccv  6304  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  addcmpblnq  7329  mulcmpblnq  7330  ordpipqqs  7336  nqnq0pi  7400  addcmpblnq0  7405  mulcmpblnq0  7406  addnq0mo  7409  mulnq0mo  7410  prarloclemcalc  7464  prarloc  7465  nqprl  7513  mullocpr  7533  distrlem4prl  7546  distrlem4pru  7547  ltprordil  7551  ltexprlemlol  7564  ltexprlemopu  7565  ltexprlemupu  7566  ltexprlemru  7574  cauappcvgprlemopl  7608  cauappcvgprlem2  7622  caucvgprlemopl  7631  caucvgprlem2  7642  caucvgprprlemexbt  7668  caucvgprprlem2  7672  suplocexprlemloc  7683  suplocexprlemub  7685  suplocexprlemlub  7686  addcmpblnr  7701  mulcmpblnrlemg  7702  mulcmpblnr  7703  prsrlem1  7704  addsrmo  7705  mulsrmo  7706  ltsrprg  7709  axmulcl  7828  recriota  7852  ltmul1  8511  divdivdivap  8630  divsubdivap  8645  ledivdiv  8806  lediv12a  8810  exbtwnz  10207  qbtwnre  10213  ioom  10217  seq3caopr  10439  leexp2r  10530  hashunlem  10739  recvguniq  10959  rsqrmo  10991  fsum2dlemstep  11397  expcnvre  11466  fprod2dlemstep  11585  suprzcl2dc  11910  bezout  11966  qredeu  12051  pw2dvdseu  12122  oddpwdclemndvds  12125  pcqmul  12257  pcadd  12293  pockthg  12309  grpridd  12641  epttop  12884  restbasg  12962  iscnp4  13012  cnptopco  13016  blssps  13221  blss  13222  metequiv2  13290  xmetxpbl  13302  suplociccex  13397  dedekindicc  13405  limcimolemlt  13427  2sqlem5  13749