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  11248  rsqrmo  11280  fsum2dlemstep  11687  expcnvre  11756  fprod2dlemstep  11875  bezout  12274  qredeu  12361  pw2dvdseu  12432  oddpwdclemdvds  12434  pcqmul  12568  pcadd  12605  pockthg  12622  grprida  13161  issubmd  13248  ghmpreima  13544  unitgrp  13820  lmodprop2d  14052  lsspropdg  14135  neiint  14559  restbasg  14582  iscnp4  14632  cnpnei  14633  cnptopco  14636  blssps  14841  blss  14842  metequiv2  14910  xmetxpbl  14922  suplociccex  15039  dedekindicc  15047  limcimolemlt  15078  lgsquad2lem2  15501  2sqlem5  15538