Theorem eqtr2di 2796

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 2795	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2745	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731

This theorem is referenced by:  eqtr4id  2798  csbin  4378  csbif  4521  csbuni  4875  csbima12  5984  somincom  6036  resresdm  6133  csbfv12  6811  opabiotafun  6843  fvmptrabfv  6900  fndifnfp  7042  elxp4  7756  elxp5  7757  fo1stres  7843  fo2ndres  7844  eloprabi  7889  fo2ndf  7946  seqomlem2  8266  oev2  8329  odi  8386  fundmen  8791  xpsnen  8812  xpassen  8822  ac6sfi  9019  infeq5  9356  alephsuc3  10320  rankcf  10517  ine0  11393  nn0n0n1ge2  12283  fzval2  13224  fseq1p1m1  13312  fzosplitprm1  13478  hashfun  14133  hashf1  14152  hashtpg  14180  cshword  14485  wrd2pr2op  14637  wrd3tpop  14642  relexpsucrd  14725  relexpsucld  14726  fsum2dlem  15463  fprod2dlem  15671  ef4p  15803  sin01bnd  15875  odd2np1  16031  bitsinvp1  16137  smumullem  16180  oppcmon  17431  issubc2  17532  curf1cl  17927  curfcl  17931  cnvtsr  18287  sylow1lem1  19184  sylow2a  19205  ablsimpgfindlem1  19691  coe1fzgsumdlem  21453  evl1gsumdlem  21503  pmatcollpw3lem  21913  pptbas  22139  2ndcctbss  22587  txcmplem1  22773  qtopeu  22848  alexsubALTlem3  23181  ustuqtop5  23378  psmetdmdm  23439  xmetdmdm  23469  pcopt  24166  pcorevlem  24170  voliunlem1  24695  i1fima2  24824  iblabs  24974  dveflem  25124  deg1val  25242  abssinper  25658  mulcxplem  25820  dvatan  26066  lgamgulmlem2  26160  lgamgulmlem5  26163  lgseisenlem1  26504  dchrisumlem1  26618  pntlemr  26731  krippenlem  27032  cusgredg  27772  cusgrsizeindb0  27797  numclwlk1lem1  28712  numclwwlk3lem2lem  28726  grporndm  28851  vafval  28944  smfval  28946  hvmul0  29365  cmcmlem  29932  cmbr3i  29941  nmbdfnlbi  30390  nmcfnlbi  30393  nmopcoadji  30442  pjin2i  30534  hst1h  30568  xaddeq0  31055  gsumhashmul  31295  cycpmconjslem1  31400  archirngz  31422  esumcst  32010  eulerpartlems  32306  dstfrvunirn  32420  sgnmul  32488  subfacp1lem5  33125  cvmliftlem10  33235  fnessref  34525  fnemeet2  34535  poimirlem4  35760  poimirlem19  35775  poimirlem20  35776  poimirlem23  35779  poimirlem24  35780  poimirlem25  35781  poimirlem28  35784  ovoliunnfl  35798  voliunnfl  35800  volsupnfl  35801  itg2addnclem  35807  itg2addnc  35810  iblabsnc  35820  iblmulc2nc  35821  sdclem2  35879  blbnd  35924  ismgmOLD  35987  ismndo2  36011  rnresequniqs  36446  tendo0co2  38781  dvhfvadd  39084  dvh4dimN  39440  sn-iotauni  40173  mzpcompact2lem  40553  diophrw  40561  eldioph2  40564  pellexlem5  40635  pell1qr1  40673  rmxy0  40725  wessf1ornlem  42675  cncfuni  43381  cncfiooicclem1  43388  fourierdlem38  43640  fourierdlem60  43661  fourierdlem61  43662  fourierdlem79  43680  fourierdlem112  43713  fourierswlem  43725  fouriersw  43726  fvmptrab  44735  fvmptrabdm  44736  fmtnofac2  44973  nn0sumshdiglem1  45919