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 2738	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 2703

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

This theorem is referenced by:  eqtr4id  2791  csbin  4439  csbif  4585  csbuni  4940  csbima12  6078  somincom  6135  resresdm  6232  iotauni2  6512  csbfv12  6939  opabiotafun  6972  fvmptrabfv  7029  fndifnfp  7176  elxp4  7915  elxp5  7916  fo1stres  8003  fo2ndres  8004  sbcoteq1a  8039  eloprabi  8051  fo2ndf  8109  seqomlem2  8453  oev2  8525  odi  8581  fundmen  9033  xpsnen  9057  xpassen  9068  ac6sfi  9289  infeq5  9634  alephsuc3  10577  rankcf  10774  ine0  11653  nn0n0n1ge2  12543  fzval2  13491  fseq1p1m1  13579  fzosplitprm1  13746  hashfun  14401  hashf1  14422  hashtpg  14450  cshword  14745  wrd2pr2op  14898  wrd3tpop  14903  relexpsucrd  14984  relexpsucld  14985  fsum2dlem  15720  fprod2dlem  15928  ef4p  16060  sin01bnd  16132  odd2np1  16288  bitsinvp1  16394  smumullem  16437  oppcmon  17689  issubc2  17790  curf1cl  18185  curfcl  18189  cnvtsr  18545  sylow1lem1  19507  sylow2a  19528  ablsimpgfindlem1  20018  coe1fzgsumdlem  22045  evl1gsumdlem  22095  pmatcollpw3lem  22505  pptbas  22731  2ndcctbss  23179  txcmplem1  23365  qtopeu  23440  alexsubALTlem3  23773  ustuqtop5  23970  psmetdmdm  24031  xmetdmdm  24061  pcopt  24762  pcorevlem  24766  voliunlem1  25291  i1fima2  25420  iblabs  25570  dveflem  25720  deg1val  25838  abssinper  26254  mulcxplem  26416  dvatan  26664  lgamgulmlem2  26758  lgamgulmlem5  26761  lgseisenlem1  27102  dchrisumlem1  27216  pntlemr  27329  negsdi  27751  krippenlem  28196  cusgredg  28936  cusgrsizeindb0  28961  numclwlk1lem1  29877  numclwwlk3lem2lem  29891  grporndm  30018  vafval  30111  smfval  30113  hvmul0  30532  cmcmlem  31099  cmbr3i  31108  nmbdfnlbi  31557  nmcfnlbi  31560  nmopcoadji  31609  pjin2i  31701  hst1h  31735  xaddeq0  32221  gsumhashmul  32466  cycpmconjslem1  32571  archirngz  32593  opprqusmulr  32867  esumcst  33347  eulerpartlems  33645  dstfrvunirn  33759  sgnmul  33827  subfacp1lem5  34461  cvmliftlem10  34571  fnessref  35545  fnemeet2  35555  poimirlem4  36795  poimirlem19  36810  poimirlem20  36811  poimirlem23  36814  poimirlem24  36815  poimirlem25  36816  poimirlem28  36819  ovoliunnfl  36833  voliunnfl  36835  volsupnfl  36836  itg2addnclem  36842  itg2addnc  36845  iblabsnc  36855  iblmulc2nc  36856  sdclem2  36913  blbnd  36958  ismgmOLD  37021  ismndo2  37045  rnresequniqs  37504  tendo0co2  39962  dvhfvadd  40265  dvh4dimN  40621  mzpcompact2lem  41791  diophrw  41799  eldioph2  41802  pellexlem5  41873  pell1qr1  41911  rmxy0  41964  wessf1ornlem  44183  cncfuni  44901  cncfiooicclem1  44908  fourierdlem38  45160  fourierdlem60  45181  fourierdlem61  45182  fourierdlem79  45200  fourierdlem112  45233  fourierswlem  45245  fouriersw  45246  fvmptrab  46299  fvmptrabdm  46300  fmtnofac2  46536  nn0sumshdiglem1  47395