Theorem simprrr 542

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

Syntax hints:   -> wi 4   /\ wa 104

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

This theorem is referenced by:  fliftfun  5968  tfrlemisucaccv  6555  tfr1onlemsucaccv  6571  tfrcllemsucaccv  6584  2omap  7268  addcmpblnq  7681  mulcmpblnq  7682  ordpipqqs  7688  nqnq0pi  7752  addcmpblnq0  7757  mulcmpblnq0  7758  addnq0mo  7761  mulnq0mo  7762  prarloclemcalc  7816  prarloc  7817  nqprl  7865  mullocpr  7885  distrlem4prl  7898  distrlem4pru  7899  ltprordil  7903  ltexprlemlol  7916  ltexprlemopu  7917  ltexprlemupu  7918  ltexprlemru  7926  cauappcvgprlemopl  7960  cauappcvgprlem2  7974  caucvgprlemopl  7983  caucvgprlem2  7994  caucvgprprlemexbt  8020  caucvgprprlem2  8024  suplocexprlemloc  8035  suplocexprlemub  8037  suplocexprlemlub  8038  addcmpblnr  8053  mulcmpblnrlemg  8054  mulcmpblnr  8055  prsrlem1  8056  addsrmo  8057  mulsrmo  8058  ltsrprg  8061  axmulcl  8180  recriota  8204  ltmul1  8865  divdivdivap  8986  divsubdivap  9001  ledivdiv  9163  lediv12a  9167  suprzcl2dc  10598  exbtwnz  10609  qbtwnre  10615  ioom  10619  seq3caopr  10856  seqcaoprg  10857  leexp2r  10954  hashunlem  11166  hashfibclem  11202  wrd2ind  11411  recvguniq  11676  rsqrmo  11708  fsum2dlemstep  12116  expcnvre  12185  fprod2dlemstep  12304  bezout  12703  qredeu  12790  pw2dvdseu  12861  oddpwdclemndvds  12864  pcqmul  12997  pcadd  13034  pockthg  13051  grprida  13592  ghmpreima  13975  unitgrp  14253  islmodd  14433  lmodprop2d  14488  lsspropdg  14571  epttop  14947  restbasg  15025  iscnp4  15075  cnptopco  15079  blssps  15284  blss  15285  metequiv2  15353  xmetxpbl  15365  suplociccex  15482  dedekindicc  15490  limcimolemlt  15521  pellexlem3  15839  lgsquad2lem2  15947  2sqlem5  15984