Theorem simprrl 534

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 108	. 2 |- ( ( ch /\ th ) -> ch )
2	1	ad2antll 488	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  dn1dc  955  imain  5280  tfrlemisucaccv  6304  tfrexlem  6313  tfr1onlemsucaccv  6320  tfrcllemsucaccv  6333  eroveu  6604  addcmpblnq  7329  mulcmpblnq  7330  ordpipqqs  7336  nqnq0pi  7400  addcmpblnq0  7405  mulcmpblnq0  7406  prarloclemcalc  7464  prarloc  7465  nqpru  7514  mullocpr  7533  distrlem4prl  7546  distrlem4pru  7547  ltprordil  7551  ltexprlemm  7562  ltexprlemopu  7565  ltexprlemupu  7566  ltexprlemru  7574  cauappcvgprlemopl  7608  cauappcvgprlem2  7622  caucvgprlemopl  7631  caucvgprlem2  7642  caucvgprprlemexbt  7668  caucvgprprlem2  7672  suplocexprlemloc  7683  suplocexprlemub  7685  suplocexprlemlub  7686  addcmpblnr  7701  mulcmpblnrlemg  7702  mulcmpblnr  7703  prsrlem1  7704  ltsrprg  7709  axmulcl  7828  ltmul1  8511  divdivdivap  8630  divmuleqap  8634  divsubdivap  8645  lt2mul2div  8795  ledivdiv  8806  lediv12a  8810  ssfzo12bi  10181  exbtwnz  10207  qbtwnre  10213  ioom  10217  seq3caopr  10439  leexp2r  10530  hashunlem  10739  recvguniq  10959  rsqrmo  10991  fsum2dlemstep  11397  expcnvre  11466  fprod2dlemstep  11585  suprzcl2dc  11910  bezout  11966  qredeu  12051  pw2dvdseu  12122  oddpwdclemdvds  12124  pcqmul  12257  pcadd  12293  pockthg  12309  grpridd  12641  issubmd  12696  neiint  12939  restbasg  12962  iscnp4  13012  cnpnei  13013  cnptopco  13016  blssps  13221  blss  13222  metequiv2  13290  xmetxpbl  13302  suplociccex  13397  dedekindicc  13405  limcimolemlt  13427  2sqlem5  13749