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  3885  ssdifeq0  4418  pofun  5477  opabbi2dv  5706  cnvsng  6066  funcnvpr  6402  funcnvtp  6403  funcnvqp  6404  fresin  6533  fresaunres2  6536  f1imacnv  6617  foimacnv  6618  funfv  6736  dffv2  6742  fimacnvinrn  6826  fsn2  6884  funiunfvf  6994  fcof1oinvd  7035  riotaxfrd  7134  f1opw2  7386  fnexALT  7638  fparlem3  7795  fparlem4  7796  fsplitfpar  7800  fvproj  7814  mpocurryd  7921  seqomlem1  8072  seqomlem4  8075  oasuc  8135  oesuclem  8136  omsuc  8137  onasuc  8139  onmsuc  8140  eqerlem  8309  pmresg  8420  fopwdom  8611  sbthlem8  8620  sbthlem9  8621  fodomr  8654  domss2  8662  mapen  8667  enp1i  8739  xpfi  8775  fiint  8781  f1opwfi  8814  mapfien  8857  marypha1lem  8883  unxpwdom  9039  cantnfval2  9118  infxpenlem  9425  djuinf  9600  isf34lem3  9783  isf34lem5  9786  axdc4lem  9863  ttukeylem6  9922  rankcf  10185  tskuni  10191  gruima  10210  dmrecnq  10376  ltexnq  10383  reclem3pr  10457  pn0sr  10509  mulgt0sr  10513  recdiv  11332  2resupmax  12568  max0sub  12576  rexmul  12651  xmulmnf1  12656  xmulm1  12661  prunioo  12856  fseq1p1m1  12971  fzshftral  12985  seqp1i  13376  seqf1olem2  13400  seqfeq4  13409  binom3  13575  expmulnbnd  13586  discr  13591  bcn2  13669  hashun2  13734  hashun3  13735  hashdif  13764  hashgt12el  13773  hashgt12el2  13774  hashfacen  13802  s2prop  14254  s4prop  14257  s3sndisj  14312  s3iunsndisj  14313  cnrecnv  14509  rddif  14685  amgm2  14714  rlimres  14900  lo1res  14901  iseraltlem2  15024  iseralt  15026  fsumss  15067  fsumcl2lem  15073  isumclim3  15099  fsumcnv  15113  telfsumo  15142  fsumiun  15161  arisum2  15201  geoisum1c  15221  fprodss  15287  fprodser  15288  fprodcl2lem  15289  fprodsplit  15305  fprodn0  15318  fprodcnv  15322  iprodclim3  15339  risefac1  15372  fallfac1  15373  bpolyval  15388  bpoly3  15397  bpoly4  15398  fsumcube  15399  sinhval  15492  cos01bnd  15524  ruclem6  15573  sadadd2lem2  15782  eucalgval  15909  pcid  16192  prmreclem4  16238  4sqlem15  16278  4sqlem16  16279  ramcl  16348  strfv2d  16512  setsid  16521  imasvscafn  16793  xpsff1o  16823  xpsaddlem  16829  xpsvsca  16833  xpsle  16835  mreexexlem2d  16899  mreexexlem4d  16901  sscres  17076  xpcid  17422  evlfcllem  17454  hofcl  17492  isacs5lem  17762  frmdup3lem  18014  cayleylem2  18524  f1omvdco2  18559  symggen  18581  psgnunilem1  18604  pgp0  18704  sylow3lem2  18736  lsmdisjr  18793  lsmdisj2r  18794  subgdisj2  18801  efgval  18826  frgpuplem  18881  frgpup2  18885  gsumval3  19010  gsumzres  19012  gsum2d2lem  19076  dprdf1  19138  dmdprdsplit2lem  19150  dmdprdsplit2  19151  ablfaclem3  19192  prdsmgp  19343  unitgrp  19400  subdrgint  19565  crng2idl  19995  psrass1lem  20140  evl1var  20482  pf1mpf  20498  pf1ind  20501  gsumfsum  20595  chrid  20657  znleval  20684  frgpcyg  20703  ocv1  20806  frlmip  20905  ellspd  20929  mamuvs2  20998  madurid  21236  baspartn  21545  mretopd  21683  ordtcld1  21788  ordtcld2  21789  leordtvallem1  21801  leordtvallem2  21802  paste  21885  imacmp  21988  cmpsub  21991  unconn  22020  1stckgen  22145  ptbasfi  22172  txcld  22194  ptclsg  22206  txdis1cn  22226  ptrescn  22230  hausdiag  22236  txkgen  22243  xkoptsub  22245  xkococnlem  22250  cnmpt21  22262  cnmpt22  22265  tgqtop  22303  qtoprest  22308  kqdisj  22323  hmeores  22362  hmphindis  22388  pt1hmeo  22397  ptuncnv  22398  ptunhmeo  22399  xpstopnlem1  22400  xkohmeo  22406  alexsublem  22635  ptcmplem2  22644  tmdcn2  22680  cldsubg  22702  qustgplem  22712  tsmsres  22735  ustbas2  22817  ressuss  22855  metreslem  22955  xpsdsval  22974  prdsxmslem2  23122  txmetcnp  23140  tngngp  23246  nrmtngdist  23249  remetdval  23380  cnheibor  23542  evth2  23547  pcoass  23611  ncvspi  23743  iscmet3  23879  rrxip  23976  minveclem2  24012  cmmbl  24118  nulmbl2  24120  volinun  24130  voliunlem1  24134  volsup  24140  ovolioo  24152  uniiccdif  24162  uniioombllem2  24167  uniioombllem3  24169  uniioombllem4  24170  uniioombllem5  24171  ismbf3d  24238  itg2uba  24327  itg2i1fseq  24339  itgsplitioo  24421  limcflf  24464  cnplimc  24470  limcun  24478  dvfval  24480  dvres  24494  dvres3a  24497  dvnp1  24507  dvn1  24508  dvexp3  24560  dvsincos  24563  mvth  24574  c1lip2  24580  dvfsumlem2  24609  itgsubstlem  24631  itgsubst  24632  coeeq2  24818  dgreq0  24841  dgrcolem2  24850  vieta1  24887  ulm2  24959  radcnv0  24990  abelthlem2  25006  tanarg  25188  advlogexp  25224  efopn  25227  logtayl  25229  cxpcn3  25315  ang180lem3  25375  quad2  25403  mcubic  25411  binom4  25414  dquart  25417  quart1lem  25419  quart1  25420  quartlem1  25421  asinlem3a  25434  efiatan  25476  tanatan  25483  atanbndlem  25489  dvatan  25499  wilthlem2  25632  ftalem3  25638  ftalem5  25640  basellem3  25646  mumullem2  25743  musum  25754  chtublem  25773  perfectlem2  25792  bposlem6  25851  bposlem9  25854  1lgs  25902  lgs1  25903  lgseisenlem1  25937  lgseisenlem2  25938  lgseisenlem3  25939  lgsquadlem2  25943  lgsquad2lem2  25947  2sqblem  25993  rpvmasum2  26074  log2sumbnd  26106  opphllem3  26521  vtxdun  27249  clwwlknon2num  27868  eucrct2eupth  28008  ex-fpar  28225  nvpi  28428  nvop  28437  phop  28579  minvecolem2  28636  hi01  28857  pjchi  29193  chjidm  29281  mayete3i  29489  ho0val  29511  lnop0  29727  adjbdlnb  29845  pjin2i  29954  mdslmd3i  30093  mdexchi  30096  imadifxp  30337  fcoinver  30343  fnunres2  30410  suppovss  30412  mptprop  30420  padct  30441  f1od2  30443  fcobijfs  30445  ffsrn  30451  iocinif  30490  difioo  30491  s2rn  30606  s3rn  30608  cshw1s2  30620  gsummpt2co  30693  symgfcoeu  30733  symgcom  30734  pmtrprfv2  30739  pmtrcnel2  30741  tocyc01  30767  cycpmconjv  30791  cycpmconjs  30805  ofldchr  30894  krull  30990  rgmoddim  31018  lindsun  31031  dimkerim  31033  fldexttr  31058  smatlem  31072  indf1ofs  31292  esumpad2  31322  hasheuni  31351  esumcvg2  31353  esum2dlem  31358  sigapildsys  31428  measxun2  31476  measunl  31482  measinblem  31486  carsgclctunlem1  31582  carsgclctunlem3  31585  sibfof  31605  sitgclg  31607  eulerpartlemgf  31644  probdif  31685  cndprobval  31698  ballotlemic  31771  signsvtn0  31847  signstres  31852  chtvalz  31907  hgt750lemd  31926  bnj1415  32317  f1resrcmplf1d  32367  f1resfz0f1d  32368  revwlk  32378  subfacp1lem1  32433  subfacp1lem3  32436  subfacp1lem5  32438  cvmscld  32527  cvmlift2lem9a  32557  cvmlift2lem9  32565  noetalem3  33226  fwddifnp1  33633  bj-imdirid  34491  csbpredg  34623  finxpreclem5  34692  ptrest  34925  poimirlem2  34928  poimirlem3  34929  poimirlem6  34932  poimirlem7  34933  poimirlem9  34935  poimirlem11  34937  poimirlem12  34938  poimirlem16  34942  poimirlem17  34943  poimirlem19  34945  poimirlem20  34946  poimirlem24  34950  poimirlem25  34951  poimirlem27  34953  poimirlem28  34954  poimirlem29  34955  poimirlem31  34957  voliunnfl  34970  volsupnfl  34971  mbfresfi  34972  itg2addnclem2  34978  itg2addnclem3  34979  ftc1anclem5  35003  dvacos  35011  areacirclem5  35018  cocnv  35032  istotbnd3  35081  ssbnd  35098  eccnvepres3  35574  symrelim  35827  osumcllem9N  37132  4atexlemex2  37239  cdleme20j  37486  cdlemg47  37904  diaintclN  38226  dibintclN  38335  dihintcl  38512  lclkrlem2e  38679  lclkrlem2p  38690  lcfrlem31  38741  readdid2  39308  diophin  39461  monotuz  39630  monotoddzzfi  39631  oddcomabszz  39633  fnwe2val  39741  lnmlmic  39780  fiuneneq  39889  cytpval  39901  ntrkbimka  40478  ntrneifv2  40520  radcnvrat  40736  nzprmdif  40741  binomcxplemnotnn0  40778  ioccncflimc  42258  icocncflimc  42262  stoweidlem50  42425  fourierdlem89  42570  fourierdlem90  42571  fourierdlem91  42572  fourierdlem107  42588  elsprel  43722  reuopreuprim  43773  perfectALTVlem2  43972  logb2aval  44948  aacllem  44987