Theorem simprrl 541

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrl	|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )

Proof of Theorem simprrl

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ch /\ th ) -> ch )
2	1	ad2antll 491	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )

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:  dn1dc  969  imain  5443  tfrlemisucaccv  6569  tfrexlem  6578  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  eroveu  6873  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  nqnq0pi  7769  addcmpblnq0  7774  mulcmpblnq0  7775  prarloclemcalc  7833  prarloc  7834  nqpru  7883  mullocpr  7902  distrlem4prl  7915  distrlem4pru  7916  ltprordil  7920  ltexprlemm  7931  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemru  7943  cauappcvgprlemopl  7977  cauappcvgprlem2  7991  caucvgprlemopl  8000  caucvgprlem2  8011  caucvgprprlemexbt  8037  caucvgprprlem2  8041  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  prsrlem1  8073  ltsrprg  8078  axmulcl  8197  ltmul1  8883  divdivdivap  9004  divmuleqap  9008  divsubdivap  9019  lt2mul2div  9170  ledivdiv  9181  lediv12a  9185  ssfzo12bi  10592  infssfzcldc  10618  infssfzledc  10619  suprzcl2dc  10623  exbtwnz  10634  qbtwnre  10640  ioom  10644  seq3caopr  10881  seqcaoprg  10882  leexp2r  10979  hashunlem  11193  hashfibclem  11231  wrd2ind  11440  recvguniq  11705  rsqrmo  11737  fsum2dlemstep  12145  expcnvre  12214  fprod2dlemstep  12333  bezout  12732  qredeu  12819  pw2dvdseu  12890  oddpwdclemdvds  12892  pcqmul  13026  pcadd  13063  pockthg  13080  grprida  13650  issubmd  13729  ghmpreima  14019  unitgrp  14361  lmodprop2d  14622  lsspropdg  14705  neiint  15136  restbasg  15159  iscnp4  15209  cnpnei  15210  cnptopco  15213  blssps  15418  blss  15419  metequiv2  15487  xmetxpbl  15499  suplociccex  15616  dedekindicc  15624  limcimolemlt  15655  pellexlem3  15973  lgsquad2lem2  16081  2sqlem5  16118