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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  rmob  3145  disjiun  4125  f1imass  5980  riota5f  6065  tfrexlem  6605  tfrcl  6635  nnsucuniel  6768  nntr2  6776  pw2f1odclem  7134  fopwdom  7136  fidceq  7171  fisbth  7187  fidcen  7203  fientri3  7222  unsnfidcex  7227  undifdc  7231  iunfidisj  7260  fiuni  7312  2omap  7319  ordiso2  7376  nninfninc  7464  acfun  7564  2omotaplemap  7624  ccfunen  7631  addcmpblnq  7735  mulcmpblnq  7736  ordpipqqs  7742  addcmpblnq0  7811  mulcmpblnq0  7812  prml  7845  addlocpr  7904  prmuloc  7934  mullocpr  7939  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemloc  7975  ltexprlemrl  7978  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  aptiprleml  8007  ltmprr  8010  cauappcvgprlemopl  8014  cauappcvgprlemopu  8016  cauappcvgprlemloc  8020  caucvgprlemopl  8037  caucvgprlemopu  8039  caucvgprlemloc  8043  caucvgprprlemopu  8067  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  caucvgprprlemaddq  8076  suplocexprlemrl  8085  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  addcmpblnr  8107  mulcmpblnrlemg  8108  mulcmpblnr  8109  ltsrprg  8115  mulgt0sr  8146  caucvgsrlemgt1  8163  suplocsrlemb  8174  axmulcl  8234  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  cnegexlem1  8503  negeu  8519  add20  8804  apreap  8918  cru  8933  apsym  8937  apcotr  8938  apadd1  8939  apneg  8942  mulext1  8943  mulge0  8950  mulap0  8985  divdivdivap  9046  prodgt0  9185  ltmul12a  9193  lt2mul2div  9212  ledivdiv  9223  lediv12a  9227  qapne  10049  xleadd1a  10286  ixxss12  10319  elfz0ubfz0  10543  qtri3or  10686  exbtwnzlemstep  10693  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2z  10700  btwnzge0  10750  iseqf1olemqf1o  10958  mulexpzap  11031  leexp1a  11046  hashen  11239  fihashdom  11259  hashun  11261  hashf1lem2  11302  swrdccatin1  11513  pfxccatin12lem3  11520  pfxccat3  11522  cjap  11688  cvg1nlemres  11767  rsqrmo  11809  abslt  11871  abs3lem  11894  cau3lem  11897  rexanre  12003  xrmaxltsup  12043  climcau  12132  sumeq2  12144  summodc  12169  fisumss  12178  fsum2d  12221  fsumabs  12251  fsumiun  12263  prodeq2  12343  prodmodclem2  12363  fprodcl2lem  12391  fprodap0  12407  fprod2d  12409  fprodrec  12415  fprodap0f  12422  fprodle  12426  eirrap  12564  divalglemeunn  12707  divalglemeuneg  12709  bezoutlemnewy  12792  bezoutlemstep  12793  bezoutlemmain  12794  bezoutlembi  12801  bezoutlemeu  12803  qredeu  12894  isprm5lem  12939  pwbdvdseu  12966  sqrt2irrap  12979  pythagtriplem2  13068  pythagtrip  13085  pclemub  13089  pcqmul  13105  pcexp  13111  pcneg  13127  pcprmpw2  13135  pcadd  13142  prmpwdvds  13157  4sqlem13m  13205  ballotfilemsf1o  13309  ennnfonelemg  13346  ennnfonelemrnh  13359  ctiunctlemfo  13382  nninfdclemf1  13395  imasival  13680  sgrppropd  13781  ismndd  13803  mndpropd  13806  mhmeql  13852  mhmmnd  13972  mulgfng  13980  issubg4m  14049  ssnmz  14067  conjnmzb  14136  gsumvalfi  14236  rngpropd  14338  ringpropd  14427  dvdsrtr  14492  aprlring  14684  islmod  14711  assapropd  15098  psrbaglefifi  15147  mplsubgfilemcl  15181  restbasg  15360  cnpnei  15411  cnptoprest2  15432  cnpdis  15434  lmtopcnp  15442  txcnp  15463  ismet2  15546  blininf  15616  metss2lem  15689  xmettxlem  15701  xmettx  15702  metcnp  15704  metcnpi3  15709  addcncntoplem  15753  fsumcncntop  15759  mulc1cncf  15781  cncfco  15783  mulcncf  15800  dedekindeulemuub  15809  dedekindeu  15815  dedekindicclemuub  15818  ivthinclemloc  15833  ivthinc  15835  limcimo  15857  limccnp2cntop  15869  dveflem  15918  plyf  15929  plyco  15951  plycj  15953  dvply2g  15958  logbgcd1irrap  16167  zprmlogbap  16179  perfectlem2  16261  lgsdilem  16312  lgsquad2lem2  16367  lgsquad3  16369  2sqlem5  16404  2sqlem9  16409  usgredg4  16622  usgr1eop  16652  usgr1vr  16655  subuhgr  16679  subumgr  16681  subusgr  16682  clwwlknonex2lem2  16845  pw1map  17191  qdencn  17238  apdiff  17264  qdiff  17265