Theorem eqtr2di 2789

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 2788	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2743	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:  eqtr4id  2791  csbin  4383  csbif  4525  elpr2elpr  4813  csbuni  4881  csbima12  6038  somincom  6091  resresdm  6191  iotauni2  6464  csbfv12  6879  opabiotafun  6914  fvmptrabfv  6974  fndifnfp  7124  elxp4  7866  elxp5  7867  fo1stres  7961  fo2ndres  7962  sbcoteq1a  7997  eloprabi  8009  fo2ndf  8064  seqomlem2  8383  oev2  8451  odi  8507  fundmen  8971  xpsnen  8992  xpassen  9002  ac6sfi  9187  infeq5  9549  alephsuc3  10494  rankcf  10691  ine0  11576  nn0n0n1ge2  12496  fzval2  13455  fseq1p1m1  13543  fzosplitprm1  13724  hashfun  14390  hashf1  14410  hashtpg  14438  cshword  14744  wrd2pr2op  14896  wrd3tpop  14901  relexpsucrd  14986  relexpsucld  14987  fsum2dlem  15723  fprod2dlem  15936  ef4p  16071  sin01bnd  16143  odd2np1  16301  bitsinvp1  16409  smumullem  16452  oppcmon  17696  issubc2  17794  curf1cl  18185  curfcl  18189  cnvtsr  18545  ex-chn1  18594  sylow1lem1  19564  sylow2a  19585  ablsimpgfindlem1  20075  coe1fzgsumdlem  22278  evl1gsumdlem  22331  pmatcollpw3lem  22758  pptbas  22983  2ndcctbss  23430  txcmplem1  23616  qtopeu  23691  alexsubALTlem3  24024  ustuqtop5  24220  psmetdmdm  24280  xmetdmdm  24310  pcopt  24999  pcorevlem  25003  voliunlem1  25527  i1fima2  25656  iblabs  25806  dveflem  25956  deg1val  26071  abssinper  26498  mulcxplem  26661  dvatan  26912  lgamgulmlem2  27007  lgamgulmlem5  27010  lgseisenlem1  27352  dchrisumlem1  27466  pntlemr  27579  negsdi  28056  noseqrdg0  28313  eucliddivs  28382  pw2cut2  28468  krippenlem  28772  cusgredg  29507  cusgrsizeindb0  29533  numclwlk1lem1  30454  numclwwlk3lem2lem  30468  grporndm  30596  vafval  30689  smfval  30691  hvmul0  31110  cmcmlem  31677  cmbr3i  31686  nmbdfnlbi  32135  nmcfnlbi  32138  nmopcoadji  32187  pjin2i  32279  hst1h  32313  xaddeq0  32841  sgnmul  32923  gsumhashmul  33143  cycpmconjslem1  33230  archirngz  33265  opprqusmulr  33566  esplyfvaln  33733  esplyind  33734  extdgfialglem2  33853  constrinvcl  33933  cos9thpiminplylem1  33942  esumcst  34223  eulerpartlems  34520  dstfrvunirn  34635  subfacp1lem5  35382  cvmliftlem10  35492  fnessref  36555  fnemeet2  36565  poimirlem4  37959  poimirlem19  37974  poimirlem20  37975  poimirlem23  37978  poimirlem24  37979  poimirlem25  37980  poimirlem28  37983  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  itg2addnclem  38006  itg2addnc  38009  iblabsnc  38019  iblmulc2nc  38020  sdclem2  38077  blbnd  38122  ismgmOLD  38185  ismndo2  38209  rnresequniqs  38669  tendo0co2  41248  dvhfvadd  41551  dvh4dimN  41907  mzpcompact2lem  43197  diophrw  43205  eldioph2  43208  pellexlem5  43279  pell1qr1  43317  rmxy0  43369  wessf1ornlem  45633  cncfuni  46332  cncfiooicclem1  46339  dvnprodlem1  46392  fourierdlem38  46591  fourierdlem60  46612  fourierdlem61  46613  fourierdlem79  46631  fourierdlem112  46664  fourierswlem  46676  fouriersw  46677  chnerlem1  47328  fvmptrab  47752  fvmptrabdm  47753  fmtnofac2  48044  nn0sumshdiglem1  49109  eloprab1st2nd  49355  dmdm  49540  isinito2lem  49985  termolmd  50157