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 2742	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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  eqtr4id  2790  csbin  4394  csbif  4537  elpr2elpr  4825  csbuni  4893  csbima12  6038  somincom  6091  resresdm  6191  iotauni2  6464  csbfv12  6879  opabiotafun  6914  fvmptrabfv  6973  fndifnfp  7122  elxp4  7864  elxp5  7865  fo1stres  7959  fo2ndres  7960  sbcoteq1a  7995  eloprabi  8007  fo2ndf  8063  seqomlem2  8382  oev2  8450  odi  8506  fundmen  8968  xpsnen  8989  xpassen  8999  ac6sfi  9184  infeq5  9546  alephsuc3  10491  rankcf  10688  ine0  11572  nn0n0n1ge2  12469  fzval2  13426  fseq1p1m1  13514  fzosplitprm1  13694  hashfun  14360  hashf1  14380  hashtpg  14408  cshword  14714  wrd2pr2op  14866  wrd3tpop  14871  relexpsucrd  14956  relexpsucld  14957  fsum2dlem  15693  fprod2dlem  15903  ef4p  16038  sin01bnd  16110  odd2np1  16268  bitsinvp1  16376  smumullem  16419  oppcmon  17662  issubc2  17760  curf1cl  18151  curfcl  18155  cnvtsr  18511  ex-chn1  18560  sylow1lem1  19527  sylow2a  19548  ablsimpgfindlem1  20038  coe1fzgsumdlem  22247  evl1gsumdlem  22300  pmatcollpw3lem  22727  pptbas  22952  2ndcctbss  23399  txcmplem1  23585  qtopeu  23660  alexsubALTlem3  23993  ustuqtop5  24189  psmetdmdm  24249  xmetdmdm  24279  pcopt  24978  pcorevlem  24982  voliunlem1  25507  i1fima2  25636  iblabs  25786  dveflem  25939  deg1val  26057  abssinper  26486  mulcxplem  26649  dvatan  26901  lgamgulmlem2  26996  lgamgulmlem5  26999  lgseisenlem1  27342  dchrisumlem1  27456  pntlemr  27569  negsdi  28046  noseqrdg0  28303  eucliddivs  28372  pw2cut2  28458  krippenlem  28762  cusgredg  29497  cusgrsizeindb0  29523  numclwlk1lem1  30444  numclwwlk3lem2lem  30458  grporndm  30585  vafval  30678  smfval  30680  hvmul0  31099  cmcmlem  31666  cmbr3i  31675  nmbdfnlbi  32124  nmcfnlbi  32127  nmopcoadji  32176  pjin2i  32268  hst1h  32302  xaddeq0  32833  sgnmul  32916  gsumhashmul  33150  cycpmconjslem1  33236  archirngz  33271  opprqusmulr  33572  esplyind  33731  extdgfialglem2  33850  constrinvcl  33930  cos9thpiminplylem1  33939  esumcst  34220  eulerpartlems  34517  dstfrvunirn  34632  subfacp1lem5  35378  cvmliftlem10  35488  fnessref  36551  fnemeet2  36561  poimirlem4  37825  poimirlem19  37840  poimirlem20  37841  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem28  37849  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  itg2addnclem  37872  itg2addnc  37875  iblabsnc  37885  iblmulc2nc  37886  sdclem2  37943  blbnd  37988  ismgmOLD  38051  ismndo2  38075  rnresequniqs  38527  tendo0co2  41048  dvhfvadd  41351  dvh4dimN  41707  mzpcompact2lem  42993  diophrw  43001  eldioph2  43004  pellexlem5  43075  pell1qr1  43113  rmxy0  43165  wessf1ornlem  45429  cncfuni  46130  cncfiooicclem1  46137  dvnprodlem1  46190  fourierdlem38  46389  fourierdlem60  46410  fourierdlem61  46411  fourierdlem79  46429  fourierdlem112  46462  fourierswlem  46474  fouriersw  46475  chnerlem1  47126  fvmptrab  47538  fvmptrabdm  47539  fmtnofac2  47815  nn0sumshdiglem1  48867  eloprab1st2nd  49113  dmdm  49298  isinito2lem  49743  termolmd  49915