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  5947  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  addcmpblnq  7630  mulcmpblnq  7631  ordpipqqs  7637  nqnq0pi  7701  addcmpblnq0  7706  mulcmpblnq0  7707  addnq0mo  7710  mulnq0mo  7711  prarloclemcalc  7765  prarloc  7766  nqprl  7814  mullocpr  7834  distrlem4prl  7847  distrlem4pru  7848  ltprordil  7852  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemru  7875  cauappcvgprlemopl  7909  cauappcvgprlem2  7923  caucvgprlemopl  7932  caucvgprlem2  7943  caucvgprprlemexbt  7969  caucvgprprlem2  7973  suplocexprlemloc  7984  suplocexprlemub  7986  suplocexprlemlub  7987  addcmpblnr  8002  mulcmpblnrlemg  8003  mulcmpblnr  8004  prsrlem1  8005  addsrmo  8006  mulsrmo  8007  ltsrprg  8010  axmulcl  8129  recriota  8153  ltmul1  8815  divdivdivap  8936  divsubdivap  8951  ledivdiv  9113  lediv12a  9117  suprzcl2dc  10543  exbtwnz  10554  qbtwnre  10560  ioom  10564  seq3caopr  10801  seqcaoprg  10802  leexp2r  10899  hashunlem  11111  wrd2ind  11351  recvguniq  11616  rsqrmo  11648  fsum2dlemstep  12056  expcnvre  12125  fprod2dlemstep  12244  bezout  12643  qredeu  12730  pw2dvdseu  12801  oddpwdclemndvds  12804  pcqmul  12937  pcadd  12974  pockthg  12991  grprida  13531  ghmpreima  13914  unitgrp  14192  islmodd  14369  lmodprop2d  14424  lsspropdg  14507  epttop  14881  restbasg  14959  iscnp4  15009  cnptopco  15013  blssps  15218  blss  15219  metequiv2  15287  xmetxpbl  15299  suplociccex  15416  dedekindicc  15424  limcimolemlt  15455  pellexlem3  15773  lgsquad2lem2  15881  2sqlem5  15918  2omap  16695