Theorem syl6req 2661

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

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  syl6reqr  2663  csbin  3962  csbif  4088  csbuni  4402  csbima12  5402  somincom  5449  csbfv12  6141  opabiotafun  6169  fndifnfp  6347  elxp4  7003  elxp5  7004  fo1stres  7083  fo2ndres  7084  eloprabi  7121  fo2ndf  7171  seqomlem2  7433  oev2  7490  odi  7546  fundmen  7916  xpsnen  7929  xpassen  7939  ac6sfi  8089  infeq5  8417  alephsuc3  9281  rankcf  9478  ine0  10344  nn0n0n1ge2  11235  fzval2  12200  fseq1p1m1  12283  hashfun  13084  hashf1  13098  hashtpg  13121  cshword  13388  wrd2pr2op  13535  wrd3tpop  13539  fsum2dlem  14343  fprod2dlem  14549  ef4p  14682  sin01bnd  14754  odd2np1  14903  bitsinvp1  15009  smumullem  15052  oppcmon  16221  issubc2  16319  curf1cl  16691  curfcl  16695  cnvtsr  17045  sylow1lem1  17836  sylow2a  17857  coe1fzgsumdlem  19492  evl1gsumdlem  19541  pmatcollpw3lem  20407  pptbas  20622  2ndcctbss  21068  txcmplem1  21254  qtopeu  21329  alexsubALTlem3  21663  ustuqtop5  21859  psmetdmdm  21920  xmetdmdm  21950  pcopt  22630  pcorevlem  22634  voliunlem1  23125  i1fima2  23252  iblabs  23401  dveflem  23546  deg1val  23660  abssinper  24074  mulcxplem  24230  dvatan  24462  lgamgulmlem2  24556  lgamgulmlem5  24559  lgseisenlem1  24900  dchrisumlem1  24978  pntlemr  25091  krippenlem  25385  usgra2wlkspthlem1  26147  wlknwwlknsur  26240  grporndm  26748  vafval  26842  smfval  26844  hvmul0  27265  cmcmlem  27834  cmbr3i  27843  nmbdfnlbi  28292  nmcfnlbi  28295  nmopcoadji  28344  pjin2i  28436  hst1h  28470  xaddeq0  28907  archirngz  29074  esumcst  29452  eulerpartlems  29749  dstfrvunirn  29863  sgnmul  29931  subfacp1lem5  30420  cvmliftlem10  30530  fnessref  31522  fnemeet2  31532  poimirlem4  32583  poimirlem19  32598  poimirlem20  32599  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem28  32607  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  itg2addnclem  32631  itg2addnc  32634  iblabsnc  32644  iblmulc2nc  32645  sdclem2  32708  blbnd  32756  ismgmOLD  32819  ismndo2  32843  tendo0co2  35094  dvhfvadd  35398  dvh4dimN  35754  mzpcompact2lem  36332  diophrw  36340  eldioph2  36343  pellexlem5  36415  pell1qr1  36453  rmxy0  36506  cncfuni  38772  cncfiooicclem1  38779  fourierdlem38  39038  fourierdlem60  39059  fourierdlem61  39060  fourierdlem79  39078  fourierdlem112  39111  fourierswlem  39123  fouriersw  39124  fmtnofac2  40019  cshword2  40300  resresdm  40319  cusgredg  40646  cusgrsizeindb0  40665  wlknwwlksnsur  41087  nn0sumshdiglem1  42213