Theorem eqtr3id 2810

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 2770	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2808	1 ⊢ (𝜑 → 𝐴 = 𝐶)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  3eqtr3g  2819  csbeq1a  3861  ssdifeq0  4442  pofun  5577  opabbi2dv  5827  cnvsng  6224  csbpredg  6310  funcnvpr  6602  funcnvtp  6603  funcnvqp  6604  fresin  6751  fresaunres2  6754  f1imacnv  6841  foimacnv  6842  funfv  6972  dffv2  6980  fimacnvinrn  7071  rescnvimafod  7073  fsn2  7137  funiunfvf  7253  f1resrcmplf1d  7279  fcof1oinvd  7301  riotaxfrd  7411  f1opw2  7676  fnexALT  7963  fparlem3  8125  fparlem4  8126  fsplitfpar  8129  fnwe2lem1  8145  fvproj  8151  mpocurryd  8286  seqomlem1  8460  seqomlem4  8463  oasuc  8532  oesuclem  8533  omsuc  8534  onasuc  8536  onmsuc  8537  eqerlem  8753  pmresg  8898  fopwdom  9104  sbthlem8  9113  sbthlem9  9114  fodomr  9147  domss2  9155  mapen  9160  cnvfi  9191  fiint  9318  fodomfir  9319  f1opwfi  9345  mapfien  9400  marypha1lem  9425  unxpwdom  9583  cantnfval2  9670  ttrcltr  9717  infxpenlem  10092  djuinf  10267  isf34lem3  10453  isf34lem5  10456  axdc4lem  10533  ttukeylem6  10592  rankcf  10862  tskuni  10868  gruima  10887  dmrecnq  11053  ltexnq  11060  reclem3pr  11134  pn0sr  11186  mulgt0sr  11190  recdiv  12023  2resupmax  13318  max0sub  13326  rexmul  13401  xmulmnf1  13406  xmulm1  13411  prunioo  13612  fseq1p1m1  13732  fzshftral  13749  f1resfz0f1d  13927  seqp1d  14161  seqf1olem2  14185  seqfeq4  14194  exp4sqsq  14344  binom3  14368  expmulnbnd  14379  discr  14384  bcn2  14463  hashun2  14527  hashun3  14528  hashdif  14558  hashgt12el  14567  hashgt12el2  14568  hashfacen  14599  s2prop  15058  s4prop  15061  s3sndisj  15120  s3iunsndisj  15121  cnrecnv  15332  rddif  15508  amgm2  15537  rlimres  15725  lo1res  15726  iseraltlem2  15850  iseralt  15852  fsumss  15891  fsumcl2lem  15897  isumclim3  15925  fsumcnv  15939  telfsumo  15969  fsumiun  15988  arisum2  16030  geoisum1c  16049  fprodss  16115  fprodser  16116  fprodcl2lem  16117  fprodsplit  16133  fprodn0  16146  fprodcnv  16150  iprodclim3  16167  risefac1  16199  fallfac1  16200  bpolyval  16215  bpoly3  16224  bpoly4  16225  fsumcube  16226  sinhval  16322  cos01bnd  16354  ruclem6  16403  sadadd2lem2  16620  eucalgval  16757  pcid  17051  prmreclem4  17097  4sqlem15  17137  4sqlem16  17138  ramcl  17207  strfv2d  17379  setsid  17385  imasvscafn  17709  xpsff1o  17739  xpsaddlem  17745  xpsvsca  17749  xpsle  17751  mreexexlem2d  17819  mreexexlem4d  17821  sscres  17998  xpcid  18363  evlfcllem  18395  hofcl  18433  isacs5lem  18719  frmdup3lem  19062  cayleylem2  19627  f1omvdco2  19662  symggen  19684  psgnunilem1  19707  pgp0  19810  sylow3lem2  19842  lsmdisjr  19898  lsmdisj2r  19899  subgdisj2  19906  efgval  19931  frgpuplem  19986  frgpup2  19990  gsumval3  20121  gsumzres  20123  gsum2d2lem  20187  dprdf1  20249  dmdprdsplit2lem  20261  dmdprdsplit2  20262  ablfaclem3  20303  prdsmgp  20371  unitgrp  20613  subdrgint  21060  crng2idl  21576  gsumfsum  21740  pzriprnglem6  21792  chrid  21831  znleval  21860  frgpcyg  21879  ofldchr  21882  ocv1  21985  frlmip  22084  ellspd  22108  psrass1lem  22241  evlsvvval  22402  selvvvval  22451  ply1chr  22624  evl1var  22654  pf1mpf  22670  pf1ind  22673  mamuvs2  22721  madurid  22959  baspartn  23272  mretopd  23410  ordtcld1  23515  ordtcld2  23516  leordtvallem1  23528  leordtvallem2  23529  paste  23612  imacmp  23715  cmpsub  23718  unconn  23747  1stckgen  23873  ptbasfi  23900  txcld  23922  ptclsg  23934  txdis1cn  23954  ptrescn  23958  hausdiag  23964  txkgen  23971  xkoptsub  23973  xkococnlem  23978  cnmpt21  23990  cnmpt22  23993  tgqtop  24031  qtoprest  24036  kqdisj  24051  hmeores  24090  hmphindis  24116  pt1hmeo  24125  ptuncnv  24126  ptunhmeo  24127  xpstopnlem1  24128  xkohmeo  24134  alexsublem  24363  ptcmplem2  24372  tmdcn2  24408  cldsubg  24430  qustgplem  24440  tsmsres  24463  ustbas2  24544  ressuss  24581  metreslem  24681  xpsdsval  24700  prdsxmslem2  24848  txmetcnp  24866  tngngp  24973  nrmtngdist  24976  remetdval  25108  cnheibor  25276  evth2  25281  pcoass  25345  ncvspi  25477  iscmet3  25614  rrxip  25711  minveclem2  25747  cmmbl  25855  nulmbl2  25857  volinun  25867  voliunlem1  25871  volsup  25877  ovolioo  25889  uniiccdif  25899  uniioombllem2  25904  uniioombllem3  25906  uniioombllem4  25907  uniioombllem5  25908  ismbf3d  25975  itg2uba  26064  itg2i1fseq  26076  itgsplitioo  26158  limcflf  26201  cnplimc  26207  limcun  26215  dvfval  26217  dvres  26231  dvres3a  26234  dvnp1  26245  dvn1  26246  dvexp3  26298  dvsincos  26301  mvth  26312  c1lip2  26318  dvfsumlem2  26347  itgsubstlem  26368  itgsubst  26369  coeeq2  26561  dgreq0  26584  dgrcolem2  26593  vieta1  26635  ulm2  26712  radcnv0  26743  abelthlem2  26759  tanarg  26947  advlogexp  26983  efopn  26986  logtayl  26988  cxpcn3  27076  ang180lem3  27139  quad2  27167  mcubic  27175  binom4  27178  dquart  27181  quart1lem  27183  quart1  27184  quartlem1  27185  asinlem3a  27198  efiatan  27240  tanatan  27247  atanbndlem  27253  dvatan  27263  wilthlem2  27396  ftalem3  27402  ftalem5  27404  basellem3  27410  mumullem2  27507  musum  27518  mpodvdsmulf1o  27521  ppiub  27531  chtublem  27538  perfectlem2  27557  bposlem6  27616  bposlem9  27619  1lgs  27667  lgs1  27668  lgseisenlem1  27702  lgseisenlem2  27703  lgseisenlem3  27704  lgsquadlem2  27708  lgsquad2lem2  27712  2sqblem  27758  rpvmasum2  27839  log2sumbnd  27871  noetasuplem4  28093  ltslpss  28294  leslss  28295  bdayfinbndlem1  28853  z12shalf  28866  opphllem3  29225  prlngpln3  29427  vtxdun  30062  revwlk  30267  clwwlknon2num  30696  eucrct2eupth  30846  ex-fpar  31063  nvpi  31269  nvop  31278  phop  31420  minvecolem2  31477  hi01  31698  pjchi  32034  chjidm  32122  mayete3i  32330  ho0val  32352  lnop0  32568  adjbdlnb  32686  pjin2i  32795  mdslmd3i  32934  mdexchi  32937  imadifxp  33195  fcoinver  33198  suppovss  33274  fressupp  33281  supppreima  33284  mptprop  33291  f1od2  33311  fcobijfs  33313  ffsrn  33320  iocinif  33373  difioo  33374  indf1ofs  33433  cshw1s2  33521  gsummpt2co  33609  gsumhashmul  33628  gsummulsubdishift1s  33631  gsummulsubdishift2s  33632  symgfcoeu  33643  symgcom  33644  pmtrprfv2  33649  pmtrcnel2  33651  tocyc01  33679  cycpmconjv  33703  cycpmconjs  33717  elrgspnlem2  33804  lsmsnorb2  33947  krull  34003  opprqusbas  34012  opprqusplusg  34013  qsdrngi  34019  psrgsum  34180  psrmonprod  34184  ply1degltdimlem  34254  lindsun  34257  dimkerim  34259  fldexttr  34290  constrcon  34406  cos9thpiminplylem3  34416  smatlem  34429  zarcmplem  34513  esumpad2  34688  hasheuni  34717  esumcvg2  34719  esum2dlem  34724  sigapildsys  34795  measxun2  34843  measunl  34849  measinblem  34853  carsgclctunlem1  34949  carsgclctunlem3  34952  sibfof  34972  sitgclg  34974  eulerpartlemgf  35011  probdif  35052  cndprobval  35065  ballotlemic  35139  signsvtn0  35199  signstres  35204  chtvalz  35258  hgt750lemd  35277  bnj1415  35668  subfacp1lem1  35944  subfacp1lem3  35947  subfacp1lem5  35949  cvmscld  36038  cvmlift2lem9a  36068  cvmlift2lem9  36076  fwddifnp1  36930  dfttc4  37318  finxpreclem5  38318  ptrest  38537  poimirlem2  38540  poimirlem3  38541  poimirlem6  38544  poimirlem7  38545  poimirlem9  38547  poimirlem11  38549  poimirlem12  38550  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem24  38562  poimirlem25  38563  poimirlem27  38565  poimirlem28  38566  poimirlem29  38567  poimirlem31  38569  voliunnfl  38582  volsupnfl  38583  mbfresfi  38584  itg2addnclem2  38590  itg2addnclem3  38591  ftc1anclem5  38615  dvacos  38623  areacirclem5  38630  cocnv  38659  istotbnd3  38705  ssbnd  38722  disjresdisj  39176  eccnvepres3  39224  dfblockliftmap2  39393  symrelim  39575  osumcllem9N  41021  4atexlemex2  41128  cdleme20j  41375  cdlemg47  41793  diaintclN  42115  dibintclN  42224  dihintcl  42401  lclkrlem2e  42568  lclkrlem2p  42579  lcfrlem31  42630  lcmineqlem  43102  sticksstones8  43203  dvun  43410  readdlid  43454  fsuppssind  43621  prjspnval2  43646  diophin  43782  monotuz  43947  monotoddzzfi  43948  oddcomabszz  43950  lnmlmic  44089  fiuneneq  44193  cytpval  44203  oaun3  44383  ntrkbimka  45037  ntrneifv2  45079  mnringmulrd  45220  mnringmulrcld  45225  radcnvrat  45297  nzprmdif  45302  binomcxplemnotnn0  45339  limsupvaluz  46717  ioccncflimc  46894  icocncflimc  46898  stoweidlem50  47059  fourierdlem48  47163  fourierdlem49  47164  fourierdlem89  47204  fourierdlem90  47205  fourierdlem91  47206  fourierdlem107  47222  lambert0  47936  lamberte  47937  elsprel  48556  reuopreuprim  48607  perfectALTVlem2  48819  dfnbgr6  48954  dfsclnbgr6  48955  smprngprmrng  49435  restclssep  50023  seposep  50033  iscnrm3rlem8  50054  swapfid  50386  cofuswapf1  50401  cofuswapf2  50402  idfudiag1lem  50630  termcfuncval  50639  ranval  50727  lmddu  50774  initocmd  50776  logb2aval  50859  aacllem  50938