Theorem syl6req 2879

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

Syntax hints:   → wi 4   = wceq 1658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-cleq 2819

This theorem is referenced by:  syl6reqr  2881  csbin  4236  csbif  4362  csbuni  4689  csbima12  5725  somincom  5773  resresdm  5868  csbfv12  6478  opabiotafun  6507  fvmptrabfv  6558  fndifnfp  6695  elxp4  7373  elxp5  7374  fo1stres  7455  fo2ndres  7456  eloprabi  7496  fo2ndf  7549  seqomlem2  7813  oev2  7871  odi  7927  fundmen  8297  xpsnen  8314  xpassen  8324  ac6sfi  8474  infeq5  8812  alephsuc3  9718  rankcf  9915  ine0  10790  nn0n0n1ge2  11686  fzval2  12623  fseq1p1m1  12709  fzosplitprm1  12874  hashfun  13514  hashf1  13531  hashtpg  13557  cshword  13911  wrd2pr2op  14065  wrd3tpop  14070  fsum2dlem  14877  fprod2dlem  15084  ef4p  15216  sin01bnd  15288  odd2np1  15440  bitsinvp1  15545  smumullem  15588  oppcmon  16751  issubc2  16849  curf1cl  17222  curfcl  17226  cnvtsr  17576  sylow1lem1  18365  sylow2a  18386  coe1fzgsumdlem  20032  evl1gsumdlem  20081  pmatcollpw3lem  20959  pptbas  21184  2ndcctbss  21630  txcmplem1  21816  qtopeu  21891  alexsubALTlem3  22224  ustuqtop5  22420  psmetdmdm  22481  xmetdmdm  22511  pcopt  23192  pcorevlem  23196  voliunlem1  23717  i1fima2  23846  iblabs  23995  dveflem  24142  deg1val  24256  abssinper  24671  mulcxplem  24830  dvatan  25076  lgamgulmlem2  25170  lgamgulmlem5  25173  lgseisenlem1  25514  dchrisumlem1  25592  pntlemr  25705  krippenlem  26003  cusgredg  26723  cusgrsizeindb0  26748  wlknwwlksnsurOLD  27191  clwwlknonmpt2  27461  numclwlk1lem1  27773  numclwwlk3lem2lem  27799  grporndm  27921  vafval  28014  smfval  28016  hvmul0  28437  cmcmlem  29006  cmbr3i  29015  nmbdfnlbi  29464  nmcfnlbi  29467  nmopcoadji  29516  pjin2i  29608  hst1h  29642  xaddeq0  30066  archirngz  30289  esumcst  30671  eulerpartlems  30968  dstfrvunirn  31083  sgnmul  31151  subfacp1lem5  31713  cvmliftlem10  31823  fnessref  32891  fnemeet2  32901  poimirlem4  33958  poimirlem19  33973  poimirlem20  33974  poimirlem23  33977  poimirlem24  33978  poimirlem25  33979  poimirlem28  33982  ovoliunnfl  33996  voliunnfl  33998  volsupnfl  33999  itg2addnclem  34005  itg2addnc  34008  iblabsnc  34018  iblmulc2nc  34019  sdclem2  34081  blbnd  34129  ismgmOLD  34192  ismndo2  34216  rnresequniqs  34651  tendo0co2  36864  dvhfvadd  37167  dvh4dimN  37523  mzpcompact2lem  38159  diophrw  38167  eldioph2  38170  pellexlem5  38242  pell1qr1  38280  rmxy0  38332  cncfuni  40895  cncfiooicclem1  40902  fourierdlem38  41157  fourierdlem60  41178  fourierdlem61  41179  fourierdlem79  41197  fourierdlem112  41230  fourierswlem  41242  fouriersw  41243  fvmptrab  42196  fvmptrabdm  42197  fmtnofac2  42312  nn0sumshdiglem1  43263