Theorem eqtr2di 2797

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 2796	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2746	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqtr4id  2799  csbin  4465  csbif  4605  elpr2elpr  4893  csbuni  4960  csbima12  6108  somincom  6166  resresdm  6264  iotauni2  6542  csbfv12  6968  opabiotafun  7002  fvmptrabfv  7061  fndifnfp  7210  elxp4  7962  elxp5  7963  fo1stres  8056  fo2ndres  8057  sbcoteq1a  8092  eloprabi  8104  fo2ndf  8162  seqomlem2  8507  oev2  8579  odi  8635  fundmen  9096  xpsnen  9121  xpassen  9132  ac6sfi  9348  infeq5  9706  alephsuc3  10649  rankcf  10846  ine0  11725  nn0n0n1ge2  12620  fzval2  13570  fseq1p1m1  13658  fzosplitprm1  13827  hashfun  14486  hashf1  14506  hashtpg  14534  cshword  14839  wrd2pr2op  14992  wrd3tpop  14997  relexpsucrd  15082  relexpsucld  15083  fsum2dlem  15818  fprod2dlem  16028  ef4p  16161  sin01bnd  16233  odd2np1  16389  bitsinvp1  16495  smumullem  16538  oppcmon  17799  issubc2  17900  curf1cl  18298  curfcl  18302  cnvtsr  18658  sylow1lem1  19640  sylow2a  19661  ablsimpgfindlem1  20151  coe1fzgsumdlem  22328  evl1gsumdlem  22381  pmatcollpw3lem  22810  pptbas  23036  2ndcctbss  23484  txcmplem1  23670  qtopeu  23745  alexsubALTlem3  24078  ustuqtop5  24275  psmetdmdm  24336  xmetdmdm  24366  pcopt  25074  pcorevlem  25078  voliunlem1  25604  i1fima2  25733  iblabs  25884  dveflem  26037  deg1val  26155  abssinper  26581  mulcxplem  26744  dvatan  26996  lgamgulmlem2  27091  lgamgulmlem5  27094  lgseisenlem1  27437  dchrisumlem1  27551  pntlemr  27664  negsdi  28100  noseqrdg0  28331  krippenlem  28716  cusgredg  29459  cusgrsizeindb0  29485  numclwlk1lem1  30401  numclwwlk3lem2lem  30415  grporndm  30542  vafval  30635  smfval  30637  hvmul0  31056  cmcmlem  31623  cmbr3i  31632  nmbdfnlbi  32081  nmcfnlbi  32084  nmopcoadji  32133  pjin2i  32225  hst1h  32259  xaddeq0  32760  gsumhashmul  33040  cycpmconjslem1  33147  archirngz  33169  opprqusmulr  33484  esumcst  34027  eulerpartlems  34325  dstfrvunirn  34439  sgnmul  34507  subfacp1lem5  35152  cvmliftlem10  35262  fnessref  36323  fnemeet2  36333  poimirlem4  37584  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem28  37608  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  itg2addnclem  37631  itg2addnc  37634  iblabsnc  37644  iblmulc2nc  37645  sdclem2  37702  blbnd  37747  ismgmOLD  37810  ismndo2  37834  rnresequniqs  38288  tendo0co2  40745  dvhfvadd  41048  dvh4dimN  41404  mzpcompact2lem  42707  diophrw  42715  eldioph2  42718  pellexlem5  42789  pell1qr1  42827  rmxy0  42880  wessf1ornlem  45092  cncfuni  45807  cncfiooicclem1  45814  fourierdlem38  46066  fourierdlem60  46087  fourierdlem61  46088  fourierdlem79  46106  fourierdlem112  46139  fourierswlem  46151  fouriersw  46152  fvmptrab  47207  fvmptrabdm  47208  fmtnofac2  47443  nn0sumshdiglem1  48355