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  5844  tfrlemisucaccv  6385  tfr1onlemsucaccv  6401  tfrcllemsucaccv  6414  addcmpblnq  7437  mulcmpblnq  7438  ordpipqqs  7444  nqnq0pi  7508  addcmpblnq0  7513  mulcmpblnq0  7514  addnq0mo  7517  mulnq0mo  7518  prarloclemcalc  7572  prarloc  7573  nqprl  7621  mullocpr  7641  distrlem4prl  7654  distrlem4pru  7655  ltprordil  7659  ltexprlemlol  7672  ltexprlemopu  7673  ltexprlemupu  7674  ltexprlemru  7682  cauappcvgprlemopl  7716  cauappcvgprlem2  7730  caucvgprlemopl  7739  caucvgprlem2  7750  caucvgprprlemexbt  7776  caucvgprprlem2  7780  suplocexprlemloc  7791  suplocexprlemub  7793  suplocexprlemlub  7794  addcmpblnr  7809  mulcmpblnrlemg  7810  mulcmpblnr  7811  prsrlem1  7812  addsrmo  7813  mulsrmo  7814  ltsrprg  7817  axmulcl  7936  recriota  7960  ltmul1  8622  divdivdivap  8743  divsubdivap  8758  ledivdiv  8920  lediv12a  8924  suprzcl2dc  10332  exbtwnz  10343  qbtwnre  10349  ioom  10353  seq3caopr  10590  seqcaoprg  10591  leexp2r  10688  hashunlem  10899  recvguniq  11163  rsqrmo  11195  fsum2dlemstep  11602  expcnvre  11671  fprod2dlemstep  11790  bezout  12189  qredeu  12276  pw2dvdseu  12347  oddpwdclemndvds  12350  pcqmul  12483  pcadd  12520  pockthg  12537  grprida  13056  ghmpreima  13422  unitgrp  13698  islmodd  13875  lmodprop2d  13930  lsspropdg  14013  epttop  14352  restbasg  14430  iscnp4  14480  cnptopco  14484  blssps  14689  blss  14690  metequiv2  14758  xmetxpbl  14770  suplociccex  14887  dedekindicc  14895  limcimolemlt  14926  lgsquad2lem2  15349  2sqlem5  15386