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  3091  disjiun  4039  f1imass  5843  riota5f  5924  tfrexlem  6420  tfrcl  6450  nnsucuniel  6581  nntr2  6589  pw2f1odclem  6931  fopwdom  6933  fidceq  6966  fisbth  6980  fientri3  7012  unsnfidcex  7017  undifdc  7021  iunfidisj  7048  fiuni  7080  ordiso2  7137  nninfninc  7225  acfun  7319  2omotaplemap  7369  ccfunen  7376  addcmpblnq  7480  mulcmpblnq  7481  ordpipqqs  7487  addcmpblnq0  7556  mulcmpblnq0  7557  prml  7590  addlocpr  7649  prmuloc  7679  mullocpr  7684  ltexprlemopl  7714  ltexprlemopu  7716  ltexprlemloc  7720  ltexprlemrl  7723  ltexprlemru  7725  addcanprleml  7727  addcanprlemu  7728  aptiprleml  7752  ltmprr  7755  cauappcvgprlemopl  7759  cauappcvgprlemopu  7761  cauappcvgprlemloc  7765  caucvgprlemopl  7782  caucvgprlemopu  7784  caucvgprlemloc  7788  caucvgprprlemopu  7812  caucvgprprlemloc  7816  caucvgprprlemexbt  7819  caucvgprprlemaddq  7821  suplocexprlemrl  7830  suplocexprlemdisj  7833  suplocexprlemloc  7834  suplocexprlemub  7836  addcmpblnr  7852  mulcmpblnrlemg  7853  mulcmpblnr  7854  ltsrprg  7860  mulgt0sr  7891  caucvgsrlemgt1  7908  suplocsrlemb  7919  axmulcl  7979  axcaucvglemres  8012  axpre-suploclemres  8014  axpre-suploc  8015  cnegexlem1  8247  negeu  8263  add20  8547  apreap  8660  cru  8675  apsym  8679  apcotr  8680  apadd1  8681  apneg  8684  mulext1  8685  mulge0  8692  mulap0  8727  divdivdivap  8786  prodgt0  8925  ltmul12a  8933  lt2mul2div  8952  ledivdiv  8963  lediv12a  8967  qapne  9760  xleadd1a  9995  ixxss12  10028  elfz0ubfz0  10247  qtri3or  10383  exbtwnzlemstep  10390  exbtwnzlemex  10392  exbtwnz  10393  rebtwn2zlemstep  10395  rebtwn2z  10397  btwnzge0  10443  iseqf1olemqf1o  10651  mulexpzap  10724  leexp1a  10739  hashen  10929  fihashdom  10948  hashun  10950  cjap  11217  cvg1nlemres  11296  rsqrmo  11338  abslt  11399  abs3lem  11422  cau3lem  11425  rexanre  11531  xrmaxltsup  11569  climcau  11658  sumeq2  11670  summodc  11694  fisumss  11703  fsum2d  11746  fsumabs  11776  fsumiun  11788  prodeq2  11868  prodmodclem2  11888  fprodcl2lem  11916  fprodap0  11932  fprod2d  11934  fprodrec  11940  fprodap0f  11947  fprodle  11951  eirrap  12089  divalglemeunn  12232  divalglemeuneg  12234  bezoutlemnewy  12317  bezoutlemstep  12318  bezoutlemmain  12319  bezoutlembi  12326  bezoutlemeu  12328  qredeu  12419  isprm5lem  12463  pw2dvdseu  12490  sqrt2irrap  12502  pythagtriplem2  12589  pythagtrip  12606  pclemub  12610  pcqmul  12626  pcexp  12632  pcneg  12648  pcprmpw2  12656  pcadd  12663  prmpwdvds  12678  4sqlem13m  12726  ennnfonelemg  12774  ennnfonelemrnh  12787  ctiunctlemfo  12810  nninfdclemf1  12823  imasival  13138  sgrppropd  13245  ismndd  13269  mndpropd  13272  mhmeql  13324  mhmmnd  13452  mulgfng  13460  issubg4m  13529  ssnmz  13547  conjnmzb  13616  rngpropd  13717  ringpropd  13800  dvdsrtr  13863  islmod  14053  mplsubgfilemcl  14461  restbasg  14640  cnpnei  14691  cnptoprest2  14712  cnpdis  14714  lmtopcnp  14722  txcnp  14743  ismet2  14826  blininf  14896  metss2lem  14969  xmettxlem  14981  xmettx  14982  metcnp  14984  metcnpi3  14989  addcncntoplem  15033  fsumcncntop  15039  mulc1cncf  15061  cncfco  15063  mulcncf  15080  dedekindeulemuub  15089  dedekindeu  15095  dedekindicclemuub  15098  ivthinclemloc  15113  ivthinc  15115  limcimo  15137  limccnp2cntop  15149  dveflem  15198  plyf  15209  plyco  15231  plycj  15233  dvply2g  15238  logbgcd1irrap  15442  perfectlem2  15472  lgsdilem  15504  lgsquad2lem2  15559  lgsquad3  15561  2sqlem5  15596  2sqlem9  15601  2omap  15932  qdencn  15966  apdiff  15987