Theorem eqtr2di 2813

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  eqtr4id  2815  csbin  4400  csbif  4540  elpr2elpr  4829  csbuni  4898  csbima12  6076  somincom  6128  resresdm  6233  iotauni2  6509  csbfv12  6928  opabiotafun  6963  fvmptrabfv  7024  fndifnfp  7179  elxp4  7932  elxp5  7933  fo1stres  8025  fo2ndres  8026  sbcoteq1a  8060  eloprabi  8072  fo2ndf  8130  seqomlem2  8454  oev2  8524  odi  8580  fundmen  9052  xpsnen  9073  xpassen  9083  ac6sfi  9268  infeq5  9631  alephsuc3  10658  rankcf  10855  ine0  11744  nn0n0n1ge2  12667  fzval2  13635  fseq1p1m1  13725  fzosplitprm1  13906  hashfun  14575  hashf1  14595  hashtpg  14623  cshword  14935  wrd2pr2op  15087  wrd3tpop  15092  s3rex  15094  relexpsucrd  15179  relexpsucld  15180  sgnmul  15253  fsum2dlem  15929  fprod2dlem  16140  ef4p  16274  sin01bnd  16346  odd2np1  16504  bitsinvp1  16612  smumullem  16655  oppcmon  17906  issubc2  18004  curf1cl  18395  curfcl  18399  cnvtsr  18755  ex-chn1  18804  sylow1lem1  19805  sylow2a  19826  ablsimpgfindlem1  20316  coe1fzgsumdlem  22614  evl1gsumdlem  22667  pmatcollpw3lem  23094  pptbas  23319  2ndcctbss  23767  txcmplem1  23953  qtopeu  24028  alexsubALTlem3  24361  ustuqtop5  24557  psmetdmdm  24617  xmetdmdm  24647  pcopt  25336  pcorevlem  25340  voliunlem1  25864  i1fima2  25993  iblabs  26142  dveflem  26292  deg1val  26407  abssinper  26842  mulcxplem  27005  dvatan  27256  lgamgulmlem2  27350  lgamgulmlem5  27353  lgseisenlem1  27695  dchrisumlem1  27809  pntlemr  27922  negsdi  28429  noseqrdg0  28686  eucliddivs  28755  pw2cut2  28841  krippenlem  29155  prlngmid2  29432  cusgredg  29998  cusgrsizeindb0  30023  numclwlk1lem1  30963  numclwwlk3lem2lem  30977  grporndm  31105  vafval  31198  smfval  31200  hvmul0  31619  cmcmlem  32186  cmbr3i  32195  nmbdfnlbi  32644  nmcfnlbi  32647  nmopcoadji  32696  pjin2i  32788  hst1h  32822  xaddeq0  33338  gsumhashmul  33621  cycpmconjslem1  33708  archirngz  33743  opprqusmulr  34008  dflringlem3  34021  dflring4  34023  selvply1rhm0  34151  esplyfvaln  34199  esplyind  34200  extdgfialglem2  34318  constrinvcl  34398  cos9thpiminplylem1  34407  esumcst  34688  eulerpartlems  34985  dstfrvunirn  35100  subfacp1lem5  35928  cvmliftlem10  36038  fnessref  37125  fnemeet2  37135  poimirlem4  38522  poimirlem19  38537  poimirlem20  38538  poimirlem23  38541  poimirlem24  38542  poimirlem25  38543  poimirlem28  38546  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  itg2addnclem  38569  itg2addnc  38572  iblabsnc  38582  iblmulc2nc  38583  sdclem2  38656  blbnd  38701  ismgmOLD  38764  ismndo2  38788  rnresequniqs  39246  tendo0co2  41825  dvhfvadd  42128  dvh4dimN  42484  mzpcompact2lem  43741  diophrw  43749  eldioph2  43752  pellexlem5  43819  pell1qr1  43857  rmxy0  43909  wessf1ornlem  46169  cncfuni  46865  cncfiooicclem1  46872  dvnprodlem1  46925  fourierdlem38  47124  fourierdlem60  47145  fourierdlem61  47146  fourierdlem79  47164  fourierdlem112  47197  fourierswlem  47209  fouriersw  47210  chnerlem1  47861  fvmptrab  48331  fvmptrabdm  48332  fmtnofac2  48623  nn0sumshdiglem1  49702  eloprab1st2nd  49947  dmdm  50130  isinito2lem  50575  termolmd  50747