Theorem syl5eqr 2670

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

Syntax hints:   → wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  3eqtr3g  2679  csbeq1a  3542  ssdifeq0  4051  pofun  5051  opabbi2dv  5271  funcnvpr  5950  funcnvtp  5951  funcnvqp  5952  funcnvqpOLD  5953  fresin  6073  fresaunres2  6076  f1imacnv  6153  foimacnv  6154  funfv  6265  dffv2  6271  fimacnvinrn  6348  fsn2  6403  funiunfvf  6507  fcof1oinvd  6548  riotaxfrd  6642  f1opw2  6888  fnexALT  7132  fparlem3  7279  fparlem4  7280  mpt2curryd  7395  seqomlem1  7545  seqomlem4  7548  oasuc  7604  oesuclem  7605  omsuc  7606  onasuc  7608  onmsuc  7609  eqerlem  7776  pmresg  7885  fopwdom  8068  sbthlem8  8077  sbthlem9  8078  fodomr  8111  domss2  8119  mapen  8124  enp1i  8195  xpfi  8231  fiint  8237  f1opwfi  8270  mapfien  8313  marypha1lem  8339  unxpwdom  8494  cantnfval2  8566  infxpenlem  8836  cdainf  9014  isf34lem3  9197  isf34lem5  9200  axdc4lem  9277  ttukeylem6  9336  rankcf  9599  tskuni  9605  gruima  9624  dmrecnq  9790  ltexnq  9797  reclem3pr  9871  pn0sr  9922  mulgt0sr  9926  recdiv  10731  2resupmax  12019  max0sub  12027  rexmul  12101  xmulmnf1  12106  xmulm1  12111  prunioo  12301  fseq1p1m1  12414  fzshftral  12428  seqp1i  12817  seqf1olem2  12841  seqfeq4  12850  binom3  12985  expmulnbnd  12996  discr  13001  bcn2  13106  hashun2  13172  hashun3  13173  hashdif  13201  hashgt12el  13210  hashgt12el2  13211  hashfacen  13238  wrdeqs1cat  13474  swrdccat3a  13494  s2prop  13652  s4prop  13655  s3sndisj  13706  s3iunsndisj  13707  cnrecnv  13905  rddif  14080  amgm2  14109  rlimres  14289  lo1res  14290  iseraltlem2  14413  iseralt  14415  fsumss  14456  fsumcl2lem  14462  isumclim3  14490  fsumcnv  14504  telfsumo  14534  fsumiun  14553  arisum2  14593  geoisum1c  14611  fprodss  14678  fprodser  14679  fprodcl2lem  14680  fprodsplit  14696  fprodn0  14709  fprodcnv  14713  iprodclim3  14731  risefac1  14764  fallfac1  14765  bpolyval  14780  bpoly3  14789  bpoly4  14790  fsumcube  14791  sinhval  14884  cos01bnd  14916  ruclem6  14964  sqrt2irrlemOLD  14978  sadadd2lem2  15172  eucalgval  15295  pcid  15577  prmreclem4  15623  4sqlem15  15663  4sqlem16  15664  ramcl  15733  strfv2d  15905  setsid  15914  imasvscafn  16197  xpsc0  16220  xpsc1  16221  xpsff1o  16228  xpsaddlem  16235  xpsvsca  16239  xpsle  16241  mreexexlem2d  16305  mreexexlem4d  16307  sscres  16483  xpcid  16829  evlfcllem  16861  hofcl  16899  isacs5lem  17169  frmdup3lem  17403  cayleylem2  17833  f1omvdco2  17868  symggen  17890  psgnunilem1  17913  pgp0  18011  sylow3lem2  18043  lsmdisjr  18097  lsmdisj2r  18098  subgdisj2  18105  efgval  18130  frgpuplem  18185  frgpup2  18189  gsumval3  18308  gsumzres  18310  gsum2d2lem  18372  dprdf1  18432  dmdprdsplit2lem  18444  dmdprdsplit2  18445  ablfaclem3  18486  prdsmgp  18610  unitgrp  18667  crng2idl  19239  psrass1lem  19377  evl1var  19700  pf1mpf  19716  pf1ind  19719  gsumfsum  19813  chrid  19875  znleval  19903  ocv1  20023  frlmip  20117  ellspd  20141  mamuvs2  20212  madurid  20450  baspartn  20758  mretopd  20896  ordtcld1  21001  ordtcld2  21002  leordtvallem1  21014  leordtvallem2  21015  paste  21098  imacmp  21200  cmpsub  21203  unconn  21232  1stckgen  21357  ptbasfi  21384  txcld  21406  ptclsg  21418  txdis1cn  21438  ptrescn  21442  hausdiag  21448  txkgen  21455  xkoptsub  21457  xkococnlem  21462  cnmpt21  21474  cnmpt22  21477  tgqtop  21515  qtoprest  21520  kqdisj  21535  hmeores  21574  hmphindis  21600  pt1hmeo  21609  ptuncnv  21610  ptunhmeo  21611  xpstopnlem1  21612  xkohmeo  21618  alexsublem  21848  ptcmplem2  21857  tmdcn2  21893  cldsubg  21914  qustgplem  21924  tsmsres  21947  ustbas2  22029  ressuss  22067  metreslem  22167  xpsdsval  22186  prdsxmslem2  22334  txmetcnp  22352  tngngp  22458  nrmtngdist  22461  remetdval  22592  cnheibor  22754  evth2  22759  pcoass  22824  ncvspi  22956  iscmet3  23091  rrxip  23178  minveclem2  23197  cmmbl  23302  nulmbl2  23304  volinun  23314  voliunlem1  23318  volsup  23324  ovolioo  23336  uniiccdif  23346  uniioombllem2  23351  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  ismbf3d  23421  itg2uba  23510  itg2i1fseq  23522  itgsplitioo  23604  limcflf  23645  cnplimc  23651  limcun  23659  dvfval  23661  dvres  23675  dvres3a  23678  dvnp1  23688  dvn1  23689  dvexp3  23741  dvsincos  23744  mvth  23755  c1lip2  23761  dvfsumlem2  23790  itgsubstlem  23811  itgsubst  23812  coeeq2  23998  dgreq0  24021  dgrcolem2  24030  vieta1  24067  ulm2  24139  radcnv0  24170  abelthlem2  24186  tanarg  24365  advlogexp  24401  efopn  24404  logtayl  24406  cxpcn3  24489  ang180lem3  24541  quad2  24566  mcubic  24574  binom4  24577  dquart  24580  quart1lem  24582  quart1  24583  quartlem1  24584  asinlem3a  24597  efiatan  24639  tanatan  24646  atanbndlem  24652  dvatan  24662  ftalem3  24801  ftalem5  24803  basellem3  24809  mumullem2  24906  musum  24917  chtublem  24936  perfectlem2  24955  bposlem6  25014  bposlem9  25017  1lgs  25065  lgs1  25066  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgsquadlem2  25106  lgsquad2lem2  25110  2sqblem  25156  rpvmasum2  25201  log2sumbnd  25233  opphllem3  25641  vtxdun  26377  wspn0  26820  eucrct2eupth  27105  numclwwlkovf2num  27218  nvpi  27522  nvop  27531  phop  27673  minvecolem2  27731  hi01  27953  pjchi  28291  chjidm  28379  mayete3i  28587  ho0val  28609  lnop0  28825  adjbdlnb  28943  pjin2i  29052  mdslmd3i  29191  mdexchi  29194  imadifxp  29414  fcoinver  29418  padct  29497  fcobijfs  29501  ffsrn  29504  iocinif  29543  difioo  29544  gsummpt2co  29780  ofldchr  29814  symgfcoeu  29845  pmtrprfv2  29848  smatlem  29863  fvproj  29899  indf1ofs  30088  esumpad2  30118  hasheuni  30147  esumcvg2  30149  esum2dlem  30154  sigapildsys  30225  measxun2  30273  measunl  30279  measinblem  30283  carsgclctunlem1  30379  carsgclctunlem3  30382  sibfof  30402  sitgclg  30404  eulerpartlemgf  30441  probdif  30482  cndprobval  30495  ballotlemic  30568  signsvtn0  30647  signstres  30652  chtvalz  30707  hgt750lemd  30726  bnj1415  31106  subfacp1lem1  31161  subfacp1lem3  31164  subfacp1lem5  31166  cvmscld  31255  cvmlift2lem9a  31285  cvmlift2lem9  31293  noetalem3  31865  fwddifnp1  32272  csbpredg  33172  finxpreclem5  33232  ptrest  33408  poimirlem2  33411  poimirlem3  33412  poimirlem6  33415  poimirlem7  33416  poimirlem9  33418  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem24  33433  poimirlem25  33434  poimirlem27  33436  poimirlem28  33437  poimirlem29  33438  poimirlem31  33440  voliunnfl  33453  volsupnfl  33454  mbfresfi  33456  itg2addnclem2  33462  itg2addnclem3  33463  ftc1anclem5  33489  dvacos  33497  areacirclem5  33504  cocnv  33520  istotbnd3  33570  ssbnd  33587  eccnvepres3  34050  fsumshftdOLD  34238  osumcllem9N  35250  4atexlemex2  35357  cdleme20j  35606  cdlemg47  36024  diaintclN  36347  dibintclN  36456  dihintcl  36633  lclkrlem2e  36800  lclkrlem2p  36811  lcfrlem31  36862  diophin  37336  monotuz  37506  monotoddzzfi  37507  oddcomabszz  37509  fnwe2val  37619  lnmlmic  37658  fiuneneq  37775  cytpval  37787  ntrkbimka  38336  ntrneifv2  38378  radcnvrat  38513  nzprmdif  38518  binomcxplemnotnn0  38555  ioccncflimc  40098  icocncflimc  40102  stoweidlem50  40267  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem107  40430  perfectALTVlem2  41631  elsprel  41725  logb2aval  42505  aacllem  42547