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  5875  tfrlemisucaccv  6421  tfr1onlemsucaccv  6437  tfrcllemsucaccv  6450  addcmpblnq  7493  mulcmpblnq  7494  ordpipqqs  7500  nqnq0pi  7564  addcmpblnq0  7569  mulcmpblnq0  7570  addnq0mo  7573  mulnq0mo  7574  prarloclemcalc  7628  prarloc  7629  nqprl  7677  mullocpr  7697  distrlem4prl  7710  distrlem4pru  7711  ltprordil  7715  ltexprlemlol  7728  ltexprlemopu  7729  ltexprlemupu  7730  ltexprlemru  7738  cauappcvgprlemopl  7772  cauappcvgprlem2  7786  caucvgprlemopl  7795  caucvgprlem2  7806  caucvgprprlemexbt  7832  caucvgprprlem2  7836  suplocexprlemloc  7847  suplocexprlemub  7849  suplocexprlemlub  7850  addcmpblnr  7865  mulcmpblnrlemg  7866  mulcmpblnr  7867  prsrlem1  7868  addsrmo  7869  mulsrmo  7870  ltsrprg  7873  axmulcl  7992  recriota  8016  ltmul1  8678  divdivdivap  8799  divsubdivap  8814  ledivdiv  8976  lediv12a  8980  suprzcl2dc  10395  exbtwnz  10406  qbtwnre  10412  ioom  10416  seq3caopr  10653  seqcaoprg  10654  leexp2r  10751  hashunlem  10962  recvguniq  11356  rsqrmo  11388  fsum2dlemstep  11795  expcnvre  11864  fprod2dlemstep  11983  bezout  12382  qredeu  12469  pw2dvdseu  12540  oddpwdclemndvds  12543  pcqmul  12676  pcadd  12713  pockthg  12730  grprida  13269  ghmpreima  13652  unitgrp  13928  islmodd  14105  lmodprop2d  14160  lsspropdg  14243  epttop  14612  restbasg  14690  iscnp4  14740  cnptopco  14744  blssps  14949  blss  14950  metequiv2  15018  xmetxpbl  15030  suplociccex  15147  dedekindicc  15155  limcimolemlt  15186  lgsquad2lem2  15609  2sqlem5  15646  2omap  16047