Theorem eqtr2di 2813

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

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

Assertion

Ref	Expression
eqtr2di	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem eqtr2di

Step	Hyp	Ref	Expression
1		eqtr2di.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr2di.2	. . 3 ⊢ 𝐵 = 𝐶
3	1, 2	eqtrdi 2812	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2767	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  eqtr4id  2815  csbin  4393  csbif  4535  elpr2elpr  4824  csbuni  4893  csbima12  6064  somincom  6117  resresdm  6215  iotauni2  6488  csbfv12  6907  opabiotafun  6942  fvmptrabfv  7003  fndifnfp  7155  elxp4  7898  elxp5  7899  fo1stres  7991  fo2ndres  7992  sbcoteq1a  8027  eloprabi  8039  fo2ndf  8094  seqomlem2  8416  oev2  8486  odi  8542  fundmen  9006  xpsnen  9027  xpassen  9037  ac6sfi  9222  infeq5  9586  alephsuc3  10532  rankcf  10729  ine0  11616  nn0n0n1ge2  12543  fzval2  13509  fseq1p1m1  13597  fzosplitprm1  13778  hashfun  14444  hashf1  14464  hashtpg  14492  cshword  14798  wrd2pr2op  14950  wrd3tpop  14955  relexpsucrd  15040  relexpsucld  15041  sgnmul  15111  fsum2dlem  15788  fprod2dlem  16001  ef4p  16136  sin01bnd  16208  odd2np1  16366  bitsinvp1  16474  smumullem  16517  oppcmon  17762  issubc2  17860  curf1cl  18251  curfcl  18255  cnvtsr  18611  ex-chn1  18660  sylow1lem1  19629  sylow2a  19650  ablsimpgfindlem1  20140  coe1fzgsumdlem  22354  evl1gsumdlem  22407  pmatcollpw3lem  22831  pptbas  23056  2ndcctbss  23503  txcmplem1  23689  qtopeu  23764  alexsubALTlem3  24097  ustuqtop5  24293  psmetdmdm  24353  xmetdmdm  24383  pcopt  25072  pcorevlem  25076  voliunlem1  25600  i1fima2  25729  iblabs  25879  dveflem  26029  deg1val  26144  abssinper  26574  mulcxplem  26737  dvatan  26988  lgamgulmlem2  27082  lgamgulmlem5  27085  lgseisenlem1  27427  dchrisumlem1  27541  pntlemr  27654  negsdi  28131  noseqrdg0  28388  eucliddivs  28457  pw2cut2  28543  krippenlem  28847  cusgredg  29582  cusgrsizeindb0  29607  numclwlk1lem1  30528  numclwwlk3lem2lem  30542  grporndm  30670  vafval  30763  smfval  30765  hvmul0  31184  cmcmlem  31751  cmbr3i  31760  nmbdfnlbi  32209  nmcfnlbi  32212  nmopcoadji  32261  pjin2i  32353  hst1h  32387  xaddeq0  32916  gsumhashmul  33208  cycpmconjslem1  33295  archirngz  33330  opprqusmulr  33640  dflringlem3  33653  dflring4  33655  selvply1rhm0  33784  esplyfvaln  33832  esplyind  33833  extdgfialglem2  33951  constrinvcl  34031  cos9thpiminplylem1  34040  esumcst  34321  eulerpartlems  34618  dstfrvunirn  34733  subfacp1lem5  35495  cvmliftlem10  35605  fnessref  36678  fnemeet2  36688  poimirlem4  38084  poimirlem19  38099  poimirlem20  38100  poimirlem23  38103  poimirlem24  38104  poimirlem25  38105  poimirlem28  38108  ovoliunnfl  38122  voliunnfl  38124  volsupnfl  38125  itg2addnclem  38131  itg2addnc  38134  iblabsnc  38144  iblmulc2nc  38145  sdclem2  38202  blbnd  38247  ismgmOLD  38310  ismndo2  38334  rnresequniqs  38794  tendo0co2  41373  dvhfvadd  41676  dvh4dimN  42032  mzpcompact2lem  43293  diophrw  43301  eldioph2  43304  pellexlem5  43371  pell1qr1  43409  rmxy0  43461  wessf1ornlem  45724  cncfuni  46421  cncfiooicclem1  46428  dvnprodlem1  46481  fourierdlem38  46680  fourierdlem60  46701  fourierdlem61  46702  fourierdlem79  46720  fourierdlem112  46753  fourierswlem  46765  fouriersw  46766  chnerlem1  47419  fvmptrab  47847  fvmptrabdm  47848  fmtnofac2  48139  nn0sumshdiglem1  49204  eloprab1st2nd  49450  dmdm  49635  isinito2lem  50080  termolmd  50252