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  963  imain  5370  tfrlemisucaccv  6429  tfrexlem  6438  tfr1onlemsucaccv  6445  tfrcllemsucaccv  6458  eroveu  6731  addcmpblnq  7510  mulcmpblnq  7511  ordpipqqs  7517  nqnq0pi  7581  addcmpblnq0  7586  mulcmpblnq0  7587  prarloclemcalc  7645  prarloc  7646  nqpru  7695  mullocpr  7714  distrlem4prl  7727  distrlem4pru  7728  ltprordil  7732  ltexprlemm  7743  ltexprlemopu  7746  ltexprlemupu  7747  ltexprlemru  7755  cauappcvgprlemopl  7789  cauappcvgprlem2  7803  caucvgprlemopl  7812  caucvgprlem2  7823  caucvgprprlemexbt  7849  caucvgprprlem2  7853  suplocexprlemloc  7864  suplocexprlemub  7866  suplocexprlemlub  7867  addcmpblnr  7882  mulcmpblnrlemg  7883  mulcmpblnr  7884  prsrlem1  7885  ltsrprg  7890  axmulcl  8009  ltmul1  8695  divdivdivap  8816  divmuleqap  8820  divsubdivap  8831  lt2mul2div  8982  ledivdiv  8993  lediv12a  8997  ssfzo12bi  10386  suprzcl2dc  10414  exbtwnz  10425  qbtwnre  10431  ioom  10435  seq3caopr  10672  seqcaoprg  10673  leexp2r  10770  hashunlem  10981  wrd2ind  11209  recvguniq  11391  rsqrmo  11423  fsum2dlemstep  11830  expcnvre  11899  fprod2dlemstep  12018  bezout  12417  qredeu  12504  pw2dvdseu  12575  oddpwdclemdvds  12577  pcqmul  12711  pcadd  12748  pockthg  12765  grprida  13304  issubmd  13391  ghmpreima  13687  unitgrp  13963  lmodprop2d  14195  lsspropdg  14278  neiint  14702  restbasg  14725  iscnp4  14775  cnpnei  14776  cnptopco  14779  blssps  14984  blss  14985  metequiv2  15053  xmetxpbl  15065  suplociccex  15182  dedekindicc  15190  limcimolemlt  15221  lgsquad2lem2  15644  2sqlem5  15681