Theorem simprrl 539

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  962  imain  5355  tfrlemisucaccv  6410  tfrexlem  6419  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  eroveu  6712  addcmpblnq  7479  mulcmpblnq  7480  ordpipqqs  7486  nqnq0pi  7550  addcmpblnq0  7555  mulcmpblnq0  7556  prarloclemcalc  7614  prarloc  7615  nqpru  7664  mullocpr  7683  distrlem4prl  7696  distrlem4pru  7697  ltprordil  7701  ltexprlemm  7712  ltexprlemopu  7715  ltexprlemupu  7716  ltexprlemru  7724  cauappcvgprlemopl  7758  cauappcvgprlem2  7772  caucvgprlemopl  7781  caucvgprlem2  7792  caucvgprprlemexbt  7818  caucvgprprlem2  7822  suplocexprlemloc  7833  suplocexprlemub  7835  suplocexprlemlub  7836  addcmpblnr  7851  mulcmpblnrlemg  7852  mulcmpblnr  7853  prsrlem1  7854  ltsrprg  7859  axmulcl  7978  ltmul1  8664  divdivdivap  8785  divmuleqap  8789  divsubdivap  8800  lt2mul2div  8951  ledivdiv  8962  lediv12a  8966  ssfzo12bi  10352  suprzcl2dc  10380  exbtwnz  10391  qbtwnre  10397  ioom  10401  seq3caopr  10638  seqcaoprg  10639  leexp2r  10736  hashunlem  10947  recvguniq  11277  rsqrmo  11309  fsum2dlemstep  11716  expcnvre  11785  fprod2dlemstep  11904  bezout  12303  qredeu  12390  pw2dvdseu  12461  oddpwdclemdvds  12463  pcqmul  12597  pcadd  12634  pockthg  12651  grprida  13190  issubmd  13277  ghmpreima  13573  unitgrp  13849  lmodprop2d  14081  lsspropdg  14164  neiint  14588  restbasg  14611  iscnp4  14661  cnpnei  14662  cnptopco  14665  blssps  14870  blss  14871  metequiv2  14939  xmetxpbl  14951  suplociccex  15068  dedekindicc  15076  limcimolemlt  15107  lgsquad2lem2  15530  2sqlem5  15567