Theorem simprrr 546

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 495	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  fliftfun  6002  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  2omap  7319  addcmpblnq  7735  mulcmpblnq  7736  ordpipqqs  7742  nqnq0pi  7806  addcmpblnq0  7811  mulcmpblnq0  7812  addnq0mo  7815  mulnq0mo  7816  prarloclemcalc  7870  prarloc  7871  nqprl  7919  mullocpr  7939  distrlem4prl  7952  distrlem4pru  7953  ltprordil  7957  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemru  7980  cauappcvgprlemopl  8014  cauappcvgprlem2  8028  caucvgprlemopl  8037  caucvgprlem2  8048  caucvgprprlemexbt  8074  caucvgprprlem2  8078  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexprlemlub  8092  addcmpblnr  8107  mulcmpblnrlemg  8108  mulcmpblnr  8109  prsrlem1  8110  addsrmo  8111  mulsrmo  8112  ltsrprg  8115  axmulcl  8234  recriota  8258  ltmul1  8923  divdivdivap  9046  divsubdivap  9061  ledivdiv  9223  lediv12a  9227  infssfzcldc  10680  infssfzledc  10681  suprzcl2dc  10685  exbtwnz  10696  qbtwnre  10702  ioom  10706  seq3caopr  10946  seqcaoprg  10947  leexp2r  11044  hashunlem  11259  hashfibclem  11297  wrd2ind  11510  recvguniq  11776  rsqrmo  11808  fsum2dlemstep  12219  expcnvre  12288  fprod2dlemstep  12407  bezout  12806  qredeu  12893  pwbdvdseu  12965  nnmaxpwlemndvds  12968  nnmaxpwlemparts  12970  pcqmul  13104  pcadd  13141  pockthg  13158  grprida  13758  ghmpreima  14120  unitgrp  14474  islmodd  14680  lmodprop2d  14736  lsspropdg  14819  assapropd  15065  epttop  15243  restbasg  15321  iscnp4  15371  cnptopco  15375  blssps  15580  blss  15581  metequiv2  15649  xmetxpbl  15661  suplociccex  15778  dedekindicc  15786  limcimolemlt  15817  pellexlem3  16153  lgsquad2lem2  16323  2sqlem5  16360