Theorem eqtr2di 2787

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  eqtr4id  2789  csbin  4417  csbif  4558  elpr2elpr  4845  csbuni  4912  csbima12  6066  somincom  6123  resresdm  6222  iotauni2  6500  csbfv12  6924  opabiotafun  6959  fvmptrabfv  7018  fndifnfp  7168  elxp4  7918  elxp5  7919  fo1stres  8014  fo2ndres  8015  sbcoteq1a  8050  eloprabi  8062  fo2ndf  8120  seqomlem2  8465  oev2  8535  odi  8591  fundmen  9045  xpsnen  9069  xpassen  9080  ac6sfi  9292  infeq5  9651  alephsuc3  10594  rankcf  10791  ine0  11672  nn0n0n1ge2  12569  fzval2  13527  fseq1p1m1  13615  fzosplitprm1  13793  hashfun  14455  hashf1  14475  hashtpg  14503  cshword  14809  wrd2pr2op  14962  wrd3tpop  14967  relexpsucrd  15052  relexpsucld  15053  fsum2dlem  15786  fprod2dlem  15996  ef4p  16131  sin01bnd  16203  odd2np1  16360  bitsinvp1  16468  smumullem  16511  oppcmon  17751  issubc2  17849  curf1cl  18240  curfcl  18244  cnvtsr  18598  sylow1lem1  19579  sylow2a  19600  ablsimpgfindlem1  20090  coe1fzgsumdlem  22241  evl1gsumdlem  22294  pmatcollpw3lem  22721  pptbas  22946  2ndcctbss  23393  txcmplem1  23579  qtopeu  23654  alexsubALTlem3  23987  ustuqtop5  24184  psmetdmdm  24244  xmetdmdm  24274  pcopt  24973  pcorevlem  24977  voliunlem1  25503  i1fima2  25632  iblabs  25782  dveflem  25935  deg1val  26053  abssinper  26482  mulcxplem  26645  dvatan  26897  lgamgulmlem2  26992  lgamgulmlem5  26995  lgseisenlem1  27338  dchrisumlem1  27452  pntlemr  27565  negsdi  28008  noseqrdg0  28253  eucliddivs  28317  krippenlem  28669  cusgredg  29403  cusgrsizeindb0  29429  numclwlk1lem1  30350  numclwwlk3lem2lem  30364  grporndm  30491  vafval  30584  smfval  30586  hvmul0  31005  cmcmlem  31572  cmbr3i  31581  nmbdfnlbi  32030  nmcfnlbi  32033  nmopcoadji  32082  pjin2i  32174  hst1h  32208  xaddeq0  32730  sgnmul  32814  gsumhashmul  33055  cycpmconjslem1  33165  archirngz  33187  opprqusmulr  33506  constrinvcl  33807  cos9thpiminplylem1  33816  esumcst  34094  eulerpartlems  34392  dstfrvunirn  34507  subfacp1lem5  35206  cvmliftlem10  35316  fnessref  36375  fnemeet2  36385  poimirlem4  37648  poimirlem19  37663  poimirlem20  37664  poimirlem23  37667  poimirlem24  37668  poimirlem25  37669  poimirlem28  37672  ovoliunnfl  37686  voliunnfl  37688  volsupnfl  37689  itg2addnclem  37695  itg2addnc  37698  iblabsnc  37708  iblmulc2nc  37709  sdclem2  37766  blbnd  37811  ismgmOLD  37874  ismndo2  37898  rnresequniqs  38350  tendo0co2  40807  dvhfvadd  41110  dvh4dimN  41466  mzpcompact2lem  42774  diophrw  42782  eldioph2  42785  pellexlem5  42856  pell1qr1  42894  rmxy0  42947  wessf1ornlem  45209  cncfuni  45915  cncfiooicclem1  45922  dvnprodlem1  45975  fourierdlem38  46174  fourierdlem60  46195  fourierdlem61  46196  fourierdlem79  46214  fourierdlem112  46247  fourierswlem  46259  fouriersw  46260  fvmptrab  47321  fvmptrabdm  47322  fmtnofac2  47583  nn0sumshdiglem1  48601  eloprab1st2nd  48843  dmdm  49020  isinito2lem  49383