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  966  imain  5403  tfrlemisucaccv  6477  tfrexlem  6486  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  eroveu  6781  addcmpblnq  7565  mulcmpblnq  7566  ordpipqqs  7572  nqnq0pi  7636  addcmpblnq0  7641  mulcmpblnq0  7642  prarloclemcalc  7700  prarloc  7701  nqpru  7750  mullocpr  7769  distrlem4prl  7782  distrlem4pru  7783  ltprordil  7787  ltexprlemm  7798  ltexprlemopu  7801  ltexprlemupu  7802  ltexprlemru  7810  cauappcvgprlemopl  7844  cauappcvgprlem2  7858  caucvgprlemopl  7867  caucvgprlem2  7878  caucvgprprlemexbt  7904  caucvgprprlem2  7908  suplocexprlemloc  7919  suplocexprlemub  7921  suplocexprlemlub  7922  addcmpblnr  7937  mulcmpblnrlemg  7938  mulcmpblnr  7939  prsrlem1  7940  ltsrprg  7945  axmulcl  8064  ltmul1  8750  divdivdivap  8871  divmuleqap  8875  divsubdivap  8886  lt2mul2div  9037  ledivdiv  9048  lediv12a  9052  ssfzo12bi  10443  suprzcl2dc  10471  exbtwnz  10482  qbtwnre  10488  ioom  10492  seq3caopr  10729  seqcaoprg  10730  leexp2r  10827  hashunlem  11038  wrd2ind  11270  recvguniq  11521  rsqrmo  11553  fsum2dlemstep  11960  expcnvre  12029  fprod2dlemstep  12148  bezout  12547  qredeu  12634  pw2dvdseu  12705  oddpwdclemdvds  12707  pcqmul  12841  pcadd  12878  pockthg  12895  grprida  13435  issubmd  13522  ghmpreima  13818  unitgrp  14095  lmodprop2d  14327  lsspropdg  14410  neiint  14834  restbasg  14857  iscnp4  14907  cnpnei  14908  cnptopco  14911  blssps  15116  blss  15117  metequiv2  15185  xmetxpbl  15197  suplociccex  15314  dedekindicc  15322  limcimolemlt  15353  lgsquad2lem2  15776  2sqlem5  15813