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  5419  tfrlemisucaccv  6534  tfrexlem  6543  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  eroveu  6838  addcmpblnq  7630  mulcmpblnq  7631  ordpipqqs  7637  nqnq0pi  7701  addcmpblnq0  7706  mulcmpblnq0  7707  prarloclemcalc  7765  prarloc  7766  nqpru  7815  mullocpr  7834  distrlem4prl  7847  distrlem4pru  7848  ltprordil  7852  ltexprlemm  7863  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemru  7875  cauappcvgprlemopl  7909  cauappcvgprlem2  7923  caucvgprlemopl  7932  caucvgprlem2  7943  caucvgprprlemexbt  7969  caucvgprprlem2  7973  suplocexprlemloc  7984  suplocexprlemub  7986  suplocexprlemlub  7987  addcmpblnr  8002  mulcmpblnrlemg  8003  mulcmpblnr  8004  prsrlem1  8005  ltsrprg  8010  axmulcl  8129  ltmul1  8814  divdivdivap  8935  divmuleqap  8939  divsubdivap  8950  lt2mul2div  9101  ledivdiv  9112  lediv12a  9116  ssfzo12bi  10516  suprzcl2dc  10545  exbtwnz  10556  qbtwnre  10562  ioom  10566  seq3caopr  10803  seqcaoprg  10804  leexp2r  10901  hashunlem  11113  wrd2ind  11353  recvguniq  11618  rsqrmo  11650  fsum2dlemstep  12058  expcnvre  12127  fprod2dlemstep  12246  bezout  12645  qredeu  12732  pw2dvdseu  12803  oddpwdclemdvds  12805  pcqmul  12939  pcadd  12976  pockthg  12993  grprida  13533  issubmd  13620  ghmpreima  13916  unitgrp  14194  lmodprop2d  14427  lsspropdg  14510  neiint  14939  restbasg  14962  iscnp4  15012  cnpnei  15013  cnptopco  15016  blssps  15221  blss  15222  metequiv2  15290  xmetxpbl  15302  suplociccex  15419  dedekindicc  15427  limcimolemlt  15458  pellexlem3  15776  lgsquad2lem2  15884  2sqlem5  15921