Theorem simplrl 535

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 489	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  3122  disjiun  4077  f1imass  5897  riota5f  5980  tfrexlem  6478  tfrcl  6508  nnsucuniel  6639  nntr2  6647  pw2f1odclem  6991  fopwdom  6993  fidceq  7027  fisbth  7041  fientri3  7073  unsnfidcex  7078  undifdc  7082  iunfidisj  7109  fiuni  7141  ordiso2  7198  nninfninc  7286  acfun  7385  2omotaplemap  7439  ccfunen  7446  addcmpblnq  7550  mulcmpblnq  7551  ordpipqqs  7557  addcmpblnq0  7626  mulcmpblnq0  7627  prml  7660  addlocpr  7719  prmuloc  7749  mullocpr  7754  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemloc  7790  ltexprlemrl  7793  ltexprlemru  7795  addcanprleml  7797  addcanprlemu  7798  aptiprleml  7822  ltmprr  7825  cauappcvgprlemopl  7829  cauappcvgprlemopu  7831  cauappcvgprlemloc  7835  caucvgprlemopl  7852  caucvgprlemopu  7854  caucvgprlemloc  7858  caucvgprprlemopu  7882  caucvgprprlemloc  7886  caucvgprprlemexbt  7889  caucvgprprlemaddq  7891  suplocexprlemrl  7900  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemub  7906  addcmpblnr  7922  mulcmpblnrlemg  7923  mulcmpblnr  7924  ltsrprg  7930  mulgt0sr  7961  caucvgsrlemgt1  7978  suplocsrlemb  7989  axmulcl  8049  axcaucvglemres  8082  axpre-suploclemres  8084  axpre-suploc  8085  cnegexlem1  8317  negeu  8333  add20  8617  apreap  8730  cru  8745  apsym  8749  apcotr  8750  apadd1  8751  apneg  8754  mulext1  8755  mulge0  8762  mulap0  8797  divdivdivap  8856  prodgt0  8995  ltmul12a  9003  lt2mul2div  9022  ledivdiv  9033  lediv12a  9037  qapne  9830  xleadd1a  10065  ixxss12  10098  elfz0ubfz0  10317  qtri3or  10455  exbtwnzlemstep  10462  exbtwnzlemex  10464  exbtwnz  10465  rebtwn2zlemstep  10467  rebtwn2z  10469  btwnzge0  10515  iseqf1olemqf1o  10723  mulexpzap  10796  leexp1a  10811  hashen  11001  fihashdom  11020  hashun  11022  swrdccatin1  11252  pfxccatin12lem3  11259  pfxccat3  11261  cjap  11412  cvg1nlemres  11491  rsqrmo  11533  abslt  11594  abs3lem  11617  cau3lem  11620  rexanre  11726  xrmaxltsup  11764  climcau  11853  sumeq2  11865  summodc  11889  fisumss  11898  fsum2d  11941  fsumabs  11971  fsumiun  11983  prodeq2  12063  prodmodclem2  12083  fprodcl2lem  12111  fprodap0  12127  fprod2d  12129  fprodrec  12135  fprodap0f  12142  fprodle  12146  eirrap  12284  divalglemeunn  12427  divalglemeuneg  12429  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlemmain  12514  bezoutlembi  12521  bezoutlemeu  12523  qredeu  12614  isprm5lem  12658  pw2dvdseu  12685  sqrt2irrap  12697  pythagtriplem2  12784  pythagtrip  12801  pclemub  12805  pcqmul  12821  pcexp  12827  pcneg  12843  pcprmpw2  12851  pcadd  12858  prmpwdvds  12873  4sqlem13m  12921  ennnfonelemg  12969  ennnfonelemrnh  12982  ctiunctlemfo  13005  nninfdclemf1  13018  imasival  13334  sgrppropd  13441  ismndd  13465  mndpropd  13468  mhmeql  13520  mhmmnd  13648  mulgfng  13656  issubg4m  13725  ssnmz  13743  conjnmzb  13812  rngpropd  13913  ringpropd  13996  dvdsrtr  14059  islmod  14249  mplsubgfilemcl  14657  restbasg  14836  cnpnei  14887  cnptoprest2  14908  cnpdis  14910  lmtopcnp  14918  txcnp  14939  ismet2  15022  blininf  15092  metss2lem  15165  xmettxlem  15177  xmettx  15178  metcnp  15180  metcnpi3  15185  addcncntoplem  15229  fsumcncntop  15235  mulc1cncf  15257  cncfco  15259  mulcncf  15276  dedekindeulemuub  15285  dedekindeu  15291  dedekindicclemuub  15294  ivthinclemloc  15309  ivthinc  15311  limcimo  15333  limccnp2cntop  15345  dveflem  15394  plyf  15405  plyco  15427  plycj  15429  dvply2g  15434  logbgcd1irrap  15638  perfectlem2  15668  lgsdilem  15700  lgsquad2lem2  15755  lgsquad3  15757  2sqlem5  15792  2sqlem9  15797  usgredg4  16007  2omap  16318  pw1map  16320  qdencn  16354  apdiff  16375