Theorem eqtr2di 2785

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 2784	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2739	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 2705

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

This theorem is referenced by:  eqtr4id  2787  csbin  4391  csbif  4532  elpr2elpr  4820  csbuni  4888  csbima12  6032  somincom  6085  resresdm  6185  iotauni2  6458  csbfv12  6873  opabiotafun  6908  fvmptrabfv  6967  fndifnfp  7116  elxp4  7858  elxp5  7859  fo1stres  7953  fo2ndres  7954  sbcoteq1a  7989  eloprabi  8001  fo2ndf  8057  seqomlem2  8376  oev2  8444  odi  8500  fundmen  8960  xpsnen  8981  xpassen  8991  ac6sfi  9175  infeq5  9534  alephsuc3  10478  rankcf  10675  ine0  11559  nn0n0n1ge2  12456  fzval2  13412  fseq1p1m1  13500  fzosplitprm1  13680  hashfun  14346  hashf1  14366  hashtpg  14394  cshword  14700  wrd2pr2op  14852  wrd3tpop  14857  relexpsucrd  14942  relexpsucld  14943  fsum2dlem  15679  fprod2dlem  15889  ef4p  16024  sin01bnd  16096  odd2np1  16254  bitsinvp1  16362  smumullem  16405  oppcmon  17647  issubc2  17745  curf1cl  18136  curfcl  18140  cnvtsr  18496  ex-chn1  18545  sylow1lem1  19512  sylow2a  19533  ablsimpgfindlem1  20023  coe1fzgsumdlem  22219  evl1gsumdlem  22272  pmatcollpw3lem  22699  pptbas  22924  2ndcctbss  23371  txcmplem1  23557  qtopeu  23632  alexsubALTlem3  23965  ustuqtop5  24161  psmetdmdm  24221  xmetdmdm  24251  pcopt  24950  pcorevlem  24954  voliunlem1  25479  i1fima2  25608  iblabs  25758  dveflem  25911  deg1val  26029  abssinper  26458  mulcxplem  26621  dvatan  26873  lgamgulmlem2  26968  lgamgulmlem5  26971  lgseisenlem1  27314  dchrisumlem1  27428  pntlemr  27541  negsdi  27993  noseqrdg0  28238  eucliddivs  28302  pw2cut2  28383  krippenlem  28669  cusgredg  29404  cusgrsizeindb0  29430  numclwlk1lem1  30351  numclwwlk3lem2lem  30365  grporndm  30492  vafval  30585  smfval  30587  hvmul0  31006  cmcmlem  31573  cmbr3i  31582  nmbdfnlbi  32031  nmcfnlbi  32034  nmopcoadji  32083  pjin2i  32175  hst1h  32209  xaddeq0  32740  sgnmul  32823  gsumhashmul  33048  cycpmconjslem1  33130  archirngz  33165  opprqusmulr  33463  esplyind  33613  extdgfialglem2  33727  constrinvcl  33807  cos9thpiminplylem1  33816  esumcst  34097  eulerpartlems  34394  dstfrvunirn  34509  subfacp1lem5  35249  cvmliftlem10  35359  fnessref  36422  fnemeet2  36432  poimirlem4  37684  poimirlem19  37699  poimirlem20  37700  poimirlem23  37703  poimirlem24  37704  poimirlem25  37705  poimirlem28  37708  ovoliunnfl  37722  voliunnfl  37724  volsupnfl  37725  itg2addnclem  37731  itg2addnc  37734  iblabsnc  37744  iblmulc2nc  37745  sdclem2  37802  blbnd  37847  ismgmOLD  37910  ismndo2  37934  rnresequniqs  38386  tendo0co2  40907  dvhfvadd  41210  dvh4dimN  41566  mzpcompact2lem  42868  diophrw  42876  eldioph2  42879  pellexlem5  42950  pell1qr1  42988  rmxy0  43040  wessf1ornlem  45306  cncfuni  46008  cncfiooicclem1  46015  dvnprodlem1  46068  fourierdlem38  46267  fourierdlem60  46288  fourierdlem61  46289  fourierdlem79  46307  fourierdlem112  46340  fourierswlem  46352  fouriersw  46353  chnerlem1  47004  fvmptrab  47416  fvmptrabdm  47417  fmtnofac2  47693  nn0sumshdiglem1  48746  eloprab1st2nd  48992  dmdm  49178  isinito2lem  49623  termolmd  49795