Theorem syl6req 2873

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
syl6req.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6req.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
syl6req	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem syl6req

Step	Hyp	Ref	Expression
1		syl6req.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6req.2	. . 3 ⊢ 𝐵 = 𝐶
3	1, 2	syl6eq 2872	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2827	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 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  syl6reqr  2875  csbin  4391  csbif  4522  csbuni  4867  csbima12  5947  somincom  5994  resresdm  6090  csbfv12  6713  opabiotafun  6744  fvmptrabfv  6799  fndifnfp  6938  elxp4  7627  elxp5  7628  fo1stres  7715  fo2ndres  7716  eloprabi  7761  fo2ndf  7817  seqomlem2  8087  oev2  8148  odi  8205  fundmen  8583  xpsnen  8601  xpassen  8611  ac6sfi  8762  infeq5  9100  alephsuc3  10002  rankcf  10199  ine0  11075  nn0n0n1ge2  11963  fzval2  12896  fseq1p1m1  12982  fzosplitprm1  13148  hashfun  13799  hashf1  13816  hashtpg  13844  cshword  14153  wrd2pr2op  14305  wrd3tpop  14310  fsum2dlem  15125  fprod2dlem  15334  ef4p  15466  sin01bnd  15538  odd2np1  15690  bitsinvp1  15798  smumullem  15841  oppcmon  17008  issubc2  17106  curf1cl  17478  curfcl  17482  cnvtsr  17832  sylow1lem1  18723  sylow2a  18744  ablsimpgfindlem1  19229  coe1fzgsumdlem  20469  evl1gsumdlem  20519  pmatcollpw3lem  21391  pptbas  21616  2ndcctbss  22063  txcmplem1  22249  qtopeu  22324  alexsubALTlem3  22657  ustuqtop5  22854  psmetdmdm  22915  xmetdmdm  22945  pcopt  23626  pcorevlem  23630  voliunlem1  24151  i1fima2  24280  iblabs  24429  dveflem  24576  deg1val  24690  abssinper  25106  mulcxplem  25267  dvatan  25513  lgamgulmlem2  25607  lgamgulmlem5  25610  lgseisenlem1  25951  dchrisumlem1  26065  pntlemr  26178  krippenlem  26476  cusgredg  27206  cusgrsizeindb0  27231  numclwlk1lem1  28148  numclwwlk3lem2lem  28162  grporndm  28287  vafval  28380  smfval  28382  hvmul0  28801  cmcmlem  29368  cmbr3i  29377  nmbdfnlbi  29826  nmcfnlbi  29829  nmopcoadji  29878  pjin2i  29970  hst1h  30004  xaddeq0  30477  cycpmconjslem1  30796  archirngz  30818  esumcst  31322  eulerpartlems  31618  dstfrvunirn  31732  sgnmul  31800  subfacp1lem5  32431  cvmliftlem10  32541  fnessref  33705  fnemeet2  33715  poimirlem4  34911  poimirlem19  34926  poimirlem20  34927  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem28  34935  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  itg2addnclem  34958  itg2addnc  34961  iblabsnc  34971  iblmulc2nc  34972  sdclem2  35032  blbnd  35080  ismgmOLD  35143  ismndo2  35167  rnresequniqs  35604  tendo0co2  37939  dvhfvadd  38242  dvh4dimN  38598  mzpcompact2lem  39368  diophrw  39376  eldioph2  39379  pellexlem5  39450  pell1qr1  39488  rmxy0  39540  wessf1ornlem  41465  cncfuni  42189  cncfiooicclem1  42196  fourierdlem38  42450  fourierdlem60  42471  fourierdlem61  42472  fourierdlem79  42490  fourierdlem112  42523  fourierswlem  42535  fouriersw  42536  fvmptrab  43511  fvmptrabdm  43512  fmtnofac2  43751  nn0sumshdiglem1  44701