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 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  eqtr4id  2790  csbin  4382  csbif  4524  elpr2elpr  4812  csbuni  4880  csbima12  6044  somincom  6097  resresdm  6197  iotauni2  6470  csbfv12  6885  opabiotafun  6920  fvmptrabfv  6980  fndifnfp  7131  elxp4  7873  elxp5  7874  fo1stres  7968  fo2ndres  7969  sbcoteq1a  8004  eloprabi  8016  fo2ndf  8071  seqomlem2  8390  oev2  8458  odi  8514  fundmen  8978  xpsnen  8999  xpassen  9009  ac6sfi  9194  infeq5  9558  alephsuc3  10503  rankcf  10700  ine0  11585  nn0n0n1ge2  12505  fzval2  13464  fseq1p1m1  13552  fzosplitprm1  13733  hashfun  14399  hashf1  14419  hashtpg  14447  cshword  14753  wrd2pr2op  14905  wrd3tpop  14910  relexpsucrd  14995  relexpsucld  14996  fsum2dlem  15732  fprod2dlem  15945  ef4p  16080  sin01bnd  16152  odd2np1  16310  bitsinvp1  16418  smumullem  16461  oppcmon  17705  issubc2  17803  curf1cl  18194  curfcl  18198  cnvtsr  18554  ex-chn1  18603  sylow1lem1  19573  sylow2a  19594  ablsimpgfindlem1  20084  coe1fzgsumdlem  22268  evl1gsumdlem  22321  pmatcollpw3lem  22748  pptbas  22973  2ndcctbss  23420  txcmplem1  23606  qtopeu  23681  alexsubALTlem3  24014  ustuqtop5  24210  psmetdmdm  24270  xmetdmdm  24300  pcopt  24989  pcorevlem  24993  voliunlem1  25517  i1fima2  25646  iblabs  25796  dveflem  25946  deg1val  26061  abssinper  26485  mulcxplem  26648  dvatan  26899  lgamgulmlem2  26993  lgamgulmlem5  26996  lgseisenlem1  27338  dchrisumlem1  27452  pntlemr  27565  negsdi  28042  noseqrdg0  28299  eucliddivs  28368  pw2cut2  28454  krippenlem  28758  cusgredg  29493  cusgrsizeindb0  29518  numclwlk1lem1  30439  numclwwlk3lem2lem  30453  grporndm  30581  vafval  30674  smfval  30676  hvmul0  31095  cmcmlem  31662  cmbr3i  31671  nmbdfnlbi  32120  nmcfnlbi  32123  nmopcoadji  32172  pjin2i  32264  hst1h  32298  xaddeq0  32826  sgnmul  32908  gsumhashmul  33128  cycpmconjslem1  33215  archirngz  33250  opprqusmulr  33551  esplyfvaln  33718  esplyind  33719  extdgfialglem2  33837  constrinvcl  33917  cos9thpiminplylem1  33926  esumcst  34207  eulerpartlems  34504  dstfrvunirn  34619  subfacp1lem5  35366  cvmliftlem10  35476  fnessref  36539  fnemeet2  36549  poimirlem4  37945  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem28  37969  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  itg2addnclem  37992  itg2addnc  37995  iblabsnc  38005  iblmulc2nc  38006  sdclem2  38063  blbnd  38108  ismgmOLD  38171  ismndo2  38195  rnresequniqs  38655  tendo0co2  41234  dvhfvadd  41537  dvh4dimN  41893  mzpcompact2lem  43183  diophrw  43191  eldioph2  43194  pellexlem5  43261  pell1qr1  43299  rmxy0  43351  wessf1ornlem  45615  cncfuni  46314  cncfiooicclem1  46321  dvnprodlem1  46374  fourierdlem38  46573  fourierdlem60  46594  fourierdlem61  46595  fourierdlem79  46613  fourierdlem112  46646  fourierswlem  46658  fouriersw  46659  chnerlem1  47312  fvmptrab  47740  fvmptrabdm  47741  fmtnofac2  48032  nn0sumshdiglem1  49097  eloprab1st2nd  49343  dmdm  49528  isinito2lem  49973  termolmd  50145