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  6234  iotauni2  6510  csbfv12  6930  opabiotafun  6965  fvmptrabfv  7026  fndifnfp  7181  elxp4  7934  elxp5  7935  fo1stres  8027  fo2ndres  8028  sbcoteq1a  8062  eloprabi  8074  fo2ndf  8132  seqomlem2  8461  oev2  8531  odi  8587  fundmen  9059  xpsnen  9080  xpassen  9090  ac6sfi  9275  infeq5  9638  alephsuc3  10665  rankcf  10862  ine0  11751  nn0n0n1ge2  12674  fzval2  13642  fseq1p1m1  13732  fzosplitprm1  13913  hashfun  14582  hashf1  14602  hashtpg  14630  cshword  14942  wrd2pr2op  15094  wrd3tpop  15099  s3rex  15101  relexpsucrd  15186  relexpsucld  15187  sgnmul  15260  fsum2dlem  15936  fprod2dlem  16147  ef4p  16281  sin01bnd  16353  odd2np1  16511  bitsinvp1  16619  smumullem  16662  oppcmon  17913  issubc2  18011  curf1cl  18402  curfcl  18406  cnvtsr  18762  ex-chn1  18811  sylow1lem1  19812  sylow2a  19833  ablsimpgfindlem1  20323  coe1fzgsumdlem  22621  evl1gsumdlem  22674  pmatcollpw3lem  23101  pptbas  23326  2ndcctbss  23774  txcmplem1  23960  qtopeu  24035  alexsubALTlem3  24368  ustuqtop5  24564  psmetdmdm  24624  xmetdmdm  24654  pcopt  25343  pcorevlem  25347  voliunlem1  25871  i1fima2  26000  iblabs  26149  dveflem  26299  deg1val  26414  abssinper  26849  mulcxplem  27012  dvatan  27263  lgamgulmlem2  27357  lgamgulmlem5  27360  lgseisenlem1  27702  dchrisumlem1  27816  pntlemr  27929  negsdi  28436  noseqrdg0  28693  eucliddivs  28762  pw2cut2  28848  krippenlem  29162  prlngmid2  29439  cusgredg  30005  cusgrsizeindb0  30030  numclwlk1lem1  30970  numclwwlk3lem2lem  30984  grporndm  31112  vafval  31205  smfval  31207  hvmul0  31626  cmcmlem  32193  cmbr3i  32202  nmbdfnlbi  32651  nmcfnlbi  32654  nmopcoadji  32703  pjin2i  32795  hst1h  32829  xaddeq0  33345  gsumhashmul  33628  cycpmconjslem1  33715  archirngz  33750  opprqusmulr  34015  dflringlem3  34028  dflring4  34030  selvply1rhm0  34158  esplyfvaln  34206  esplyind  34207  extdgfialglem2  34325  constrinvcl  34405  cos9thpiminplylem1  34414  esumcst  34695  eulerpartlems  34992  dstfrvunirn  35107  subfacp1lem5  35949  cvmliftlem10  36059  fnessref  37145  fnemeet2  37155  poimirlem4  38542  poimirlem19  38557  poimirlem20  38558  poimirlem23  38561  poimirlem24  38562  poimirlem25  38563  poimirlem28  38566  ovoliunnfl  38580  voliunnfl  38582  volsupnfl  38583  itg2addnclem  38589  itg2addnc  38592  iblabsnc  38602  iblmulc2nc  38603  sdclem2  38676  blbnd  38721  ismgmOLD  38784  ismndo2  38808  rnresequniqs  39266  tendo0co2  41845  dvhfvadd  42148  dvh4dimN  42504  mzpcompact2lem  43761  diophrw  43769  eldioph2  43772  pellexlem5  43839  pell1qr1  43877  rmxy0  43929  wessf1ornlem  46199  cncfuni  46895  cncfiooicclem1  46902  dvnprodlem1  46955  fourierdlem38  47154  fourierdlem60  47175  fourierdlem61  47176  fourierdlem79  47194  fourierdlem112  47227  fourierswlem  47239  fouriersw  47240  chnerlem1  47891  fvmptrab  48361  fvmptrabdm  48362  fmtnofac2  48653  nn0sumshdiglem1  49732  eloprab1st2nd  49977  dmdm  50160  isinito2lem  50605  termolmd  50777