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  5913  tfrlemisucaccv  6461  tfr1onlemsucaccv  6477  tfrcllemsucaccv  6490  addcmpblnq  7542  mulcmpblnq  7543  ordpipqqs  7549  nqnq0pi  7613  addcmpblnq0  7618  mulcmpblnq0  7619  addnq0mo  7622  mulnq0mo  7623  prarloclemcalc  7677  prarloc  7678  nqprl  7726  mullocpr  7746  distrlem4prl  7759  distrlem4pru  7760  ltprordil  7764  ltexprlemlol  7777  ltexprlemopu  7778  ltexprlemupu  7779  ltexprlemru  7787  cauappcvgprlemopl  7821  cauappcvgprlem2  7835  caucvgprlemopl  7844  caucvgprlem2  7855  caucvgprprlemexbt  7881  caucvgprprlem2  7885  suplocexprlemloc  7896  suplocexprlemub  7898  suplocexprlemlub  7899  addcmpblnr  7914  mulcmpblnrlemg  7915  mulcmpblnr  7916  prsrlem1  7917  addsrmo  7918  mulsrmo  7919  ltsrprg  7922  axmulcl  8041  recriota  8065  ltmul1  8727  divdivdivap  8848  divsubdivap  8863  ledivdiv  9025  lediv12a  9029  suprzcl2dc  10446  exbtwnz  10457  qbtwnre  10463  ioom  10467  seq3caopr  10704  seqcaoprg  10705  leexp2r  10802  hashunlem  11013  wrd2ind  11241  recvguniq  11492  rsqrmo  11524  fsum2dlemstep  11931  expcnvre  12000  fprod2dlemstep  12119  bezout  12518  qredeu  12605  pw2dvdseu  12676  oddpwdclemndvds  12679  pcqmul  12812  pcadd  12849  pockthg  12866  grprida  13406  ghmpreima  13789  unitgrp  14065  islmodd  14242  lmodprop2d  14297  lsspropdg  14380  epttop  14749  restbasg  14827  iscnp4  14877  cnptopco  14881  blssps  15086  blss  15087  metequiv2  15155  xmetxpbl  15167  suplociccex  15284  dedekindicc  15292  limcimolemlt  15323  lgsquad2lem2  15746  2sqlem5  15783  2omap  16290