Theorem simprrl 545

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 495	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  dn1dc  973  imain  5463  tfrlemisucaccv  6596  tfrexlem  6605  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  eroveu  6900  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  nqnq0pi  7805  addcmpblnq0  7810  mulcmpblnq0  7811  prarloclemcalc  7869  prarloc  7870  nqpru  7919  mullocpr  7938  distrlem4prl  7951  distrlem4pru  7952  ltprordil  7956  ltexprlemm  7967  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemru  7979  cauappcvgprlemopl  8013  cauappcvgprlem2  8027  caucvgprlemopl  8036  caucvgprlem2  8047  caucvgprprlemexbt  8073  caucvgprprlem2  8077  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  prsrlem1  8109  ltsrprg  8114  axmulcl  8233  ltmul1  8920  divdivdivap  9043  divmuleqap  9047  divsubdivap  9058  lt2mul2div  9209  ledivdiv  9220  lediv12a  9224  ssfzo12bi  10643  infssfzcldc  10669  infssfzledc  10670  suprzcl2dc  10674  exbtwnz  10685  qbtwnre  10691  ioom  10695  seq3caopr  10932  seqcaoprg  10933  leexp2r  11030  hashunlem  11244  hashfibclem  11282  wrd2ind  11495  recvguniq  11761  rsqrmo  11793  fsum2dlemstep  12201  expcnvre  12270  fprod2dlemstep  12389  bezout  12788  qredeu  12875  pw2dvdseu  12946  oddpwdclemdvds  12948  pcqmul  13082  pcadd  13119  pockthg  13136  grprida  13707  issubmd  13781  ghmpreima  14069  unitgrp  14423  lmodprop2d  14685  lsspropdg  14768  assapropd  15014  neiint  15246  restbasg  15269  iscnp4  15319  cnpnei  15320  cnptopco  15323  blssps  15528  blss  15529  metequiv2  15597  xmetxpbl  15609  suplociccex  15726  dedekindicc  15734  limcimolemlt  15765  pellexlem3  16093  lgsquad2lem2  16201  2sqlem5  16238