Theorem simplrl 541

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplrl	|- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	ad2antlr 493	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )

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:  rmob  3145  disjiun  4120  f1imass  5970  riota5f  6055  tfrexlem  6595  tfrcl  6625  nnsucuniel  6758  nntr2  6766  pw2f1odclem  7124  fopwdom  7126  fidceq  7161  fisbth  7177  fidcen  7193  fientri3  7212  unsnfidcex  7217  undifdc  7221  iunfidisj  7250  fiuni  7302  2omap  7308  ordiso2  7365  nninfninc  7453  acfun  7553  2omotaplemap  7613  ccfunen  7620  addcmpblnq  7724  mulcmpblnq  7725  ordpipqqs  7731  addcmpblnq0  7800  mulcmpblnq0  7801  prml  7834  addlocpr  7893  prmuloc  7923  mullocpr  7928  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemloc  7964  ltexprlemrl  7967  ltexprlemru  7969  addcanprleml  7971  addcanprlemu  7972  aptiprleml  7996  ltmprr  7999  cauappcvgprlemopl  8003  cauappcvgprlemopu  8005  cauappcvgprlemloc  8009  caucvgprlemopl  8026  caucvgprlemopu  8028  caucvgprlemloc  8032  caucvgprprlemopu  8056  caucvgprprlemloc  8060  caucvgprprlemexbt  8063  caucvgprprlemaddq  8065  suplocexprlemrl  8074  suplocexprlemdisj  8077  suplocexprlemloc  8078  suplocexprlemub  8080  addcmpblnr  8096  mulcmpblnrlemg  8097  mulcmpblnr  8098  ltsrprg  8104  mulgt0sr  8135  caucvgsrlemgt1  8152  suplocsrlemb  8163  axmulcl  8223  axcaucvglemres  8256  axpre-suploclemres  8258  axpre-suploc  8259  cnegexlem1  8491  negeu  8507  add20  8792  apreap  8905  cru  8920  apsym  8924  apcotr  8925  apadd1  8926  apneg  8929  mulext1  8930  mulge0  8937  mulap0  8972  divdivdivap  9033  prodgt0  9172  ltmul12a  9180  lt2mul2div  9199  ledivdiv  9210  lediv12a  9214  qapne  10018  xleadd1a  10254  ixxss12  10287  elfz0ubfz0  10510  qtri3or  10653  exbtwnzlemstep  10660  exbtwnzlemex  10662  exbtwnz  10663  rebtwn2zlemstep  10665  rebtwn2z  10667  btwnzge0  10713  iseqf1olemqf1o  10921  mulexpzap  10994  leexp1a  11009  hashen  11201  fihashdom  11221  hashun  11223  hashf1lem2  11264  swrdccatin1  11475  pfxccatin12lem3  11482  pfxccat3  11484  cjap  11650  cvg1nlemres  11729  rsqrmo  11771  abslt  11832  abs3lem  11855  cau3lem  11858  rexanre  11964  xrmaxltsup  12002  climcau  12091  sumeq2  12103  summodc  12128  fisumss  12137  fsum2d  12180  fsumabs  12210  fsumiun  12222  prodeq2  12302  prodmodclem2  12322  fprodcl2lem  12350  fprodap0  12366  fprod2d  12368  fprodrec  12374  fprodap0f  12381  fprodle  12385  eirrap  12523  divalglemeunn  12666  divalglemeuneg  12668  bezoutlemnewy  12751  bezoutlemstep  12752  bezoutlemmain  12753  bezoutlembi  12760  bezoutlemeu  12762  qredeu  12853  isprm5lem  12897  pw2dvdseu  12924  sqrt2irrap  12936  pythagtriplem2  13023  pythagtrip  13040  pclemub  13044  pcqmul  13060  pcexp  13066  pcneg  13082  pcprmpw2  13090  pcadd  13097  prmpwdvds  13112  4sqlem13m  13160  ballotfilemsf1o  13235  ennnfonelemg  13272  ennnfonelemrnh  13285  ctiunctlemfo  13308  nninfdclemf1  13321  imasival  13604  sgrppropd  13705  ismndd  13727  mndpropd  13730  mhmeql  13776  mhmmnd  13896  mulgfng  13904  issubg4m  13973  ssnmz  13991  conjnmzb  14060  gsumvalfi  14129  rngpropd  14229  ringpropd  14316  dvdsrtr  14381  aprlring  14573  islmod  14600  mplsubgfilemcl  15013  restbasg  15192  cnpnei  15243  cnptoprest2  15264  cnpdis  15266  lmtopcnp  15274  txcnp  15295  ismet2  15378  blininf  15448  metss2lem  15521  xmettxlem  15533  xmettx  15534  metcnp  15536  metcnpi3  15541  addcncntoplem  15585  fsumcncntop  15591  mulc1cncf  15613  cncfco  15615  mulcncf  15632  dedekindeulemuub  15641  dedekindeu  15647  dedekindicclemuub  15650  ivthinclemloc  15665  ivthinc  15667  limcimo  15689  limccnp2cntop  15701  dveflem  15750  plyf  15761  plyco  15783  plycj  15785  dvply2g  15790  logbgcd1irrap  15995  perfectlem2  16028  lgsdilem  16060  lgsquad2lem2  16115  lgsquad3  16117  2sqlem5  16152  2sqlem9  16157  usgredg4  16370  usgr1eop  16400  usgr1vr  16403  subuhgr  16427  subumgr  16429  subusgr  16430  clwwlknonex2lem2  16593  pw1map  16939  qdencn  16977  apdiff  17002  qdiff  17003