Theorem simprrr 540

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  5840  tfrlemisucaccv  6380  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  addcmpblnq  7429  mulcmpblnq  7430  ordpipqqs  7436  nqnq0pi  7500  addcmpblnq0  7505  mulcmpblnq0  7506  addnq0mo  7509  mulnq0mo  7510  prarloclemcalc  7564  prarloc  7565  nqprl  7613  mullocpr  7633  distrlem4prl  7646  distrlem4pru  7647  ltprordil  7651  ltexprlemlol  7664  ltexprlemopu  7665  ltexprlemupu  7666  ltexprlemru  7674  cauappcvgprlemopl  7708  cauappcvgprlem2  7722  caucvgprlemopl  7731  caucvgprlem2  7742  caucvgprprlemexbt  7768  caucvgprprlem2  7772  suplocexprlemloc  7783  suplocexprlemub  7785  suplocexprlemlub  7786  addcmpblnr  7801  mulcmpblnrlemg  7802  mulcmpblnr  7803  prsrlem1  7804  addsrmo  7805  mulsrmo  7806  ltsrprg  7809  axmulcl  7928  recriota  7952  ltmul1  8613  divdivdivap  8734  divsubdivap  8749  ledivdiv  8911  lediv12a  8915  exbtwnz  10322  qbtwnre  10328  ioom  10332  seq3caopr  10569  seqcaoprg  10570  leexp2r  10667  hashunlem  10878  recvguniq  11142  rsqrmo  11174  fsum2dlemstep  11580  expcnvre  11649  fprod2dlemstep  11768  suprzcl2dc  12095  bezout  12151  qredeu  12238  pw2dvdseu  12309  oddpwdclemndvds  12312  pcqmul  12444  pcadd  12481  pockthg  12498  grprida  12973  ghmpreima  13339  unitgrp  13615  islmodd  13792  lmodprop2d  13847  lsspropdg  13930  epttop  14269  restbasg  14347  iscnp4  14397  cnptopco  14401  blssps  14606  blss  14607  metequiv2  14675  xmetxpbl  14687  suplociccex  14804  dedekindicc  14812  limcimolemlt  14843  lgsquad2lem2  15239  2sqlem5  15276