Theorem eqtr2di 2790

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 2789	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2739	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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  eqtr4id  2792  csbin  4440  csbif  4586  csbuni  4941  csbima12  6079  somincom  6136  resresdm  6233  iotauni2  6513  csbfv12  6940  opabiotafun  6973  fvmptrabfv  7030  fndifnfp  7174  elxp4  7913  elxp5  7914  fo1stres  8001  fo2ndres  8002  sbcoteq1a  8037  eloprabi  8049  fo2ndf  8107  seqomlem2  8451  oev2  8523  odi  8579  fundmen  9031  xpsnen  9055  xpassen  9066  ac6sfi  9287  infeq5  9632  alephsuc3  10575  rankcf  10772  ine0  11649  nn0n0n1ge2  12539  fzval2  13487  fseq1p1m1  13575  fzosplitprm1  13742  hashfun  14397  hashf1  14418  hashtpg  14446  cshword  14741  wrd2pr2op  14894  wrd3tpop  14899  relexpsucrd  14980  relexpsucld  14981  fsum2dlem  15716  fprod2dlem  15924  ef4p  16056  sin01bnd  16128  odd2np1  16284  bitsinvp1  16390  smumullem  16433  oppcmon  17685  issubc2  17786  curf1cl  18181  curfcl  18185  cnvtsr  18541  sylow1lem1  19466  sylow2a  19487  ablsimpgfindlem1  19977  coe1fzgsumdlem  21825  evl1gsumdlem  21875  pmatcollpw3lem  22285  pptbas  22511  2ndcctbss  22959  txcmplem1  23145  qtopeu  23220  alexsubALTlem3  23553  ustuqtop5  23750  psmetdmdm  23811  xmetdmdm  23841  pcopt  24538  pcorevlem  24542  voliunlem1  25067  i1fima2  25196  iblabs  25346  dveflem  25496  deg1val  25614  abssinper  26030  mulcxplem  26192  dvatan  26440  lgamgulmlem2  26534  lgamgulmlem5  26537  lgseisenlem1  26878  dchrisumlem1  26992  pntlemr  27105  negsdi  27524  krippenlem  27941  cusgredg  28681  cusgrsizeindb0  28706  numclwlk1lem1  29622  numclwwlk3lem2lem  29636  grporndm  29763  vafval  29856  smfval  29858  hvmul0  30277  cmcmlem  30844  cmbr3i  30853  nmbdfnlbi  31302  nmcfnlbi  31305  nmopcoadji  31354  pjin2i  31446  hst1h  31480  xaddeq0  31966  gsumhashmul  32208  cycpmconjslem1  32313  archirngz  32335  opprqusmulr  32605  esumcst  33061  eulerpartlems  33359  dstfrvunirn  33473  sgnmul  33541  subfacp1lem5  34175  cvmliftlem10  34285  fnessref  35242  fnemeet2  35252  poimirlem4  36492  poimirlem19  36507  poimirlem20  36508  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem28  36516  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  itg2addnclem  36539  itg2addnc  36542  iblabsnc  36552  iblmulc2nc  36553  sdclem2  36610  blbnd  36655  ismgmOLD  36718  ismndo2  36742  rnresequniqs  37201  tendo0co2  39659  dvhfvadd  39962  dvh4dimN  40318  mzpcompact2lem  41489  diophrw  41497  eldioph2  41500  pellexlem5  41571  pell1qr1  41609  rmxy0  41662  wessf1ornlem  43882  cncfuni  44602  cncfiooicclem1  44609  fourierdlem38  44861  fourierdlem60  44882  fourierdlem61  44883  fourierdlem79  44901  fourierdlem112  44934  fourierswlem  44946  fouriersw  44947  fvmptrab  46000  fvmptrabdm  46001  fmtnofac2  46237  nn0sumshdiglem1  47307