Theorem eqtr3id 2812

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 2772	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	eqtrid 2810	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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  3eqtr3g  2821  csbeq1a  3865  ssdifeq0  4445  pofun  5584  opabbi2dv  5837  cnvsng  6243  csbpredg  6336  funcnvpr  6632  funcnvtp  6633  funcnvqp  6634  fresin  6781  fresaunres2  6784  f1imacnv  6871  foimacnv  6872  funfv  7003  dffv2  7011  fimacnvinrn  7103  rescnvimafod  7105  fsn2  7169  funiunfvf  7284  f1resrcmplf1d  7310  fcof1oinvd  7332  riotaxfrd  7442  f1opw2  7708  fnexALT  7997  f1od2  8145  fparlem3  8162  fparlem4  8163  fsplitfpar  8166  fnwe2lem1  8182  fvproj  8188  mpocurryd  8324  seqomlem1  8498  seqomlem4  8501  oasuc  8570  oesuclem  8571  omsuc  8572  onasuc  8574  onmsuc  8575  eqerlem  8791  pmresg  8936  fopwdom  9142  sbthlem8  9151  sbthlem9  9152  fodomr  9185  domss2  9193  mapen  9198  cnvfi  9229  fiint  9356  fodomfir  9357  f1opwfi  9383  mapfien  9437  marypha1lem  9462  unxpwdom  9620  cantnfval2  9707  ttrcltr  9754  infxpenlem  10131  djuinf  10306  isf34lem3  10492  isf34lem5  10495  axdc4lem  10572  ttukeylem6  10631  rankcf  10901  tskuni  10907  gruima  10926  dmrecnq  11092  ltexnq  11099  reclem3pr  11173  pn0sr  11225  mulgt0sr  11229  recdiv  12063  2resupmax  13358  max0sub  13366  rexmul  13441  xmulmnf1  13446  xmulm1  13451  prunioo  13652  fseq1p1m1  13772  fzshftral  13789  f1resfz0f1d  13967  seqp1d  14201  seqf1olem2  14225  seqfeq4  14234  exp4sqsq  14384  binom3  14409  expmulnbnd  14420  discr  14425  bcn2  14504  hashun2  14568  hashun3  14569  hashdif  14599  hashgt12el  14608  hashgt12el2  14609  hashfacen  14640  s2prop  15101  s4prop  15104  s3sndisj  15163  s3iunsndisj  15164  cnrecnv  15375  rddif  15552  amgm2  15581  rlimres  15769  lo1res  15770  iseraltlem2  15894  iseralt  15896  fsumss  15935  fsumcl2lem  15941  isumclim3  15969  fsumcnv  15983  telfsumo  16013  fsumiun  16032  arisum2  16074  geoisum1c  16093  fprodss  16159  fprodser  16160  fprodcl2lem  16161  fprodsplit  16177  fprodn0  16190  fprodcnv  16194  iprodclim3  16211  risefac1  16243  fallfac1  16244  bpolyval  16259  bpoly3  16268  bpoly4  16269  fsumcube  16270  sinhval  16366  cos01bnd  16398  ruclem6  16447  sadadd2lem2  16664  eucalgval  16801  pcid  17095  prmreclem4  17141  4sqlem15  17181  4sqlem16  17182  ramcl  17251  strfv2d  17423  setsid  17429  imasvscafn  17759  xpsff1o  17789  xpsaddlem  17795  xpsvsca  17799  xpsle  17801  mreexexlem2d  17869  mreexexlem4d  17871  sscres  18048  xpcid  18413  evlfcllem  18445  hofcl  18483  isacs5lem  18769  frmdup3lem  19112  cayleylem2  19678  f1omvdco2  19713  symggen  19735  psgnunilem1  19758  pgp0  19861  sylow3lem2  19893  lsmdisjr  19949  lsmdisj2r  19950  subgdisj2  19957  efgval  19982  frgpuplem  20037  frgpup2  20041  gsumval3  20172  gsumzres  20174  gsum2d2lem  20238  dprdf1  20300  dmdprdsplit2lem  20312  dmdprdsplit2  20313  ablfaclem3  20354  prdsmgp  20422  unitgrp  20664  subdrgint  21111  crng2idl  21627  gsumfsum  21794  pzriprnglem6  21847  chrid  21886  znleval  21915  frgpcyg  21934  ofldchr  21937  ocv1  22040  frlmip  22139  ellspd  22163  psrass1lem  22296  evlsvvval  22457  selvvvval  22506  ply1chr  22679  evl1var  22709  pf1mpf  22725  pf1ind  22728  mamuvs2  22776  madurid  23014  baspartn  23327  mretopd  23465  ordtcld1  23570  ordtcld2  23571  leordtvallem1  23583  leordtvallem2  23584  paste  23667  imacmp  23770  cmpsub  23773  unconn  23802  1stckgen  23928  ptbasfi  23955  txcld  23977  ptclsg  23989  txdis1cn  24009  ptrescn  24013  hausdiag  24019  txkgen  24026  xkoptsub  24028  xkococnlem  24033  cnmpt21  24045  cnmpt22  24048  tgqtop  24086  qtoprest  24091  kqdisj  24106  hmeores  24145  hmphindis  24171  pt1hmeo  24180  ptuncnv  24181  ptunhmeo  24182  xpstopnlem1  24183  xkohmeo  24189  alexsublem  24418  ptcmplem2  24427  tmdcn2  24463  cldsubg  24485  qustgplem  24495  tsmsres  24518  ustbas2  24599  ressuss  24636  metreslem  24736  xpsdsval  24755  prdsxmslem2  24903  txmetcnp  24921  tngngp  25028  nrmtngdist  25031  remetdval  25163  cnheibor  25331  evth2  25336  pcoass  25400  ncvspi  25532  iscmet3  25669  rrxip  25766  minveclem2  25802  cmmbl  25910  nulmbl2  25912  volinun  25922  voliunlem1  25926  volsup  25932  ovolioo  25944  uniiccdif  25954  uniioombllem2  25959  uniioombllem3  25961  uniioombllem4  25962  uniioombllem5  25963  ismbf3d  26030  itg2uba  26119  itg2i1fseq  26131  itgsplitioo  26213  limcflf  26256  cnplimc  26262  limcun  26270  dvfval  26272  dvres  26286  dvres3a  26289  dvnp1  26300  dvn1  26301  dvexp3  26353  dvsincos  26356  mvth  26367  c1lip2  26373  dvfsumlem2  26402  itgsubstlem  26423  itgsubst  26424  coeeq2  26616  dgreq0  26639  dgrcolem2  26648  vieta1  26690  ulm2  26769  radcnv0  26800  abelthlem2  26816  tanarg  27004  advlogexp  27040  efopn  27043  logtayl  27045  cxpcn3  27133  ang180lem3  27196  quad2  27224  mcubic  27232  binom4  27235  dquart  27238  quart1lem  27240  quart1  27241  quartlem1  27242  asinlem3a  27255  efiatan  27297  tanatan  27304  atanbndlem  27310  dvatan  27320  wilthlem2  27453  ftalem3  27459  ftalem5  27461  basellem3  27467  mumullem2  27564  musum  27575  mpodvdsmulf1o  27578  ppiub  27588  chtublem  27595  perfectlem2  27614  bposlem6  27673  bposlem9  27676  1lgs  27724  lgs1  27725  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem3  27761  lgsquadlem2  27765  lgsquad2lem2  27769  2sqblem  27815  rpvmasum2  27896  log2sumbnd  27928  noetasuplem4  28150  ltslpss  28351  leslss  28352  bdayfinbndlem1  28910  z12shalf  28923  opphllem3  29282  prlngpln3  29484  vtxdun  30119  revwlk  30324  clwwlknon2num  30753  eucrct2eupth  30903  ex-fpar  31120  nvpi  31326  nvop  31335  phop  31477  minvecolem2  31534  hi01  31755  pjchi  32091  chjidm  32179  mayete3i  32387  ho0val  32409  lnop0  32625  adjbdlnb  32743  pjin2i  32852  mdslmd3i  32991  mdexchi  32994  imadifxp  33293  fcoinver  33296  suppovss  33371  fressupp  33378  supppreima  33381  mptprop  33388  fcobijfs  33409  ffsrn  33416  iocinif  33469  difioo  33470  indf1ofs  33529  cshw1s2  33617  gsummpt2co  33708  gsumhashmul  33727  gsummulsubdishift1s  33730  gsummulsubdishift2s  33731  symgfcoeu  33742  symgcom  33743  pmtrprfv2  33748  pmtrcnel2  33750  tocyc01  33778  cycpmconjv  33802  cycpmconjs  33816  elrgspnlem2  33903  lsmsnorb2  34051  krull  34107  opprqusbas  34116  opprqusplusg  34117  qsdrngi  34123  psrgsum  34291  psrmonprod  34295  ply1degltdimlem  34365  lindsun  34368  dimkerim  34370  fldexttr  34401  constrcon  34517  cos9thpiminplylem3  34527  smatlem  34540  zarcmplem  34624  esumpad2  34799  hasheuni  34828  esumcvg2  34830  esum2dlem  34835  sigapildsys  34906  measxun2  34954  measunl  34960  measinblem  34964  carsgclctunlem1  35060  carsgclctunlem3  35063  sibfof  35083  sitgclg  35085  eulerpartlemgf  35122  probdif  35163  cndprobval  35176  ballotlemic  35250  signsvtn0  35310  signstres  35315  chtvalz  35369  hgt750lemd  35388  bnj1415  35779  subfacp1lem1  36152  subfacp1lem3  36155  subfacp1lem5  36157  cvmscld  36246  cvmlift2lem9a  36276  cvmlift2lem9  36284  fwddifnp1  37145  dfttc4  37533  coss2b  38218  nvo3  38230  finxpreclem5  38586  ptrest  38805  poimirlem2  38808  poimirlem3  38809  poimirlem6  38812  poimirlem7  38813  poimirlem9  38815  poimirlem11  38817  poimirlem12  38818  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem24  38830  poimirlem25  38831  poimirlem27  38833  poimirlem28  38834  poimirlem29  38835  poimirlem31  38837  voliunnfl  38850  volsupnfl  38851  mbfresfi  38852  itg2addnclem2  38858  itg2addnclem3  38859  ftc1anclem5  38883  dvacos  38891  areacirclem5  38898  cocnv  38927  istotbnd3  38971  ssbnd  38988  disjresdisj  39442  eccnvepres3  39490  dfblockliftmap2  39659  symrelim  39841  osumcllem9N  41287  4atexlemex2  41394  cdleme20j  41641  cdlemg47  42059  diaintclN  42381  dibintclN  42490  dihintcl  42667  lclkrlem2e  42834  lclkrlem2p  42845  lcfrlem31  42896  lcmineqlem  43368  sticksstones8  43469  dvun  43676  readdlid  43720  fsuppssind  43887  prjspnval2  43912  diophin  44049  monotuz  44214  monotoddzzfi  44215  oddcomabszz  44217  lnmlmic  44356  fiuneneq  44455  cytpval  44465  oaun3  44645  ntrkbimka  45299  ntrneifv2  45341  mnringmulrd  45482  mnringmulrcld  45487  radcnvrat  45559  nzprmdif  45564  binomcxplemnotnn0  45601  limsupvaluz  46991  ioccncflimc  47168  icocncflimc  47172  stoweidlem50  47333  fourierdlem48  47437  fourierdlem49  47438  fourierdlem89  47478  fourierdlem90  47479  fourierdlem91  47480  fourierdlem107  47496  lambert0  48210  lamberte  48211  elsprel  48830  reuopreuprim  48881  perfectALTVlem2  49093  dfnbgr6  49228  dfsclnbgr6  49229  smprngprmrng  49767  restclssep  50361  seposep  50371  iscnrm3rlem8  50392  swapfid  50732  cofuswapf1  50747  cofuswapf2  50748  fucoaltvallem  50823  idfudiag1lem  50989  termcfuncval  50998  ranval  51134  lmddu  51181  initocmd  51183  logb2aval  51288  aacllem  51367