Theorem eqtr2di 2783

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 2782	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2737	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 2121  ax-ext 2703

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

This theorem is referenced by:  eqtr4id  2785  csbin  4387  csbif  4528  elpr2elpr  4816  csbuni  4883  csbima12  6023  somincom  6076  resresdm  6175  iotauni2  6448  csbfv12  6862  opabiotafun  6897  fvmptrabfv  6956  fndifnfp  7105  elxp4  7847  elxp5  7848  fo1stres  7942  fo2ndres  7943  sbcoteq1a  7978  eloprabi  7990  fo2ndf  8046  seqomlem2  8365  oev2  8433  odi  8489  fundmen  8948  xpsnen  8969  xpassen  8979  ac6sfi  9163  infeq5  9522  alephsuc3  10466  rankcf  10663  ine0  11547  nn0n0n1ge2  12444  fzval2  13405  fseq1p1m1  13493  fzosplitprm1  13673  hashfun  14339  hashf1  14359  hashtpg  14387  cshword  14693  wrd2pr2op  14845  wrd3tpop  14850  relexpsucrd  14935  relexpsucld  14936  fsum2dlem  15672  fprod2dlem  15882  ef4p  16017  sin01bnd  16089  odd2np1  16247  bitsinvp1  16355  smumullem  16398  oppcmon  17640  issubc2  17738  curf1cl  18129  curfcl  18133  cnvtsr  18489  ex-chn1  18538  sylow1lem1  19505  sylow2a  19526  ablsimpgfindlem1  20016  coe1fzgsumdlem  22213  evl1gsumdlem  22266  pmatcollpw3lem  22693  pptbas  22918  2ndcctbss  23365  txcmplem1  23551  qtopeu  23626  alexsubALTlem3  23959  ustuqtop5  24155  psmetdmdm  24215  xmetdmdm  24245  pcopt  24944  pcorevlem  24948  voliunlem1  25473  i1fima2  25602  iblabs  25752  dveflem  25905  deg1val  26023  abssinper  26452  mulcxplem  26615  dvatan  26867  lgamgulmlem2  26962  lgamgulmlem5  26965  lgseisenlem1  27308  dchrisumlem1  27422  pntlemr  27535  negsdi  27987  noseqrdg0  28232  eucliddivs  28296  pw2cut2  28377  krippenlem  28663  cusgredg  29397  cusgrsizeindb0  29423  numclwlk1lem1  30341  numclwwlk3lem2lem  30355  grporndm  30482  vafval  30575  smfval  30577  hvmul0  30996  cmcmlem  31563  cmbr3i  31572  nmbdfnlbi  32021  nmcfnlbi  32024  nmopcoadji  32073  pjin2i  32165  hst1h  32199  xaddeq0  32728  sgnmul  32810  gsumhashmul  33033  cycpmconjslem1  33115  archirngz  33150  opprqusmulr  33448  extdgfialglem2  33698  constrinvcl  33778  cos9thpiminplylem1  33787  esumcst  34068  eulerpartlems  34365  dstfrvunirn  34480  subfacp1lem5  35220  cvmliftlem10  35330  fnessref  36391  fnemeet2  36401  poimirlem4  37664  poimirlem19  37679  poimirlem20  37680  poimirlem23  37683  poimirlem24  37684  poimirlem25  37685  poimirlem28  37688  ovoliunnfl  37702  voliunnfl  37704  volsupnfl  37705  itg2addnclem  37711  itg2addnc  37714  iblabsnc  37724  iblmulc2nc  37725  sdclem2  37782  blbnd  37827  ismgmOLD  37890  ismndo2  37914  rnresequniqs  38362  tendo0co2  40827  dvhfvadd  41130  dvh4dimN  41486  mzpcompact2lem  42784  diophrw  42792  eldioph2  42795  pellexlem5  42866  pell1qr1  42904  rmxy0  42956  wessf1ornlem  45222  cncfuni  45924  cncfiooicclem1  45931  dvnprodlem1  45984  fourierdlem38  46183  fourierdlem60  46204  fourierdlem61  46205  fourierdlem79  46223  fourierdlem112  46256  fourierswlem  46268  fouriersw  46269  fvmptrab  47323  fvmptrabdm  47324  fmtnofac2  47600  nn0sumshdiglem1  48653  eloprab1st2nd  48899  dmdm  49085  isinito2lem  49530  termolmd  49702