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  8883  divdivdivap  9004  divsubdivap  9019  ledivdiv  9181  lediv12a  9185  infssfzcldc  10618  infssfzledc  10619  suprzcl2dc  10623  exbtwnz  10634  qbtwnre  10640  ioom  10644  seq3caopr  10881  seqcaoprg  10882  leexp2r  10979  hashunlem  11193  hashfibclem  11231  wrd2ind  11440  recvguniq  11705  rsqrmo  11737  fsum2dlemstep  12145  expcnvre  12214  fprod2dlemstep  12333  bezout  12732  qredeu  12819  pw2dvdseu  12890  oddpwdclemndvds  12893  pcqmul  13026  pcadd  13063  pockthg  13080  grprida  13684  ghmpreima  14067  unitgrp  14346  islmodd  14553  lmodprop2d  14608  lsspropdg  14691  epttop  15067  restbasg  15145  iscnp4  15195  cnptopco  15199  blssps  15404  blss  15405  metequiv2  15473  xmetxpbl  15485  suplociccex  15602  dedekindicc  15610  limcimolemlt  15641  pellexlem3  15959  lgsquad2lem2  16067  2sqlem5  16104