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 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  eqtr4id  2817  csbin  4407  csbif  4545  elpr2elpr  4834  csbuni  4903  csbima12  6081  somincom  6134  resresdm  6234  iotauni2  6508  csbfv12  6926  opabiotafun  6961  fvmptrabfv  7022  fndifnfp  7174  elxp4  7915  elxp5  7916  fo1stres  8008  fo2ndres  8009  sbcoteq1a  8044  eloprabi  8056  fo2ndf  8112  seqomlem2  8434  oev2  8504  odi  8560  fundmen  9024  xpsnen  9045  xpassen  9055  ac6sfi  9240  infeq5  9602  alephsuc3  10560  rankcf  10757  ine0  11644  nn0n0n1ge2  12567  fzval2  13533  fseq1p1m1  13622  fzosplitprm1  13803  hashfun  14470  hashf1  14490  hashtpg  14518  cshword  14824  wrd2pr2op  14976  wrd3tpop  14981  relexpsucrd  15066  relexpsucld  15067  sgnmul  15140  fsum2dlem  15817  fprod2dlem  16030  ef4p  16164  sin01bnd  16236  odd2np1  16394  bitsinvp1  16502  smumullem  16545  oppcmon  17790  issubc2  17888  curf1cl  18279  curfcl  18283  cnvtsr  18639  ex-chn1  18688  sylow1lem1  19663  sylow2a  19684  ablsimpgfindlem1  20174  coe1fzgsumdlem  22463  evl1gsumdlem  22516  pmatcollpw3lem  22940  pptbas  23165  2ndcctbss  23612  txcmplem1  23798  qtopeu  23873  alexsubALTlem3  24206  ustuqtop5  24402  psmetdmdm  24462  xmetdmdm  24492  pcopt  25181  pcorevlem  25185  voliunlem1  25709  i1fima2  25838  iblabs  25988  dveflem  26138  deg1val  26253  abssinper  26686  mulcxplem  26849  dvatan  27100  lgamgulmlem2  27194  lgamgulmlem5  27197  lgseisenlem1  27539  dchrisumlem1  27653  pntlemr  27766  negsdi  28243  noseqrdg0  28500  eucliddivs  28569  pw2cut2  28655  krippenlem  28967  prlngmid2  29211  cusgredg  29774  cusgrsizeindb0  29799  numclwlk1lem1  30720  numclwwlk3lem2lem  30734  grporndm  30862  vafval  30955  smfval  30957  hvmul0  31376  cmcmlem  31943  cmbr3i  31952  nmbdfnlbi  32401  nmcfnlbi  32404  nmopcoadji  32453  pjin2i  32545  hst1h  32579  xaddeq0  33098  gsumhashmul  33387  cycpmconjslem1  33474  archirngz  33509  opprqusmulr  33773  dflringlem3  33786  dflring4  33788  selvply1rhm0  33916  esplyfvaln  33964  esplyind  33965  extdgfialglem2  34083  constrinvcl  34163  cos9thpiminplylem1  34172  esumcst  34453  eulerpartlems  34750  dstfrvunirn  34865  subfacp1lem5  35676  cvmliftlem10  35786  fnessref  36868  fnemeet2  36878  poimirlem4  38275  poimirlem19  38290  poimirlem20  38291  poimirlem23  38294  poimirlem24  38295  poimirlem25  38296  poimirlem28  38299  ovoliunnfl  38313  voliunnfl  38315  volsupnfl  38316  itg2addnclem  38322  itg2addnc  38325  iblabsnc  38335  iblmulc2nc  38336  sdclem2  38393  blbnd  38438  ismgmOLD  38501  ismndo2  38525  rnresequniqs  38983  tendo0co2  41562  dvhfvadd  41865  dvh4dimN  42221  mzpcompact2lem  43482  diophrw  43490  eldioph2  43493  pellexlem5  43560  pell1qr1  43598  rmxy0  43650  wessf1ornlem  45903  cncfuni  46600  cncfiooicclem1  46607  dvnprodlem1  46660  fourierdlem38  46859  fourierdlem60  46880  fourierdlem61  46881  fourierdlem79  46899  fourierdlem112  46932  fourierswlem  46944  fouriersw  46945  chnerlem1  47598  fvmptrab  48029  fvmptrabdm  48030  fmtnofac2  48321  nn0sumshdiglem1  49401  eloprab1st2nd  49646  dmdm  49831  isinito2lem  50276  termolmd  50448