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  6005  tfrlemisucaccv  6601  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  2omap  7325  addcmpblnq  7741  mulcmpblnq  7742  ordpipqqs  7748  nqnq0pi  7812  addcmpblnq0  7817  mulcmpblnq0  7818  addnq0mo  7821  mulnq0mo  7822  prarloclemcalc  7876  prarloc  7877  nqprl  7925  mullocpr  7945  distrlem4prl  7958  distrlem4pru  7959  ltprordil  7963  ltexprlemlol  7976  ltexprlemopu  7977  ltexprlemupu  7978  ltexprlemru  7986  cauappcvgprlemopl  8020  cauappcvgprlem2  8034  caucvgprlemopl  8043  caucvgprlem2  8054  caucvgprprlemexbt  8080  caucvgprprlem2  8084  suplocexprlemloc  8095  suplocexprlemub  8097  suplocexprlemlub  8098  addcmpblnr  8113  mulcmpblnrlemg  8114  mulcmpblnr  8115  prsrlem1  8116  addsrmo  8117  mulsrmo  8118  ltsrprg  8121  axmulcl  8240  recriota  8264  ltmul1  8929  divdivdivap  9052  divsubdivap  9067  ledivdiv  9229  lediv12a  9233  infssfzcldc  10686  infssfzledc  10687  suprzcl2dc  10691  exbtwnz  10702  qbtwnre  10708  ioom  10712  seq3caopr  10953  seqcaoprg  10954  leexp2r  11051  hashunlem  11266  hashfibclem  11304  wrd2ind  11517  recvguniq  11783  rsqrmo  11815  fsum2dlemstep  12226  expcnvre  12295  fprod2dlemstep  12414  bezout  12813  qredeu  12900  pwbdvdseu  12972  nnmaxpwlemndvds  12975  nnmaxpwlemparts  12977  pcqmul  13111  pcadd  13148  pockthg  13165  grprida  13766  ghmpreima  14128  unitgrp  14532  islmodd  14738  lmodprop2d  14794  lsspropdg  14877  assapropd  15123  mplsubgfilemcl  15246  epttop  15349  restbasg  15427  iscnp4  15477  cnptopco  15481  blssps  15686  blss  15687  metequiv2  15755  xmetxpbl  15767  suplociccex  15884  dedekindicc  15892  limcimolemlt  15923  pellexlem3  16264  lgsquad2lem2  16439  2sqlem5  16476