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  5975  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  2omap  7282  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  nqnq0pi  7769  addcmpblnq0  7774  mulcmpblnq0  7775  addnq0mo  7778  mulnq0mo  7779  prarloclemcalc  7833  prarloc  7834  nqprl  7882  mullocpr  7902  distrlem4prl  7915  distrlem4pru  7916  ltprordil  7920  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemru  7943  cauappcvgprlemopl  7977  cauappcvgprlem2  7991  caucvgprlemopl  8000  caucvgprlem2  8011  caucvgprprlemexbt  8037  caucvgprprlem2  8041  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  prsrlem1  8073  addsrmo  8074  mulsrmo  8075  ltsrprg  8078  axmulcl  8197  recriota  8221  ltmul1  8884  divdivdivap  9007  divsubdivap  9022  ledivdiv  9184  lediv12a  9188  infssfzcldc  10621  infssfzledc  10622  suprzcl2dc  10626  exbtwnz  10637  qbtwnre  10643  ioom  10647  seq3caopr  10884  seqcaoprg  10885  leexp2r  10982  hashunlem  11196  hashfibclem  11234  wrd2ind  11443  recvguniq  11709  rsqrmo  11741  fsum2dlemstep  12149  expcnvre  12218  fprod2dlemstep  12337  bezout  12736  qredeu  12823  pw2dvdseu  12894  oddpwdclemndvds  12897  pcqmul  13030  pcadd  13067  pockthg  13084  grprida  13654  ghmpreima  14023  unitgrp  14365  islmodd  14571  lmodprop2d  14626  lsspropdg  14709  epttop  15085  restbasg  15163  iscnp4  15213  cnptopco  15217  blssps  15422  blss  15423  metequiv2  15491  xmetxpbl  15503  suplociccex  15620  dedekindicc  15628  limcimolemlt  15659  pellexlem3  15977  lgsquad2lem2  16085  2sqlem5  16122