Theorem simprrl 545

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 495	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  973  imain  5458  tfrlemisucaccv  6586  tfrexlem  6595  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  eroveu  6890  addcmpblnq  7724  mulcmpblnq  7725  ordpipqqs  7731  nqnq0pi  7795  addcmpblnq0  7800  mulcmpblnq0  7801  prarloclemcalc  7859  prarloc  7860  nqpru  7909  mullocpr  7928  distrlem4prl  7941  distrlem4pru  7942  ltprordil  7946  ltexprlemm  7957  ltexprlemopu  7960  ltexprlemupu  7961  ltexprlemru  7969  cauappcvgprlemopl  8003  cauappcvgprlem2  8017  caucvgprlemopl  8026  caucvgprlem2  8037  caucvgprprlemexbt  8063  caucvgprprlem2  8067  suplocexprlemloc  8078  suplocexprlemub  8080  suplocexprlemlub  8081  addcmpblnr  8096  mulcmpblnrlemg  8097  mulcmpblnr  8098  prsrlem1  8099  ltsrprg  8104  axmulcl  8223  ltmul1  8910  divdivdivap  9033  divmuleqap  9037  divsubdivap  9048  lt2mul2div  9199  ledivdiv  9210  lediv12a  9214  ssfzo12bi  10621  infssfzcldc  10647  infssfzledc  10648  suprzcl2dc  10652  exbtwnz  10663  qbtwnre  10669  ioom  10673  seq3caopr  10910  seqcaoprg  10911  leexp2r  11008  hashunlem  11222  hashfibclem  11260  wrd2ind  11473  recvguniq  11739  rsqrmo  11771  fsum2dlemstep  12179  expcnvre  12248  fprod2dlemstep  12367  bezout  12766  qredeu  12853  pw2dvdseu  12924  oddpwdclemdvds  12926  pcqmul  13060  pcadd  13097  pockthg  13114  grprida  13684  issubmd  13758  ghmpreima  14046  unitgrp  14396  lmodprop2d  14657  lsspropdg  14740  neiint  15169  restbasg  15192  iscnp4  15242  cnpnei  15243  cnptopco  15246  blssps  15451  blss  15452  metequiv2  15520  xmetxpbl  15532  suplociccex  15649  dedekindicc  15657  limcimolemlt  15688  pellexlem3  16007  lgsquad2lem2  16115  2sqlem5  16152