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  968  imain  5412  tfrlemisucaccv  6491  tfrexlem  6500  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  eroveu  6795  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  nqnq0pi  7658  addcmpblnq0  7663  mulcmpblnq0  7664  prarloclemcalc  7722  prarloc  7723  nqpru  7772  mullocpr  7791  distrlem4prl  7804  distrlem4pru  7805  ltprordil  7809  ltexprlemm  7820  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemru  7832  cauappcvgprlemopl  7866  cauappcvgprlem2  7880  caucvgprlemopl  7889  caucvgprlem2  7900  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  prsrlem1  7962  ltsrprg  7967  axmulcl  8086  ltmul1  8772  divdivdivap  8893  divmuleqap  8897  divsubdivap  8908  lt2mul2div  9059  ledivdiv  9070  lediv12a  9074  ssfzo12bi  10471  suprzcl2dc  10500  exbtwnz  10511  qbtwnre  10517  ioom  10521  seq3caopr  10758  seqcaoprg  10759  leexp2r  10856  hashunlem  11068  wrd2ind  11308  recvguniq  11573  rsqrmo  11605  fsum2dlemstep  12013  expcnvre  12082  fprod2dlemstep  12201  bezout  12600  qredeu  12687  pw2dvdseu  12758  oddpwdclemdvds  12760  pcqmul  12894  pcadd  12931  pockthg  12948  grprida  13488  issubmd  13575  ghmpreima  13871  unitgrp  14149  lmodprop2d  14381  lsspropdg  14464  neiint  14888  restbasg  14911  iscnp4  14961  cnpnei  14962  cnptopco  14965  blssps  15170  blss  15171  metequiv2  15239  xmetxpbl  15251  suplociccex  15368  dedekindicc  15376  limcimolemlt  15407  lgsquad2lem2  15830  2sqlem5  15867