Theorem eqtr3id 2811

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

Syntax hints:   → wi 4   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  3eqtr3g  2820  csbeq1a  3866  ssdifeq0  4440  pofun  5573  opabbi2dv  5821  cnvsng  6210  csbpredg  6294  funcnvpr  6583  funcnvtp  6584  funcnvqp  6585  f1imadifssran  6607  fresin  6733  fresaunres2  6736  f1imacnv  6823  foimacnv  6824  funfv  6954  dffv2  6962  fimacnvinrn  7052  rescnvimafod  7054  fsn2  7118  funiunfvf  7233  fcof1oinvd  7277  riotaxfrd  7387  f1opw2  7651  fnexALT  7932  fparlem3  8093  fparlem4  8094  fsplitfpar  8097  fvproj  8114  mpocurryd  8249  seqomlem1  8421  seqomlem4  8424  oasuc  8493  oesuclem  8494  omsuc  8495  onasuc  8497  onmsuc  8498  eqerlem  8714  pmresg  8852  fopwdom  9057  sbthlem8  9066  sbthlem9  9067  fodomr  9100  domss2  9108  mapen  9113  cnvfi  9144  fiint  9271  fodomfir  9272  f1opwfi  9299  mapfien  9354  marypha1lem  9379  unxpwdom  9537  cantnfval2  9624  ttrcltr  9671  infxpenlem  9969  djuinf  10145  isf34lem3  10332  isf34lem5  10335  axdc4lem  10412  ttukeylem6  10471  rankcf  10735  tskuni  10741  gruima  10760  dmrecnq  10926  ltexnq  10933  reclem3pr  11007  pn0sr  11059  mulgt0sr  11063  recdiv  11897  2resupmax  13191  max0sub  13199  rexmul  13274  xmulmnf1  13279  xmulm1  13284  prunioo  13485  fseq1p1m1  13603  fzshftral  13620  seqp1d  14031  seqf1olem2  14055  seqfeq4  14064  binom3  14237  expmulnbnd  14248  discr  14253  bcn2  14332  hashun2  14396  hashun3  14397  hashdif  14426  hashgt12el  14435  hashgt12el2  14436  hashfacen  14467  s2prop  14920  s4prop  14923  s3sndisj  14980  s3iunsndisj  14981  cnrecnv  15192  rddif  15368  amgm2  15397  rlimres  15585  lo1res  15586  iseraltlem2  15710  iseralt  15712  fsumss  15752  fsumcl2lem  15758  isumclim3  15786  fsumcnv  15800  telfsumo  15830  fsumiun  15849  arisum2  15891  geoisum1c  15910  fprodss  15978  fprodser  15979  fprodcl2lem  15980  fprodsplit  15996  fprodn0  16009  fprodcnv  16013  iprodclim3  16030  risefac1  16063  fallfac1  16064  bpolyval  16079  bpoly3  16088  bpoly4  16089  fsumcube  16090  sinhval  16186  cos01bnd  16218  ruclem6  16267  sadadd2lem2  16484  eucalgval  16616  pcid  16909  prmreclem4  16955  4sqlem15  16995  4sqlem16  16996  ramcl  17065  strfv2d  17237  setsid  17243  imasvscafn  17567  xpsff1o  17597  xpsaddlem  17603  xpsvsca  17607  xpsle  17609  mreexexlem2d  17677  mreexexlem4d  17679  sscres  17856  xpcid  18221  evlfcllem  18253  hofcl  18291  isacs5lem  18577  frmdup3lem  18900  cayleylem2  19453  f1omvdco2  19488  symggen  19510  psgnunilem1  19533  pgp0  19636  sylow3lem2  19668  lsmdisjr  19724  lsmdisj2r  19725  subgdisj2  19732  efgval  19757  frgpuplem  19812  frgpup2  19816  gsumval3  19947  gsumzres  19949  gsum2d2lem  20013  dprdf1  20075  dmdprdsplit2lem  20087  dmdprdsplit2  20088  ablfaclem3  20129  prdsmgp  20197  unitgrp  20428  subdrgint  20849  crng2idl  21348  gsumfsum  21483  pzriprnglem6  21535  chrid  21574  znleval  21603  frgpcyg  21622  ofldchr  21625  ocv1  21728  frlmip  21827  ellspd  21851  psrass1lem  21982  evlsvvval  22143  selvvvval  22192  ply1chr  22366  evl1var  22396  pf1mpf  22412  pf1ind  22415  mamuvs2  22463  madurid  22701  baspartn  23011  mretopd  23149  ordtcld1  23254  ordtcld2  23255  leordtvallem1  23267  leordtvallem2  23268  paste  23351  imacmp  23454  cmpsub  23457  unconn  23486  1stckgen  23611  ptbasfi  23638  txcld  23660  ptclsg  23672  txdis1cn  23692  ptrescn  23696  hausdiag  23702  txkgen  23709  xkoptsub  23711  xkococnlem  23716  cnmpt21  23728  cnmpt22  23731  tgqtop  23769  qtoprest  23774  kqdisj  23789  hmeores  23828  hmphindis  23854  pt1hmeo  23863  ptuncnv  23864  ptunhmeo  23865  xpstopnlem1  23866  xkohmeo  23872  alexsublem  24101  ptcmplem2  24110  tmdcn2  24146  cldsubg  24168  qustgplem  24178  tsmsres  24201  ustbas2  24282  ressuss  24319  metreslem  24419  xpsdsval  24438  prdsxmslem2  24586  txmetcnp  24604  tngngp  24711  nrmtngdist  24714  remetdval  24846  cnheibor  25014  evth2  25019  pcoass  25083  ncvspi  25215  iscmet3  25352  rrxip  25449  minveclem2  25485  cmmbl  25593  nulmbl2  25595  volinun  25605  voliunlem1  25609  volsup  25615  ovolioo  25627  uniiccdif  25637  uniioombllem2  25642  uniioombllem3  25644  uniioombllem4  25645  uniioombllem5  25646  ismbf3d  25713  itg2uba  25802  itg2i1fseq  25814  itgsplitioo  25897  limcflf  25940  cnplimc  25946  limcun  25954  dvfval  25956  dvres  25970  dvres3a  25973  dvnp1  25984  dvn1  25985  dvexp3  26037  dvsincos  26040  mvth  26051  c1lip2  26057  dvfsumlem2  26086  itgsubstlem  26107  itgsubst  26108  coeeq2  26299  dgreq0  26322  dgrcolem2  26331  vieta1  26373  ulm2  26445  radcnv0  26476  abelthlem2  26492  tanarg  26681  advlogexp  26717  efopn  26720  logtayl  26722  cxpcn3  26810  ang180lem3  26873  quad2  26901  mcubic  26909  binom4  26912  dquart  26915  quart1lem  26917  quart1  26918  quartlem1  26919  asinlem3a  26932  efiatan  26974  tanatan  26981  atanbndlem  26987  dvatan  26997  wilthlem2  27130  ftalem3  27136  ftalem5  27138  basellem3  27144  mumullem2  27241  musum  27252  mpodvdsmulf1o  27255  chtublem  27272  perfectlem2  27291  bposlem6  27350  bposlem9  27353  1lgs  27401  lgs1  27402  lgseisenlem1  27436  lgseisenlem2  27437  lgseisenlem3  27438  lgsquadlem2  27442  lgsquad2lem2  27446  2sqblem  27492  rpvmasum2  27573  log2sumbnd  27605  noetasuplem4  27797  ltslpss  27998  leslss  27999  bdayfinbndlem1  28557  z12shalf  28570  opphllem3  28919  vtxdun  29679  clwwlknon2num  30304  eucrct2eupth  30444  ex-fpar  30661  nvpi  30867  nvop  30876  phop  31018  minvecolem2  31075  hi01  31296  pjchi  31632  chjidm  31720  mayete3i  31928  ho0val  31950  lnop0  32166  adjbdlnb  32284  pjin2i  32393  mdslmd3i  32532  mdexchi  32535  imadifxp  32798  fcoinver  32801  suppovss  32880  fressupp  32887  supppreima  32890  mptprop  32897  f1od2  32918  fcobijfs  32920  ffsrn  32927  iocinif  32980  difioo  32981  indf1ofs  33041  s2rnOLD  33119  s3rnOLD  33121  cshw1s2  33135  gsummpt2co  33225  gsumhashmul  33244  gsummulsubdishift1s  33247  gsummulsubdishift2s  33248  symgfcoeu  33259  symgcom  33260  pmtrprfv2  33265  pmtrcnel2  33267  tocyc01  33295  cycpmconjv  33319  cycpmconjs  33333  elrgspnlem2  33421  lsmsnorb2  33575  krull  33664  opprqusbas  33673  opprqusplusg  33674  qsdrngi  33680  psrgsum  33842  psrmonprod  33846  ply1degltdimlem  33916  lindsun  33919  dimkerim  33921  fldexttr  33952  constrcon  34068  cos9thpiminplylem3  34078  smatlem  34091  zarcmplem  34175  esumpad2  34350  hasheuni  34379  esumcvg2  34381  esum2dlem  34386  sigapildsys  34456  measxun2  34504  measunl  34510  measinblem  34514  carsgclctunlem1  34611  carsgclctunlem3  34614  sibfof  34634  sitgclg  34636  eulerpartlemgf  34673  probdif  34714  cndprobval  34727  ballotlemic  34801  signsvtn0  34861  signstres  34866  chtvalz  34920  hgt750lemd  34939  bnj1415  35330  f1resrcmplf1d  35378  f1resfz0f1d  35461  revwlk  35472  subfacp1lem1  35526  subfacp1lem3  35529  subfacp1lem5  35531  cvmscld  35620  cvmlift2lem9a  35650  cvmlift2lem9  35658  fwddifnp1  36512  dfttc4  36887  finxpreclem5  37886  ptrest  38115  poimirlem2  38118  poimirlem3  38119  poimirlem6  38122  poimirlem7  38123  poimirlem9  38125  poimirlem11  38127  poimirlem12  38128  poimirlem16  38132  poimirlem17  38133  poimirlem19  38135  poimirlem20  38136  poimirlem24  38140  poimirlem25  38141  poimirlem27  38143  poimirlem28  38144  poimirlem29  38145  poimirlem31  38147  voliunnfl  38160  volsupnfl  38161  mbfresfi  38162  itg2addnclem2  38168  itg2addnclem3  38169  ftc1anclem5  38193  dvacos  38201  areacirclem5  38208  cocnv  38221  istotbnd3  38267  ssbnd  38284  disjresdisj  38740  eccnvepres3  38788  dfblockliftmap2  38957  symrelim  39139  osumcllem9N  40585  4atexlemex2  40692  cdleme20j  40939  cdlemg47  41357  diaintclN  41679  dibintclN  41788  dihintcl  41965  lclkrlem2e  42132  lclkrlem2p  42143  lcfrlem31  42194  lcmineqlem  42666  sticksstones8  42767  dvun  42965  readdlid  43009  fsuppssind  43172  prjspnval2  43197  flt4lem  43224  diophin  43350  monotuz  43515  monotoddzzfi  43516  oddcomabszz  43518  fnwe2val  43623  lnmlmic  43662  fiuneneq  43766  cytpval  43776  oaun3  43956  ntrkbimka  44611  ntrneifv2  44653  mnringmulrd  44796  mnringmulrcld  44801  radcnvrat  44887  nzprmdif  44892  binomcxplemnotnn0  44929  limsupvaluz  46279  ioccncflimc  46456  icocncflimc  46460  stoweidlem50  46621  fourierdlem48  46725  fourierdlem49  46726  fourierdlem89  46766  fourierdlem90  46767  fourierdlem91  46768  fourierdlem107  46784  lambert0  47478  lamberte  47479  elsprel  48078  reuopreuprim  48129  perfectALTVlem2  48341  dfnbgr6  48476  dfsclnbgr6  48477  restclssep  49534  seposep  49544  iscnrm3rlem8  49565  swapfid  49897  cofuswapf1  49912  cofuswapf2  49913  idfudiag1lem  50141  termcfuncval  50150  ranval  50238  lmddu  50285  initocmd  50287  logb2aval  50382  aacllem  50419