Theorem eqtr3id 2786

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  3eqtr3g  2795  csbeq1a  3865  ssdifeq0  4441  pofun  5558  opabbi2dv  5806  cnvsng  6189  csbpredg  6273  funcnvpr  6562  funcnvtp  6563  funcnvqp  6564  f1imadifssran  6586  fresin  6711  fresaunres2  6714  f1imacnv  6798  foimacnv  6799  funfv  6929  dffv2  6937  fimacnvinrn  7025  rescnvimafod  7027  fsn2  7091  funiunfvf  7205  fcof1oinvd  7249  riotaxfrd  7359  f1opw2  7623  fnexALT  7905  fparlem3  8066  fparlem4  8067  fsplitfpar  8070  fvproj  8086  mpocurryd  8221  seqomlem1  8391  seqomlem4  8394  oasuc  8461  oesuclem  8462  omsuc  8463  onasuc  8465  onmsuc  8466  eqerlem  8681  pmresg  8820  fopwdom  9025  sbthlem8  9034  sbthlem9  9035  fodomr  9068  domss2  9076  mapen  9081  cnvfi  9112  fiint  9239  fodomfir  9240  f1opwfi  9268  mapfien  9323  marypha1lem  9348  unxpwdom  9506  cantnfval2  9590  ttrcltr  9637  infxpenlem  9935  djuinf  10111  isf34lem3  10297  isf34lem5  10300  axdc4lem  10377  ttukeylem6  10436  rankcf  10700  tskuni  10706  gruima  10725  dmrecnq  10891  ltexnq  10898  reclem3pr  10972  pn0sr  11024  mulgt0sr  11028  recdiv  11859  2resupmax  13115  max0sub  13123  rexmul  13198  xmulmnf1  13203  xmulm1  13208  prunioo  13409  fseq1p1m1  13526  fzshftral  13543  seqp1d  13953  seqf1olem2  13977  seqfeq4  13986  binom3  14159  expmulnbnd  14170  discr  14175  bcn2  14254  hashun2  14318  hashun3  14319  hashdif  14348  hashgt12el  14357  hashgt12el2  14358  hashfacen  14389  s2prop  14842  s4prop  14845  s3sndisj  14902  s3iunsndisj  14903  cnrecnv  15100  rddif  15276  amgm2  15305  rlimres  15493  lo1res  15494  iseraltlem2  15618  iseralt  15620  fsumss  15660  fsumcl2lem  15666  isumclim3  15694  fsumcnv  15708  telfsumo  15737  fsumiun  15756  arisum2  15796  geoisum1c  15815  fprodss  15883  fprodser  15884  fprodcl2lem  15885  fprodsplit  15901  fprodn0  15914  fprodcnv  15918  iprodclim3  15935  risefac1  15968  fallfac1  15969  bpolyval  15984  bpoly3  15993  bpoly4  15994  fsumcube  15995  sinhval  16091  cos01bnd  16123  ruclem6  16172  sadadd2lem2  16389  eucalgval  16521  pcid  16813  prmreclem4  16859  4sqlem15  16899  4sqlem16  16900  ramcl  16969  strfv2d  17140  setsid  17146  imasvscafn  17470  xpsff1o  17500  xpsaddlem  17506  xpsvsca  17510  xpsle  17512  mreexexlem2d  17580  mreexexlem4d  17582  sscres  17759  xpcid  18124  evlfcllem  18156  hofcl  18194  isacs5lem  18480  frmdup3lem  18803  cayleylem2  19354  f1omvdco2  19389  symggen  19411  psgnunilem1  19434  pgp0  19537  sylow3lem2  19569  lsmdisjr  19625  lsmdisj2r  19626  subgdisj2  19633  efgval  19658  frgpuplem  19713  frgpup2  19717  gsumval3  19848  gsumzres  19850  gsum2d2lem  19914  dprdf1  19976  dmdprdsplit2lem  19988  dmdprdsplit2  19989  ablfaclem3  20030  prdsmgp  20098  unitgrp  20331  subdrgint  20748  crng2idl  21248  gsumfsum  21401  pzriprnglem6  21453  chrid  21492  znleval  21521  frgpcyg  21540  ofldchr  21543  ocv1  21646  frlmip  21745  ellspd  21769  psrass1lem  21900  evlsvvval  22060  ply1chr  22262  evl1var  22292  pf1mpf  22308  pf1ind  22311  mamuvs2  22362  madurid  22600  baspartn  22910  mretopd  23048  ordtcld1  23153  ordtcld2  23154  leordtvallem1  23166  leordtvallem2  23167  paste  23250  imacmp  23353  cmpsub  23356  unconn  23385  1stckgen  23510  ptbasfi  23537  txcld  23559  ptclsg  23571  txdis1cn  23591  ptrescn  23595  hausdiag  23601  txkgen  23608  xkoptsub  23610  xkococnlem  23615  cnmpt21  23627  cnmpt22  23630  tgqtop  23668  qtoprest  23673  kqdisj  23688  hmeores  23727  hmphindis  23753  pt1hmeo  23762  ptuncnv  23763  ptunhmeo  23764  xpstopnlem1  23765  xkohmeo  23771  alexsublem  24000  ptcmplem2  24009  tmdcn2  24045  cldsubg  24067  qustgplem  24077  tsmsres  24100  ustbas2  24181  ressuss  24218  metreslem  24318  xpsdsval  24337  prdsxmslem2  24485  txmetcnp  24503  tngngp  24610  nrmtngdist  24613  remetdval  24745  cnheibor  24922  evth2  24927  pcoass  24992  ncvspi  25124  iscmet3  25261  rrxip  25358  minveclem2  25394  cmmbl  25503  nulmbl2  25505  volinun  25515  voliunlem1  25519  volsup  25525  ovolioo  25537  uniiccdif  25547  uniioombllem2  25552  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  ismbf3d  25623  itg2uba  25712  itg2i1fseq  25724  itgsplitioo  25807  limcflf  25850  cnplimc  25856  limcun  25864  dvfval  25866  dvres  25880  dvres3a  25883  dvnp1  25895  dvn1  25896  dvexp3  25950  dvsincos  25953  mvth  25965  c1lip2  25971  dvfsumlem2  26001  dvfsumlem2OLD  26002  itgsubstlem  26023  itgsubst  26024  coeeq2  26215  dgreq0  26239  dgrcolem2  26248  vieta1  26288  ulm2  26362  radcnv0  26393  abelthlem2  26410  tanarg  26596  advlogexp  26632  efopn  26635  logtayl  26637  cxpcn3  26726  ang180lem3  26789  quad2  26817  mcubic  26825  binom4  26828  dquart  26831  quart1lem  26833  quart1  26834  quartlem1  26835  asinlem3a  26848  efiatan  26890  tanatan  26897  atanbndlem  26903  dvatan  26913  wilthlem2  27047  ftalem3  27053  ftalem5  27055  basellem3  27061  mumullem2  27158  musum  27169  mpodvdsmulf1o  27172  chtublem  27190  perfectlem2  27209  bposlem6  27268  bposlem9  27271  1lgs  27319  lgs1  27320  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgsquadlem2  27360  lgsquad2lem2  27364  2sqblem  27410  rpvmasum2  27491  log2sumbnd  27523  noetasuplem4  27716  ltslpss  27916  leslss  27917  bdayfinbndlem1  28475  z12shalf  28488  opphllem3  28833  vtxdun  29567  clwwlknon2num  30192  eucrct2eupth  30332  ex-fpar  30549  nvpi  30755  nvop  30764  phop  30906  minvecolem2  30963  hi01  31184  pjchi  31520  chjidm  31608  mayete3i  31816  ho0val  31838  lnop0  32054  adjbdlnb  32172  pjin2i  32281  mdslmd3i  32420  mdexchi  32423  imadifxp  32688  fcoinver  32691  suppovss  32771  fressupp  32778  supppreima  32781  mptprop  32788  padct  32808  f1od2  32809  fcobijfs  32811  ffsrn  32818  iocinif  32872  difioo  32873  indf1ofs  32959  s2rnOLD  33037  s3rnOLD  33039  cshw1s2  33053  gsummpt2co  33142  gsumhashmul  33161  gsummulsubdishift1s  33164  gsummulsubdishift2s  33165  symgfcoeu  33176  symgcom  33177  pmtrprfv2  33182  pmtrcnel2  33184  tocyc01  33212  cycpmconjv  33236  cycpmconjs  33250  elrgspnlem2  33337  lsmsnorb2  33485  krull  33572  opprqusbas  33581  opprqusplusg  33582  qsdrngi  33588  psrgsum  33725  psrmonprod  33729  rgmoddimOLD  33788  ply1degltdimlem  33800  lindsun  33803  dimkerim  33805  fldexttr  33836  constrcon  33952  cos9thpiminplylem3  33962  smatlem  33975  zarcmplem  34059  esumpad2  34234  hasheuni  34263  esumcvg2  34265  esum2dlem  34270  sigapildsys  34340  measxun2  34388  measunl  34394  measinblem  34398  carsgclctunlem1  34495  carsgclctunlem3  34498  sibfof  34518  sitgclg  34520  eulerpartlemgf  34557  probdif  34598  cndprobval  34611  ballotlemic  34685  signsvtn0  34748  signstres  34753  chtvalz  34807  hgt750lemd  34826  bnj1415  35214  f1resrcmplf1d  35264  f1resfz0f1d  35330  revwlk  35341  subfacp1lem1  35395  subfacp1lem3  35398  subfacp1lem5  35400  cvmscld  35489  cvmlift2lem9a  35519  cvmlift2lem9  35527  fwddifnp1  36381  finxpreclem5  37650  ptrest  37870  poimirlem2  37873  poimirlem3  37874  poimirlem6  37877  poimirlem7  37878  poimirlem9  37880  poimirlem11  37882  poimirlem12  37883  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem24  37895  poimirlem25  37896  poimirlem27  37898  poimirlem28  37899  poimirlem29  37900  poimirlem31  37902  voliunnfl  37915  volsupnfl  37916  mbfresfi  37917  itg2addnclem2  37923  itg2addnclem3  37924  ftc1anclem5  37948  dvacos  37956  areacirclem5  37963  cocnv  37976  istotbnd3  38022  ssbnd  38039  disjresdisj  38495  eccnvepres3  38543  dfblockliftmap2  38712  symrelim  38894  osumcllem9N  40340  4atexlemex2  40447  cdleme20j  40694  cdlemg47  41112  diaintclN  41434  dibintclN  41543  dihintcl  41720  lclkrlem2e  41887  lclkrlem2p  41898  lcfrlem31  41949  lcmineqlem  42422  sticksstones8  42523  dvun  42729  readdlid  42773  selvvvval  42943  fsuppssind  42951  prjspnval2  42976  flt4lem  43003  diophin  43129  monotuz  43298  monotoddzzfi  43299  oddcomabszz  43301  fnwe2val  43406  lnmlmic  43445  fiuneneq  43549  cytpval  43559  oaun3  43739  ntrkbimka  44394  ntrneifv2  44436  mnringmulrd  44579  mnringmulrcld  44584  radcnvrat  44670  nzprmdif  44675  binomcxplemnotnn0  44712  ioccncflimc  46243  icocncflimc  46247  stoweidlem50  46408  fourierdlem89  46553  fourierdlem90  46554  fourierdlem91  46555  fourierdlem107  46571  lambert0  47247  lamberte  47248  elsprel  47835  reuopreuprim  47886  perfectALTVlem2  48082  dfnbgr6  48217  dfsclnbgr6  48218  restclssep  49275  seposep  49285  iscnrm3rlem8  49306  swapfid  49638  cofuswapf1  49653  cofuswapf2  49654  idfudiag1lem  49882  termcfuncval  49891  ranval  49979  lmddu  50026  initocmd  50028  logb2aval  50123  aacllem  50160