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  5937  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  nqnq0pi  7658  addcmpblnq0  7663  mulcmpblnq0  7664  addnq0mo  7667  mulnq0mo  7668  prarloclemcalc  7722  prarloc  7723  nqprl  7771  mullocpr  7791  distrlem4prl  7804  distrlem4pru  7805  ltprordil  7809  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemru  7832  cauappcvgprlemopl  7866  cauappcvgprlem2  7880  caucvgprlemopl  7889  caucvgprlem2  7900  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  prsrlem1  7962  addsrmo  7963  mulsrmo  7964  ltsrprg  7967  axmulcl  8086  recriota  8110  ltmul1  8772  divdivdivap  8893  divsubdivap  8908  ledivdiv  9070  lediv12a  9074  suprzcl2dc  10500  exbtwnz  10511  qbtwnre  10517  ioom  10521  seq3caopr  10758  seqcaoprg  10759  leexp2r  10856  hashunlem  11068  wrd2ind  11308  recvguniq  11560  rsqrmo  11592  fsum2dlemstep  12000  expcnvre  12069  fprod2dlemstep  12188  bezout  12587  qredeu  12674  pw2dvdseu  12745  oddpwdclemndvds  12748  pcqmul  12881  pcadd  12918  pockthg  12935  grprida  13475  ghmpreima  13858  unitgrp  14136  islmodd  14313  lmodprop2d  14368  lsspropdg  14451  epttop  14820  restbasg  14898  iscnp4  14948  cnptopco  14952  blssps  15157  blss  15158  metequiv2  15226  xmetxpbl  15238  suplociccex  15355  dedekindicc  15363  limcimolemlt  15394  lgsquad2lem2  15817  2sqlem5  15854  2omap  16620