Theorem eqtr2di 2788

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 2787	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2737	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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  eqtr4id  2790  csbin  4404  csbif  4548  csbuni  4902  csbima12  6036  somincom  6093  resresdm  6190  iotauni2  6470  csbfv12  6895  opabiotafun  6927  fvmptrabfv  6984  fndifnfp  7127  elxp4  7864  elxp5  7865  fo1stres  7952  fo2ndres  7953  sbcoteq1a  7988  eloprabi  8000  fo2ndf  8058  seqomlem2  8402  oev2  8474  odi  8531  fundmen  8982  xpsnen  9006  xpassen  9017  ac6sfi  9238  infeq5  9582  alephsuc3  10525  rankcf  10722  ine0  11599  nn0n0n1ge2  12489  fzval2  13437  fseq1p1m1  13525  fzosplitprm1  13692  hashfun  14347  hashf1  14368  hashtpg  14396  cshword  14691  wrd2pr2op  14844  wrd3tpop  14849  relexpsucrd  14930  relexpsucld  14931  fsum2dlem  15666  fprod2dlem  15874  ef4p  16006  sin01bnd  16078  odd2np1  16234  bitsinvp1  16340  smumullem  16383  oppcmon  17635  issubc2  17736  curf1cl  18131  curfcl  18135  cnvtsr  18491  sylow1lem1  19394  sylow2a  19415  ablsimpgfindlem1  19900  coe1fzgsumdlem  21709  evl1gsumdlem  21759  pmatcollpw3lem  22169  pptbas  22395  2ndcctbss  22843  txcmplem1  23029  qtopeu  23104  alexsubALTlem3  23437  ustuqtop5  23634  psmetdmdm  23695  xmetdmdm  23725  pcopt  24422  pcorevlem  24426  voliunlem1  24951  i1fima2  25080  iblabs  25230  dveflem  25380  deg1val  25498  abssinper  25914  mulcxplem  26076  dvatan  26322  lgamgulmlem2  26416  lgamgulmlem5  26419  lgseisenlem1  26760  dchrisumlem1  26874  pntlemr  26987  negsdi  27389  krippenlem  27695  cusgredg  28435  cusgrsizeindb0  28460  numclwlk1lem1  29376  numclwwlk3lem2lem  29390  grporndm  29515  vafval  29608  smfval  29610  hvmul0  30029  cmcmlem  30596  cmbr3i  30605  nmbdfnlbi  31054  nmcfnlbi  31057  nmopcoadji  31106  pjin2i  31198  hst1h  31232  xaddeq0  31726  gsumhashmul  31968  cycpmconjslem1  32073  archirngz  32095  esumcst  32751  eulerpartlems  33049  dstfrvunirn  33163  sgnmul  33231  subfacp1lem5  33865  cvmliftlem10  33975  fnessref  34905  fnemeet2  34915  poimirlem4  36155  poimirlem19  36170  poimirlem20  36171  poimirlem23  36174  poimirlem24  36175  poimirlem25  36176  poimirlem28  36179  ovoliunnfl  36193  voliunnfl  36195  volsupnfl  36196  itg2addnclem  36202  itg2addnc  36205  iblabsnc  36215  iblmulc2nc  36216  sdclem2  36274  blbnd  36319  ismgmOLD  36382  ismndo2  36406  rnresequniqs  36866  tendo0co2  39324  dvhfvadd  39627  dvh4dimN  39983  mzpcompact2lem  41132  diophrw  41140  eldioph2  41143  pellexlem5  41214  pell1qr1  41252  rmxy0  41305  wessf1ornlem  43525  cncfuni  44247  cncfiooicclem1  44254  fourierdlem38  44506  fourierdlem60  44527  fourierdlem61  44528  fourierdlem79  44546  fourierdlem112  44579  fourierswlem  44591  fouriersw  44592  fvmptrab  45644  fvmptrabdm  45645  fmtnofac2  45881  nn0sumshdiglem1  46827