Theorem eqtr3id 2809

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

Hypotheses

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

Assertion

Ref	Expression
eqtr3id	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr3id

Step	Hyp	Ref	Expression
1		eqtr3id.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2769	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2807	1 ⊢ (𝜑 → 𝐴 = 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  3eqtr3g  2818  csbeq1a  3861  ssdifeq0  4441  pofun  5577  opabbi2dv  5828  cnvsng  6227  csbpredg  6313  funcnvpr  6607  funcnvtp  6608  funcnvqp  6609  fresin  6756  fresaunres2  6759  f1imacnv  6846  foimacnv  6847  funfv  6977  dffv2  6985  fimacnvinrn  7076  rescnvimafod  7078  fsn2  7142  funiunfvf  7257  f1resrcmplf1d  7283  fcof1oinvd  7305  riotaxfrd  7415  f1opw2  7680  fnexALT  7967  f1od2  8115  fparlem3  8132  fparlem4  8133  fsplitfpar  8136  fnwe2lem1  8152  fvproj  8158  mpocurryd  8294  seqomlem1  8468  seqomlem4  8471  oasuc  8540  oesuclem  8541  omsuc  8542  onasuc  8544  onmsuc  8545  eqerlem  8761  pmresg  8906  fopwdom  9112  sbthlem8  9121  sbthlem9  9122  fodomr  9155  domss2  9163  mapen  9168  cnvfi  9199  fiint  9326  fodomfir  9327  f1opwfi  9353  mapfien  9407  marypha1lem  9432  unxpwdom  9590  cantnfval2  9677  ttrcltr  9724  infxpenlem  10099  djuinf  10274  isf34lem3  10460  isf34lem5  10463  axdc4lem  10540  ttukeylem6  10599  rankcf  10869  tskuni  10875  gruima  10894  dmrecnq  11060  ltexnq  11067  reclem3pr  11141  pn0sr  11193  mulgt0sr  11197  recdiv  12030  2resupmax  13325  max0sub  13333  rexmul  13408  xmulmnf1  13413  xmulm1  13418  prunioo  13619  fseq1p1m1  13739  fzshftral  13756  f1resfz0f1d  13934  seqp1d  14168  seqf1olem2  14192  seqfeq4  14201  exp4sqsq  14351  binom3  14375  expmulnbnd  14386  discr  14391  bcn2  14470  hashun2  14534  hashun3  14535  hashdif  14565  hashgt12el  14574  hashgt12el2  14575  hashfacen  14606  s2prop  15067  s4prop  15070  s3sndisj  15129  s3iunsndisj  15130  cnrecnv  15341  rddif  15517  amgm2  15546  rlimres  15734  lo1res  15735  iseraltlem2  15859  iseralt  15861  fsumss  15900  fsumcl2lem  15906  isumclim3  15934  fsumcnv  15948  telfsumo  15978  fsumiun  15997  arisum2  16039  geoisum1c  16058  fprodss  16124  fprodser  16125  fprodcl2lem  16126  fprodsplit  16142  fprodn0  16155  fprodcnv  16159  iprodclim3  16176  risefac1  16208  fallfac1  16209  bpolyval  16224  bpoly3  16233  bpoly4  16234  fsumcube  16235  sinhval  16331  cos01bnd  16363  ruclem6  16412  sadadd2lem2  16629  eucalgval  16766  pcid  17060  prmreclem4  17106  4sqlem15  17146  4sqlem16  17147  ramcl  17216  strfv2d  17388  setsid  17394  imasvscafn  17718  xpsff1o  17748  xpsaddlem  17754  xpsvsca  17758  xpsle  17760  mreexexlem2d  17828  mreexexlem4d  17830  sscres  18007  xpcid  18372  evlfcllem  18404  hofcl  18442  isacs5lem  18728  frmdup3lem  19071  cayleylem2  19636  f1omvdco2  19671  symggen  19693  psgnunilem1  19716  pgp0  19819  sylow3lem2  19851  lsmdisjr  19907  lsmdisj2r  19908  subgdisj2  19915  efgval  19940  frgpuplem  19995  frgpup2  19999  gsumval3  20130  gsumzres  20132  gsum2d2lem  20196  dprdf1  20258  dmdprdsplit2lem  20270  dmdprdsplit2  20271  ablfaclem3  20312  prdsmgp  20380  unitgrp  20622  subdrgint  21069  crng2idl  21585  gsumfsum  21749  pzriprnglem6  21801  chrid  21840  znleval  21869  frgpcyg  21888  ofldchr  21891  ocv1  21994  frlmip  22093  ellspd  22117  psrass1lem  22250  evlsvvval  22411  selvvvval  22460  ply1chr  22633  evl1var  22663  pf1mpf  22679  pf1ind  22682  mamuvs2  22730  madurid  22968  baspartn  23281  mretopd  23419  ordtcld1  23524  ordtcld2  23525  leordtvallem1  23537  leordtvallem2  23538  paste  23621  imacmp  23724  cmpsub  23727  unconn  23756  1stckgen  23882  ptbasfi  23909  txcld  23931  ptclsg  23943  txdis1cn  23963  ptrescn  23967  hausdiag  23973  txkgen  23980  xkoptsub  23982  xkococnlem  23987  cnmpt21  23999  cnmpt22  24002  tgqtop  24040  qtoprest  24045  kqdisj  24060  hmeores  24099  hmphindis  24125  pt1hmeo  24134  ptuncnv  24135  ptunhmeo  24136  xpstopnlem1  24137  xkohmeo  24143  alexsublem  24372  ptcmplem2  24381  tmdcn2  24417  cldsubg  24439  qustgplem  24449  tsmsres  24472  ustbas2  24553  ressuss  24590  metreslem  24690  xpsdsval  24709  prdsxmslem2  24857  txmetcnp  24875  tngngp  24982  nrmtngdist  24985  remetdval  25117  cnheibor  25285  evth2  25290  pcoass  25354  ncvspi  25486  iscmet3  25623  rrxip  25720  minveclem2  25756  cmmbl  25864  nulmbl2  25866  volinun  25876  voliunlem1  25880  volsup  25886  ovolioo  25898  uniiccdif  25908  uniioombllem2  25913  uniioombllem3  25915  uniioombllem4  25916  uniioombllem5  25917  ismbf3d  25984  itg2uba  26073  itg2i1fseq  26085  itgsplitioo  26167  limcflf  26210  cnplimc  26216  limcun  26224  dvfval  26226  dvres  26240  dvres3a  26243  dvnp1  26254  dvn1  26255  dvexp3  26307  dvsincos  26310  mvth  26321  c1lip2  26327  dvfsumlem2  26356  itgsubstlem  26377  itgsubst  26378  coeeq2  26570  dgreq0  26593  dgrcolem2  26602  vieta1  26644  ulm2  26721  radcnv0  26752  abelthlem2  26768  tanarg  26956  advlogexp  26992  efopn  26995  logtayl  26997  cxpcn3  27085  ang180lem3  27148  quad2  27176  mcubic  27184  binom4  27187  dquart  27190  quart1lem  27192  quart1  27193  quartlem1  27194  asinlem3a  27207  efiatan  27249  tanatan  27256  atanbndlem  27262  dvatan  27272  wilthlem2  27405  ftalem3  27411  ftalem5  27413  basellem3  27419  mumullem2  27516  musum  27527  mpodvdsmulf1o  27530  ppiub  27540  chtublem  27547  perfectlem2  27566  bposlem6  27625  bposlem9  27628  1lgs  27676  lgs1  27677  lgseisenlem1  27711  lgseisenlem2  27712  lgseisenlem3  27713  lgsquadlem2  27717  lgsquad2lem2  27721  2sqblem  27767  rpvmasum2  27848  log2sumbnd  27880  noetasuplem4  28102  ltslpss  28303  leslss  28304  bdayfinbndlem1  28862  z12shalf  28875  opphllem3  29234  prlngpln3  29436  vtxdun  30071  revwlk  30276  clwwlknon2num  30705  eucrct2eupth  30855  ex-fpar  31072  nvpi  31278  nvop  31287  phop  31429  minvecolem2  31486  hi01  31707  pjchi  32043  chjidm  32131  mayete3i  32339  ho0val  32361  lnop0  32577  adjbdlnb  32695  pjin2i  32804  mdslmd3i  32943  mdexchi  32946  imadifxp  33246  fcoinver  33249  suppovss  33325  fressupp  33332  supppreima  33335  mptprop  33342  fcobijfs  33363  ffsrn  33370  iocinif  33423  difioo  33424  indf1ofs  33483  cshw1s2  33571  gsummpt2co  33659  gsumhashmul  33678  gsummulsubdishift1s  33681  gsummulsubdishift2s  33682  symgfcoeu  33693  symgcom  33694  pmtrprfv2  33699  pmtrcnel2  33701  tocyc01  33729  cycpmconjv  33753  cycpmconjs  33767  elrgspnlem2  33854  lsmsnorb2  33997  krull  34053  opprqusbas  34062  opprqusplusg  34063  qsdrngi  34069  psrgsum  34230  psrmonprod  34234  ply1degltdimlem  34304  lindsun  34307  dimkerim  34309  fldexttr  34340  constrcon  34456  cos9thpiminplylem3  34466  smatlem  34479  zarcmplem  34563  esumpad2  34738  hasheuni  34767  esumcvg2  34769  esum2dlem  34774  sigapildsys  34845  measxun2  34893  measunl  34899  measinblem  34903  carsgclctunlem1  34999  carsgclctunlem3  35002  sibfof  35022  sitgclg  35024  eulerpartlemgf  35061  probdif  35102  cndprobval  35115  ballotlemic  35189  signsvtn0  35249  signstres  35254  chtvalz  35308  hgt750lemd  35327  bnj1415  35718  subfacp1lem1  36062  subfacp1lem3  36065  subfacp1lem5  36067  cvmscld  36156  cvmlift2lem9a  36186  cvmlift2lem9  36194  fwddifnp1  37054  dfttc4  37442  finxpreclem5  38455  ptrest  38674  poimirlem2  38677  poimirlem3  38678  poimirlem6  38681  poimirlem7  38682  poimirlem9  38684  poimirlem11  38686  poimirlem12  38687  poimirlem16  38691  poimirlem17  38692  poimirlem19  38694  poimirlem20  38695  poimirlem24  38699  poimirlem25  38700  poimirlem27  38702  poimirlem28  38703  poimirlem29  38704  poimirlem31  38706  voliunnfl  38719  volsupnfl  38720  mbfresfi  38721  itg2addnclem2  38727  itg2addnclem3  38728  ftc1anclem5  38752  dvacos  38760  areacirclem5  38767  cocnv  38796  istotbnd3  38842  ssbnd  38859  disjresdisj  39313  eccnvepres3  39361  dfblockliftmap2  39530  symrelim  39712  osumcllem9N  41158  4atexlemex2  41265  cdleme20j  41512  cdlemg47  41930  diaintclN  42252  dibintclN  42361  dihintcl  42538  lclkrlem2e  42705  lclkrlem2p  42716  lcfrlem31  42767  lcmineqlem  43239  sticksstones8  43340  dvun  43547  readdlid  43591  fsuppssind  43758  prjspnval2  43783  diophin  43920  monotuz  44085  monotoddzzfi  44086  oddcomabszz  44088  lnmlmic  44227  fiuneneq  44331  cytpval  44341  oaun3  44521  ntrkbimka  45175  ntrneifv2  45217  mnringmulrd  45358  mnringmulrcld  45363  radcnvrat  45435  nzprmdif  45440  binomcxplemnotnn0  45477  limsupvaluz  46854  ioccncflimc  47031  icocncflimc  47035  stoweidlem50  47196  fourierdlem48  47300  fourierdlem49  47301  fourierdlem89  47341  fourierdlem90  47342  fourierdlem91  47343  fourierdlem107  47359  lambert0  48073  lamberte  48074  elsprel  48693  reuopreuprim  48744  perfectALTVlem2  48956  dfnbgr6  49091  dfsclnbgr6  49092  smprngprmrng  49572  restclssep  50166  seposep  50176  iscnrm3rlem8  50197  swapfid  50537  cofuswapf1  50552  cofuswapf2  50553  fucoaltvallem  50628  idfudiag1lem  50794  termcfuncval  50803  ranval  50939  lmddu  50986  initocmd  50988  logb2aval  51071  aacllem  51150