Theorem syl5eqr 2825

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl5eqr.1	⊢ 𝐵 = 𝐴
syl5eqr.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
syl5eqr	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem syl5eqr

Step	Hyp	Ref	Expression
1		syl5eqr.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2784	. 2 ⊢ 𝐴 = 𝐵
3		syl5eqr.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5eq 2823	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-9 2057  ax-ext 2747

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2768

This theorem is referenced by:  3eqtr3g  2834  csbeq1a  3794  ssdifeq0  4313  pofun  5340  opabbi2dv  5567  cnvsng  5917  funcnvpr  6247  funcnvtp  6248  funcnvqp  6249  fresin  6374  fresaunres2  6377  f1imacnv  6458  foimacnv  6459  funfv  6576  dffv2  6582  fimacnvinrn  6663  fsn2  6719  funiunfvf  6831  fcof1oinvd  6872  riotaxfrd  6966  f1opw2  7216  fnexALT  7462  fparlem3  7614  fparlem4  7615  mpocurryd  7735  seqomlem1  7886  seqomlem4  7889  oasuc  7947  oesuclem  7948  omsuc  7949  onasuc  7951  onmsuc  7952  eqerlem  8119  pmresg  8230  fopwdom  8417  sbthlem8  8426  sbthlem9  8427  fodomr  8460  domss2  8468  mapen  8473  enp1i  8544  xpfi  8580  fiint  8586  f1opwfi  8619  mapfien  8662  marypha1lem  8688  unxpwdom  8844  cantnfval2  8922  infxpenlem  9229  djuinf  9408  isf34lem3  9591  isf34lem5  9594  axdc4lem  9671  ttukeylem6  9730  rankcf  9993  tskuni  9999  gruima  10018  dmrecnq  10184  ltexnq  10191  reclem3pr  10265  pn0sr  10317  mulgt0sr  10321  recdiv  11143  2resupmax  12395  max0sub  12403  rexmul  12477  xmulmnf1  12482  xmulm1  12487  prunioo  12680  fseq1p1m1  12794  fzshftral  12808  seqp1i  13198  seqf1olem2  13222  seqfeq4  13231  binom3  13397  expmulnbnd  13408  discr  13413  bcn2  13491  hashun2  13554  hashun3  13555  hashdif  13582  hashgt12el  13591  hashgt12el2  13592  hashfacen  13619  wrdeqs1catOLD  13907  swrdccat3aOLD  13937  s2prop  14125  s4prop  14128  s3sndisj  14182  s3iunsndisj  14183  cnrecnv  14379  rddif  14555  amgm2  14584  rlimres  14770  lo1res  14771  iseraltlem2  14894  iseralt  14896  fsumss  14936  fsumcl2lem  14942  isumclim3  14968  fsumcnv  14982  telfsumo  15011  fsumiun  15030  arisum2  15070  geoisum1c  15090  fprodss  15156  fprodser  15157  fprodcl2lem  15158  fprodsplit  15174  fprodn0  15187  fprodcnv  15191  iprodclim3  15208  risefac1  15241  fallfac1  15242  bpolyval  15257  bpoly3  15266  bpoly4  15267  fsumcube  15268  sinhval  15361  cos01bnd  15393  ruclem6  15442  sadadd2lem2  15653  eucalgval  15776  pcid  16059  prmreclem4  16105  4sqlem15  16145  4sqlem16  16146  ramcl  16215  strfv2d  16379  setsid  16388  imasvscafn  16660  xpsc0  16683  xpsc1  16684  xpsff1o  16691  xpsaddlem  16698  xpsvsca  16702  xpsle  16704  mreexexlem2d  16768  mreexexlem4d  16770  sscres  16945  xpcid  17291  evlfcllem  17323  hofcl  17361  isacs5lem  17631  frmdup3lem  17866  cayleylem2  18296  f1omvdco2  18331  symggen  18353  psgnunilem1  18376  pgp0  18476  sylow3lem2  18508  lsmdisjr  18562  lsmdisj2r  18563  subgdisj2  18570  efgval  18595  frgpuplem  18652  frgpup2  18656  gsumval3  18775  gsumzres  18777  gsum2d2lem  18840  dprdf1  18899  dmdprdsplit2lem  18911  dmdprdsplit2  18912  ablfaclem3  18953  prdsmgp  19077  unitgrp  19134  subdrgint  19298  crng2idl  19727  psrass1lem  19865  evl1var  20195  pf1mpf  20211  pf1ind  20214  gsumfsum  20308  chrid  20370  znleval  20397  ocv1  20519  frlmip  20618  ellspd  20642  mamuvs2  20713  madurid  20951  baspartn  21260  mretopd  21398  ordtcld1  21503  ordtcld2  21504  leordtvallem1  21516  leordtvallem2  21517  paste  21600  imacmp  21703  cmpsub  21706  unconn  21735  1stckgen  21860  ptbasfi  21887  txcld  21909  ptclsg  21921  txdis1cn  21941  ptrescn  21945  hausdiag  21951  txkgen  21958  xkoptsub  21960  xkococnlem  21965  cnmpt21  21977  cnmpt22  21980  tgqtop  22018  qtoprest  22023  kqdisj  22038  hmeores  22077  hmphindis  22103  pt1hmeo  22112  ptuncnv  22113  ptunhmeo  22114  xpstopnlem1  22115  xkohmeo  22121  alexsublem  22350  ptcmplem2  22359  tmdcn2  22395  cldsubg  22416  qustgplem  22426  tsmsres  22449  ustbas2  22531  ressuss  22569  metreslem  22669  xpsdsval  22688  prdsxmslem2  22836  txmetcnp  22854  tngngp  22960  nrmtngdist  22963  remetdval  23094  cnheibor  23256  evth2  23261  pcoass  23325  ncvspi  23457  iscmet3  23593  rrxip  23690  minveclem2  23726  cmmbl  23832  nulmbl2  23834  volinun  23844  voliunlem1  23848  volsup  23854  ovolioo  23866  uniiccdif  23876  uniioombllem2  23881  uniioombllem3  23883  uniioombllem4  23884  uniioombllem5  23885  ismbf3d  23952  itg2uba  24041  itg2i1fseq  24053  itgsplitioo  24135  limcflf  24176  cnplimc  24182  limcun  24190  dvfval  24192  dvres  24206  dvres3a  24209  dvnp1  24219  dvn1  24220  dvexp3  24272  dvsincos  24275  mvth  24286  c1lip2  24292  dvfsumlem2  24321  itgsubstlem  24342  itgsubst  24343  coeeq2  24529  dgreq0  24552  dgrcolem2  24561  vieta1  24598  ulm2  24670  radcnv0  24701  abelthlem2  24717  tanarg  24897  advlogexp  24933  efopn  24936  logtayl  24938  cxpcn3  25024  ang180lem3  25084  quad2  25112  mcubic  25120  binom4  25123  dquart  25126  quart1lem  25128  quart1  25129  quartlem1  25130  asinlem3a  25143  efiatan  25185  tanatan  25192  atanbndlem  25198  dvatan  25208  ftalem3  25348  ftalem5  25350  basellem3  25356  mumullem2  25453  musum  25464  chtublem  25483  perfectlem2  25502  bposlem6  25561  bposlem9  25564  1lgs  25612  lgs1  25613  lgseisenlem1  25647  lgseisenlem2  25648  lgseisenlem3  25649  lgsquadlem2  25653  lgsquad2lem2  25657  2sqblem  25703  rpvmasum2  25784  log2sumbnd  25816  opphllem3  26231  vtxdun  26960  clwwlknon2num  27627  eucrct2eupthOLD  27770  eucrct2eupth  27771  nvpi  28215  nvop  28224  phop  28366  minvecolem2  28424  hi01  28646  pjchi  28984  chjidm  29072  mayete3i  29280  ho0val  29302  lnop0  29518  adjbdlnb  29636  pjin2i  29745  mdslmd3i  29884  mdexchi  29887  imadifxp  30111  fcoinver  30115  suppovss  30181  padct  30201  f1od2  30203  fcobijfs  30205  ffsrn  30211  iocinif  30250  difioo  30251  s2rn  30356  s3rn  30358  cycpm2tr  30442  gsummpt2co  30514  ofldchr  30557  rgmoddim  30628  lindsun  30641  dimkerim  30643  fldexttr  30668  symgfcoeu  30678  pmtrprfv2  30680  smatlem  30695  fvproj  30731  indf1ofs  30920  esumpad2  30950  hasheuni  30979  esumcvg2  30981  esum2dlem  30986  sigapildsys  31057  measxun2  31105  measunl  31111  measinblem  31115  carsgclctunlem1  31211  carsgclctunlem3  31214  sibfof  31234  sitgclg  31236  eulerpartlemgf  31273  probdif  31315  cndprobval  31328  ballotlemic  31401  signsvtn0  31477  signsvtn0OLD  31478  signstres  31483  chtvalz  31539  hgt750lemd  31558  bnj1415  31946  subfacp1lem1  32001  subfacp1lem3  32004  subfacp1lem5  32006  cvmscld  32095  cvmlift2lem9a  32125  cvmlift2lem9  32133  noetalem3  32710  fwddifnp1  33117  csbpredg  34014  finxpreclem5  34082  ptrest  34310  poimirlem2  34313  poimirlem3  34314  poimirlem6  34317  poimirlem7  34318  poimirlem9  34320  poimirlem11  34322  poimirlem12  34323  poimirlem16  34327  poimirlem17  34328  poimirlem19  34330  poimirlem20  34331  poimirlem24  34335  poimirlem25  34336  poimirlem27  34338  poimirlem28  34339  poimirlem29  34340  poimirlem31  34342  voliunnfl  34355  volsupnfl  34356  mbfresfi  34357  itg2addnclem2  34363  itg2addnclem3  34364  ftc1anclem5  34390  dvacos  34398  areacirclem5  34405  cocnv  34420  istotbnd3  34469  ssbnd  34486  eccnvepres3  34964  symrelim  35218  osumcllem9N  36523  4atexlemex2  36630  cdleme20j  36877  cdlemg47  37295  diaintclN  37617  dibintclN  37726  dihintcl  37903  lclkrlem2e  38070  lclkrlem2p  38081  lcfrlem31  38132  diophin  38743  monotuz  38912  monotoddzzfi  38913  oddcomabszz  38915  fnwe2val  39023  lnmlmic  39062  fiuneneq  39171  cytpval  39183  ntrkbimka  39729  ntrneifv2  39771  radcnvrat  40039  nzprmdif  40044  binomcxplemnotnn0  40081  ioccncflimc  41577  icocncflimc  41581  stoweidlem50  41745  fourierdlem89  41890  fourierdlem90  41891  fourierdlem91  41892  fourierdlem107  41908  elsprel  42979  reuopreuprim  43030  perfectALTVlem2  43229  logb2aval  44204  aacllem  44243