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  969  imain  5438  tfrlemisucaccv  6556  tfrexlem  6565  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  eroveu  6860  addcmpblnq  7682  mulcmpblnq  7683  ordpipqqs  7689  nqnq0pi  7753  addcmpblnq0  7758  mulcmpblnq0  7759  prarloclemcalc  7817  prarloc  7818  nqpru  7867  mullocpr  7886  distrlem4prl  7899  distrlem4pru  7900  ltprordil  7904  ltexprlemm  7915  ltexprlemopu  7918  ltexprlemupu  7919  ltexprlemru  7927  cauappcvgprlemopl  7961  cauappcvgprlem2  7975  caucvgprlemopl  7984  caucvgprlem2  7995  caucvgprprlemexbt  8021  caucvgprprlem2  8025  suplocexprlemloc  8036  suplocexprlemub  8038  suplocexprlemlub  8039  addcmpblnr  8054  mulcmpblnrlemg  8055  mulcmpblnr  8056  prsrlem1  8057  ltsrprg  8062  axmulcl  8181  ltmul1  8866  divdivdivap  8987  divmuleqap  8991  divsubdivap  9002  lt2mul2div  9153  ledivdiv  9164  lediv12a  9168  ssfzo12bi  10570  suprzcl2dc  10599  exbtwnz  10610  qbtwnre  10616  ioom  10620  seq3caopr  10857  seqcaoprg  10858  leexp2r  10955  hashunlem  11168  hashfibclem  11206  wrd2ind  11415  recvguniq  11680  rsqrmo  11712  fsum2dlemstep  12120  expcnvre  12189  fprod2dlemstep  12308  bezout  12707  qredeu  12794  pw2dvdseu  12865  oddpwdclemdvds  12867  pcqmul  13001  pcadd  13038  pockthg  13055  grprida  13600  issubmd  13687  ghmpreima  13983  unitgrp  14261  lmodprop2d  14496  lsspropdg  14579  neiint  15010  restbasg  15033  iscnp4  15083  cnpnei  15084  cnptopco  15087  blssps  15292  blss  15293  metequiv2  15361  xmetxpbl  15373  suplociccex  15490  dedekindicc  15498  limcimolemlt  15529  pellexlem3  15847  lgsquad2lem2  15955  2sqlem5  15992