Theorem simplrl 530

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 108	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	ad2antlr 486	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  rmob  3047  disjiun  3984  f1imass  5753  riota5f  5833  tfrexlem  6313  tfrcl  6343  nnsucuniel  6474  nntr2  6482  fopwdom  6814  fidceq  6847  fisbth  6861  fientri3  6892  unsnfidcex  6897  undifdc  6901  iunfidisj  6923  fiuni  6955  ordiso2  7012  acfun  7184  ccfunen  7226  addcmpblnq  7329  mulcmpblnq  7330  ordpipqqs  7336  addcmpblnq0  7405  mulcmpblnq0  7406  prml  7439  addlocpr  7498  prmuloc  7528  mullocpr  7533  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemloc  7569  ltexprlemrl  7572  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  aptiprleml  7601  ltmprr  7604  cauappcvgprlemopl  7608  cauappcvgprlemopu  7610  cauappcvgprlemloc  7614  caucvgprlemopl  7631  caucvgprlemopu  7633  caucvgprlemloc  7637  caucvgprprlemopu  7661  caucvgprprlemloc  7665  caucvgprprlemexbt  7668  caucvgprprlemaddq  7670  suplocexprlemrl  7679  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  addcmpblnr  7701  mulcmpblnrlemg  7702  mulcmpblnr  7703  ltsrprg  7709  mulgt0sr  7740  caucvgsrlemgt1  7757  suplocsrlemb  7768  axmulcl  7828  axcaucvglemres  7861  axpre-suploclemres  7863  axpre-suploc  7864  cnegexlem1  8094  negeu  8110  add20  8393  apreap  8506  cru  8521  apsym  8525  apcotr  8526  apadd1  8527  apneg  8530  mulext1  8531  mulge0  8538  mulap0  8572  divdivdivap  8630  prodgt0  8768  ltmul12a  8776  lt2mul2div  8795  ledivdiv  8806  lediv12a  8810  qapne  9598  xleadd1a  9830  ixxss12  9863  elfz0ubfz0  10081  qtri3or  10199  exbtwnzlemstep  10204  exbtwnzlemex  10206  exbtwnz  10207  rebtwn2zlemstep  10209  rebtwn2z  10211  btwnzge0  10256  iseqf1olemqf1o  10449  mulexpzap  10516  leexp1a  10531  hashen  10718  fihashdom  10738  hashun  10740  cjap  10870  cvg1nlemres  10949  rsqrmo  10991  abslt  11052  abs3lem  11075  cau3lem  11078  rexanre  11184  xrmaxltsup  11221  climcau  11310  sumeq2  11322  summodc  11346  fisumss  11355  fsum2d  11398  fsumabs  11428  fsumiun  11440  prodeq2  11520  prodmodclem2  11540  fprodcl2lem  11568  fprodap0  11584  fprod2d  11586  fprodrec  11592  fprodap0f  11599  fprodle  11603  eirrap  11740  divalglemeunn  11880  divalglemeuneg  11882  bezoutlemnewy  11951  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlembi  11960  bezoutlemeu  11962  qredeu  12051  isprm5lem  12095  pw2dvdseu  12122  sqrt2irrap  12134  pythagtriplem2  12220  pythagtrip  12237  pclemub  12241  pcqmul  12257  pcexp  12263  pcneg  12278  pcprmpw2  12286  pcadd  12293  prmpwdvds  12307  ennnfonelemg  12358  ennnfonelemrnh  12371  ctiunctlemfo  12394  nninfdclemf1  12407  ismndd  12673  mndpropd  12676  mhmeql  12707  restbasg  12962  cnpnei  13013  cnptoprest2  13034  cnpdis  13036  lmtopcnp  13044  txcnp  13065  ismet2  13148  blininf  13218  metss2lem  13291  xmettxlem  13303  xmettx  13304  metcnp  13306  metcnpi3  13311  addcncntoplem  13345  fsumcncntop  13350  mulc1cncf  13370  cncfco  13372  mulcncf  13385  dedekindeulemuub  13389  dedekindeu  13395  dedekindicclemuub  13398  ivthinclemloc  13413  ivthinc  13415  limcimo  13428  limccnp2cntop  13440  dveflem  13481  logbgcd1irrap  13682  lgsdilem  13722  2sqlem5  13749  2sqlem9  13754  qdencn  14059  apdiff  14080