Theorem eqtr2di 2815

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 2814	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2769	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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqtr4id  2817  csbin  4403  csbif  4543  elpr2elpr  4829  csbuni  4903  csbima12  6094  somincom  6146  resresdm  6253  iotauni2  6536  csbfv12  6961  opabiotafun  6996  fvmptrabfv  7057  fndifnfp  7212  elxp4  7968  elxp5  7969  fo1stres  8061  fo2ndres  8062  sbcoteq1a  8097  eloprabi  8109  fo2ndf  8169  seqomlem2  8499  oev2  8569  odi  8625  fundmen  9097  xpsnen  9118  xpassen  9128  ac6sfi  9313  infeq5  9675  alephsuc3  10704  rankcf  10901  ine0  11790  nn0n0n1ge2  12714  fzval2  13682  fseq1p1m1  13772  fzosplitprm1  13953  hashfun  14623  hashf1  14643  hashtpg  14671  cshword  14984  wrd2pr2op  15137  wrd3tpop  15142  s3rex  15144  relexpsucrd  15229  relexpsucld  15230  sgnmul  15303  fsum2dlem  15980  fprod2dlem  16191  ef4p  16325  sin01bnd  16397  odd2np1  16555  bitsinvp1  16663  smumullem  16706  oppcmon  17963  issubc2  18061  curf1cl  18452  curfcl  18456  cnvtsr  18812  ex-chn1  18861  sylow1lem1  19863  sylow2a  19884  ablsimpgfindlem1  20374  coe1fzgsumdlem  22676  evl1gsumdlem  22729  pmatcollpw3lem  23156  pptbas  23381  2ndcctbss  23829  txcmplem1  24015  qtopeu  24090  alexsubALTlem3  24423  ustuqtop5  24619  psmetdmdm  24679  xmetdmdm  24709  pcopt  25398  pcorevlem  25402  voliunlem1  25926  i1fima2  26055  iblabs  26204  dveflem  26354  deg1val  26469  abssinper  26906  mulcxplem  27069  dvatan  27320  lgamgulmlem2  27414  lgamgulmlem5  27417  lgseisenlem1  27759  dchrisumlem1  27873  pntlemr  27986  negsdi  28493  noseqrdg0  28750  eucliddivs  28819  pw2cut2  28905  krippenlem  29219  prlngmid2  29496  cusgredg  30062  cusgrsizeindb0  30087  numclwlk1lem1  31027  numclwwlk3lem2lem  31041  grporndm  31169  vafval  31262  smfval  31264  hvmul0  31683  cmcmlem  32250  cmbr3i  32259  nmbdfnlbi  32708  nmcfnlbi  32711  nmopcoadji  32760  pjin2i  32852  hst1h  32886  xaddeq0  33441  gsumhashmul  33727  cycpmconjslem1  33814  archirngz  33849  opprqusmulr  34119  dflringlem3  34132  dflring4  34134  selvply1rhm0  34269  esplyfvaln  34317  esplyind  34318  extdgfialglem2  34436  constrinvcl  34516  cos9thpiminplylem1  34525  esumcst  34806  eulerpartlems  35103  dstfrvunirn  35218  subfacp1lem5  36157  cvmliftlem10  36267  fnessref  37360  fnemeet2  37370  poimirlem4  38810  poimirlem19  38825  poimirlem20  38826  poimirlem23  38829  poimirlem24  38830  poimirlem25  38831  poimirlem28  38834  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  itg2addnclem  38857  itg2addnc  38860  iblabsnc  38870  iblmulc2nc  38871  sdclem2  38942  blbnd  38987  ismgmOLD  39050  ismndo2  39074  rnresequniqs  39532  tendo0co2  42111  dvhfvadd  42414  dvh4dimN  42770  mzpcompact2lem  44028  diophrw  44036  eldioph2  44039  pellexlem5  44106  pell1qr1  44144  rmxy0  44196  wessf1ornlem  46473  cncfuni  47169  cncfiooicclem1  47176  dvnprodlem1  47229  fourierdlem38  47428  fourierdlem60  47449  fourierdlem61  47450  fourierdlem79  47468  fourierdlem112  47501  fourierswlem  47513  fouriersw  47514  chnerlem1  48165  fvmptrab  48635  fvmptrabdm  48636  fmtnofac2  48927  nn0sumshdiglem1  50064  eloprab1st2nd  50310  dmdm  50498  isinito2lem  50964  termolmd  51184