Theorem syl5eqr 2870

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 2830	. 2 ⊢ 𝐴 = 𝐵
3		syl5eqr.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5eq 2868	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  3eqtr3g  2879  csbeq1a  3897  ssdifeq0  4432  pofun  5491  opabbi2dv  5720  cnvsng  6080  funcnvpr  6416  funcnvtp  6417  funcnvqp  6418  fresin  6547  fresaunres2  6550  f1imacnv  6631  foimacnv  6632  funfv  6750  dffv2  6756  fimacnvinrn  6840  fsn2  6898  funiunfvf  7008  fcof1oinvd  7049  riotaxfrd  7148  f1opw2  7400  fnexALT  7652  fparlem3  7809  fparlem4  7810  fsplitfpar  7814  fvproj  7828  mpocurryd  7935  seqomlem1  8086  seqomlem4  8089  oasuc  8149  oesuclem  8150  omsuc  8151  onasuc  8153  onmsuc  8154  eqerlem  8323  pmresg  8434  fopwdom  8625  sbthlem8  8634  sbthlem9  8635  fodomr  8668  domss2  8676  mapen  8681  enp1i  8753  xpfi  8789  fiint  8795  f1opwfi  8828  mapfien  8871  marypha1lem  8897  unxpwdom  9053  cantnfval2  9132  infxpenlem  9439  djuinf  9614  isf34lem3  9797  isf34lem5  9800  axdc4lem  9877  ttukeylem6  9936  rankcf  10199  tskuni  10205  gruima  10224  dmrecnq  10390  ltexnq  10397  reclem3pr  10471  pn0sr  10523  mulgt0sr  10527  recdiv  11346  2resupmax  12582  max0sub  12590  rexmul  12665  xmulmnf1  12670  xmulm1  12675  prunioo  12868  fseq1p1m1  12982  fzshftral  12996  seqp1i  13387  seqf1olem2  13411  seqfeq4  13420  binom3  13586  expmulnbnd  13597  discr  13602  bcn2  13680  hashun2  13745  hashun3  13746  hashdif  13775  hashgt12el  13784  hashgt12el2  13785  hashfacen  13813  s2prop  14269  s4prop  14272  s3sndisj  14327  s3iunsndisj  14328  cnrecnv  14524  rddif  14700  amgm2  14729  rlimres  14915  lo1res  14916  iseraltlem2  15039  iseralt  15041  fsumss  15082  fsumcl2lem  15088  isumclim3  15114  fsumcnv  15128  telfsumo  15157  fsumiun  15176  arisum2  15216  geoisum1c  15236  fprodss  15302  fprodser  15303  fprodcl2lem  15304  fprodsplit  15320  fprodn0  15333  fprodcnv  15337  iprodclim3  15354  risefac1  15387  fallfac1  15388  bpolyval  15403  bpoly3  15412  bpoly4  15413  fsumcube  15414  sinhval  15507  cos01bnd  15539  ruclem6  15588  sadadd2lem2  15799  eucalgval  15926  pcid  16209  prmreclem4  16255  4sqlem15  16295  4sqlem16  16296  ramcl  16365  strfv2d  16529  setsid  16538  imasvscafn  16810  xpsff1o  16840  xpsaddlem  16846  xpsvsca  16850  xpsle  16852  mreexexlem2d  16916  mreexexlem4d  16918  sscres  17093  xpcid  17439  evlfcllem  17471  hofcl  17509  isacs5lem  17779  frmdup3lem  18031  cayleylem2  18541  f1omvdco2  18576  symggen  18598  psgnunilem1  18621  pgp0  18721  sylow3lem2  18753  lsmdisjr  18810  lsmdisj2r  18811  subgdisj2  18818  efgval  18843  frgpuplem  18898  frgpup2  18902  gsumval3  19027  gsumzres  19029  gsum2d2lem  19093  dprdf1  19155  dmdprdsplit2lem  19167  dmdprdsplit2  19168  ablfaclem3  19209  prdsmgp  19360  unitgrp  19417  subdrgint  19582  crng2idl  20012  psrass1lem  20157  evl1var  20499  pf1mpf  20515  pf1ind  20518  gsumfsum  20612  chrid  20674  znleval  20701  frgpcyg  20720  ocv1  20823  frlmip  20922  ellspd  20946  mamuvs2  21015  madurid  21253  baspartn  21562  mretopd  21700  ordtcld1  21805  ordtcld2  21806  leordtvallem1  21818  leordtvallem2  21819  paste  21902  imacmp  22005  cmpsub  22008  unconn  22037  1stckgen  22162  ptbasfi  22189  txcld  22211  ptclsg  22223  txdis1cn  22243  ptrescn  22247  hausdiag  22253  txkgen  22260  xkoptsub  22262  xkococnlem  22267  cnmpt21  22279  cnmpt22  22282  tgqtop  22320  qtoprest  22325  kqdisj  22340  hmeores  22379  hmphindis  22405  pt1hmeo  22414  ptuncnv  22415  ptunhmeo  22416  xpstopnlem1  22417  xkohmeo  22423  alexsublem  22652  ptcmplem2  22661  tmdcn2  22697  cldsubg  22719  qustgplem  22729  tsmsres  22752  ustbas2  22834  ressuss  22872  metreslem  22972  xpsdsval  22991  prdsxmslem2  23139  txmetcnp  23157  tngngp  23263  nrmtngdist  23266  remetdval  23397  cnheibor  23559  evth2  23564  pcoass  23628  ncvspi  23760  iscmet3  23896  rrxip  23993  minveclem2  24029  cmmbl  24135  nulmbl2  24137  volinun  24147  voliunlem1  24151  volsup  24157  ovolioo  24169  uniiccdif  24179  uniioombllem2  24184  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  ismbf3d  24255  itg2uba  24344  itg2i1fseq  24356  itgsplitioo  24438  limcflf  24479  cnplimc  24485  limcun  24493  dvfval  24495  dvres  24509  dvres3a  24512  dvnp1  24522  dvn1  24523  dvexp3  24575  dvsincos  24578  mvth  24589  c1lip2  24595  dvfsumlem2  24624  itgsubstlem  24645  itgsubst  24646  coeeq2  24832  dgreq0  24855  dgrcolem2  24864  vieta1  24901  ulm2  24973  radcnv0  25004  abelthlem2  25020  tanarg  25202  advlogexp  25238  efopn  25241  logtayl  25243  cxpcn3  25329  ang180lem3  25389  quad2  25417  mcubic  25425  binom4  25428  dquart  25431  quart1lem  25433  quart1  25434  quartlem1  25435  asinlem3a  25448  efiatan  25490  tanatan  25497  atanbndlem  25503  dvatan  25513  wilthlem2  25646  ftalem3  25652  ftalem5  25654  basellem3  25660  mumullem2  25757  musum  25768  chtublem  25787  perfectlem2  25806  bposlem6  25865  bposlem9  25868  1lgs  25916  lgs1  25917  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgsquadlem2  25957  lgsquad2lem2  25961  2sqblem  26007  rpvmasum2  26088  log2sumbnd  26120  opphllem3  26535  vtxdun  27263  clwwlknon2num  27884  eucrct2eupth  28024  ex-fpar  28241  nvpi  28444  nvop  28453  phop  28595  minvecolem2  28652  hi01  28873  pjchi  29209  chjidm  29297  mayete3i  29505  ho0val  29527  lnop0  29743  adjbdlnb  29861  pjin2i  29970  mdslmd3i  30109  mdexchi  30112  imadifxp  30351  fcoinver  30357  fnunres2  30424  suppovss  30426  mptprop  30434  padct  30455  f1od2  30457  fcobijfs  30459  ffsrn  30465  iocinif  30504  difioo  30505  s2rn  30620  s3rn  30622  cshw1s2  30634  gsummpt2co  30686  symgfcoeu  30726  symgcom  30727  pmtrprfv2  30732  pmtrcnel2  30734  tocyc01  30760  cycpmconjv  30784  cycpmconjs  30798  ofldchr  30887  krull  30980  rgmoddim  31008  lindsun  31021  dimkerim  31023  fldexttr  31048  smatlem  31062  indf1ofs  31285  esumpad2  31315  hasheuni  31344  esumcvg2  31346  esum2dlem  31351  sigapildsys  31421  measxun2  31469  measunl  31475  measinblem  31479  carsgclctunlem1  31575  carsgclctunlem3  31578  sibfof  31598  sitgclg  31600  eulerpartlemgf  31637  probdif  31678  cndprobval  31691  ballotlemic  31764  signsvtn0  31840  signstres  31845  chtvalz  31900  hgt750lemd  31919  bnj1415  32310  f1resrcmplf1d  32360  f1resfz0f1d  32361  revwlk  32371  subfacp1lem1  32426  subfacp1lem3  32429  subfacp1lem5  32431  cvmscld  32520  cvmlift2lem9a  32550  cvmlift2lem9  32558  noetalem3  33219  fwddifnp1  33626  bj-imdirid  34478  csbpredg  34610  finxpreclem5  34679  ptrest  34906  poimirlem2  34909  poimirlem3  34910  poimirlem6  34913  poimirlem7  34914  poimirlem9  34916  poimirlem11  34918  poimirlem12  34919  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem24  34931  poimirlem25  34932  poimirlem27  34934  poimirlem28  34935  poimirlem29  34936  poimirlem31  34938  voliunnfl  34951  volsupnfl  34952  mbfresfi  34953  itg2addnclem2  34959  itg2addnclem3  34960  ftc1anclem5  34986  dvacos  34994  areacirclem5  35001  cocnv  35015  istotbnd3  35064  ssbnd  35081  eccnvepres3  35557  symrelim  35810  osumcllem9N  37115  4atexlemex2  37222  cdleme20j  37469  cdlemg47  37887  diaintclN  38209  dibintclN  38318  dihintcl  38495  lclkrlem2e  38662  lclkrlem2p  38673  lcfrlem31  38724  readdid2  39253  diophin  39389  monotuz  39558  monotoddzzfi  39559  oddcomabszz  39561  fnwe2val  39669  lnmlmic  39708  fiuneneq  39817  cytpval  39829  ntrkbimka  40408  ntrneifv2  40450  radcnvrat  40666  nzprmdif  40671  binomcxplemnotnn0  40708  ioccncflimc  42188  icocncflimc  42192  stoweidlem50  42355  fourierdlem89  42500  fourierdlem90  42501  fourierdlem91  42502  fourierdlem107  42518  elsprel  43657  reuopreuprim  43708  perfectALTVlem2  43907  logb2aval  44883  aacllem  44922