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  968  imain  5412  tfrlemisucaccv  6490  tfrexlem  6499  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  eroveu  6794  addcmpblnq  7586  mulcmpblnq  7587  ordpipqqs  7593  nqnq0pi  7657  addcmpblnq0  7662  mulcmpblnq0  7663  prarloclemcalc  7721  prarloc  7722  nqpru  7771  mullocpr  7790  distrlem4prl  7803  distrlem4pru  7804  ltprordil  7808  ltexprlemm  7819  ltexprlemopu  7822  ltexprlemupu  7823  ltexprlemru  7831  cauappcvgprlemopl  7865  cauappcvgprlem2  7879  caucvgprlemopl  7888  caucvgprlem2  7899  caucvgprprlemexbt  7925  caucvgprprlem2  7929  suplocexprlemloc  7940  suplocexprlemub  7942  suplocexprlemlub  7943  addcmpblnr  7958  mulcmpblnrlemg  7959  mulcmpblnr  7960  prsrlem1  7961  ltsrprg  7966  axmulcl  8085  ltmul1  8771  divdivdivap  8892  divmuleqap  8896  divsubdivap  8907  lt2mul2div  9058  ledivdiv  9069  lediv12a  9073  ssfzo12bi  10469  suprzcl2dc  10498  exbtwnz  10509  qbtwnre  10515  ioom  10519  seq3caopr  10756  seqcaoprg  10757  leexp2r  10854  hashunlem  11066  wrd2ind  11303  recvguniq  11555  rsqrmo  11587  fsum2dlemstep  11994  expcnvre  12063  fprod2dlemstep  12182  bezout  12581  qredeu  12668  pw2dvdseu  12739  oddpwdclemdvds  12741  pcqmul  12875  pcadd  12912  pockthg  12929  grprida  13469  issubmd  13556  ghmpreima  13852  unitgrp  14129  lmodprop2d  14361  lsspropdg  14444  neiint  14868  restbasg  14891  iscnp4  14941  cnpnei  14942  cnptopco  14945  blssps  15150  blss  15151  metequiv2  15219  xmetxpbl  15231  suplociccex  15348  dedekindicc  15356  limcimolemlt  15387  lgsquad2lem2  15810  2sqlem5  15847