Theorem eqtr2di 2782

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 2781	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2736	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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  eqtr4id  2784  csbin  4408  csbif  4549  elpr2elpr  4836  csbuni  4903  csbima12  6053  somincom  6110  resresdm  6209  iotauni2  6483  csbfv12  6909  opabiotafun  6944  fvmptrabfv  7003  fndifnfp  7153  elxp4  7901  elxp5  7902  fo1stres  7997  fo2ndres  7998  sbcoteq1a  8033  eloprabi  8045  fo2ndf  8103  seqomlem2  8422  oev2  8490  odi  8546  fundmen  9005  xpsnen  9029  xpassen  9040  ac6sfi  9238  infeq5  9597  alephsuc3  10540  rankcf  10737  ine0  11620  nn0n0n1ge2  12517  fzval2  13478  fseq1p1m1  13566  fzosplitprm1  13745  hashfun  14409  hashf1  14429  hashtpg  14457  cshword  14763  wrd2pr2op  14916  wrd3tpop  14921  relexpsucrd  15006  relexpsucld  15007  fsum2dlem  15743  fprod2dlem  15953  ef4p  16088  sin01bnd  16160  odd2np1  16318  bitsinvp1  16426  smumullem  16469  oppcmon  17707  issubc2  17805  curf1cl  18196  curfcl  18200  cnvtsr  18554  sylow1lem1  19535  sylow2a  19556  ablsimpgfindlem1  20046  coe1fzgsumdlem  22197  evl1gsumdlem  22250  pmatcollpw3lem  22677  pptbas  22902  2ndcctbss  23349  txcmplem1  23535  qtopeu  23610  alexsubALTlem3  23943  ustuqtop5  24140  psmetdmdm  24200  xmetdmdm  24230  pcopt  24929  pcorevlem  24933  voliunlem1  25458  i1fima2  25587  iblabs  25737  dveflem  25890  deg1val  26008  abssinper  26437  mulcxplem  26600  dvatan  26852  lgamgulmlem2  26947  lgamgulmlem5  26950  lgseisenlem1  27293  dchrisumlem1  27407  pntlemr  27520  negsdi  27963  noseqrdg0  28208  eucliddivs  28272  krippenlem  28624  cusgredg  29358  cusgrsizeindb0  29384  numclwlk1lem1  30305  numclwwlk3lem2lem  30319  grporndm  30446  vafval  30539  smfval  30541  hvmul0  30960  cmcmlem  31527  cmbr3i  31536  nmbdfnlbi  31985  nmcfnlbi  31988  nmopcoadji  32037  pjin2i  32129  hst1h  32163  xaddeq0  32683  sgnmul  32767  gsumhashmul  33008  cycpmconjslem1  33118  archirngz  33150  opprqusmulr  33469  constrinvcl  33770  cos9thpiminplylem1  33779  esumcst  34060  eulerpartlems  34358  dstfrvunirn  34473  subfacp1lem5  35178  cvmliftlem10  35288  fnessref  36352  fnemeet2  36362  poimirlem4  37625  poimirlem19  37640  poimirlem20  37641  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem28  37649  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  itg2addnclem  37672  itg2addnc  37675  iblabsnc  37685  iblmulc2nc  37686  sdclem2  37743  blbnd  37788  ismgmOLD  37851  ismndo2  37875  rnresequniqs  38323  tendo0co2  40789  dvhfvadd  41092  dvh4dimN  41448  mzpcompact2lem  42746  diophrw  42754  eldioph2  42757  pellexlem5  42828  pell1qr1  42866  rmxy0  42919  wessf1ornlem  45186  cncfuni  45891  cncfiooicclem1  45898  dvnprodlem1  45951  fourierdlem38  46150  fourierdlem60  46171  fourierdlem61  46172  fourierdlem79  46190  fourierdlem112  46223  fourierswlem  46235  fouriersw  46236  fvmptrab  47297  fvmptrabdm  47298  fmtnofac2  47574  nn0sumshdiglem1  48614  eloprab1st2nd  48860  dmdm  49046  isinito2lem  49491  termolmd  49663