Theorem syl6req 2479

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

Hypotheses

Ref	Expression
syl6req.1	|- ( ph -> A = B )
syl6req.2	|- B = C

Assertion

Ref	Expression
syl6req	|- ( ph -> C = A )

Proof of Theorem syl6req

Step	Hyp	Ref	Expression
1		syl6req.1	. . 3 |- ( ph -> A = B )
2		syl6req.2	. . 3 |- B = C
3	1, 2	syl6eq 2478	. 2 |- ( ph -> A = C )
4	3	eqcomd 2434	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-cleq 2421

This theorem is referenced by:  syl6reqr  2481  csbin  3772  csbif  3904  csbuni  4190  csbima12  5147  somincom  5196  csbfv12  5860  opabiotafun  5886  fndifnfp  6052  elxp4  6695  elxp5  6696  fo1stres  6775  fo2ndres  6776  eloprabi  6813  fo2ndf  6858  seqomlem2  7123  oev2  7180  odi  7235  fundmen  7597  xpsnen  7609  xpassen  7619  ac6sfi  7768  infeq5  8095  alephsuc3  8956  rankcf  9153  ine0  10005  nn0n0n1ge2  10883  fzval2  11738  fseq1p1m1  11819  hashfun  12557  hashf1  12568  hashtpg  12589  cshword  12839  fsum2dlem  13774  fprod2dlem  13977  ef4p  14110  sin01bnd  14182  odd2np1  14308  bitsinvp1  14366  smumullem  14409  oppcmon  15586  issubc2  15684  curf1cl  16056  curfcl  16060  cnvtsr  16411  sylow1lem1  17193  sylow2a  17214  coe1fzgsumdlem  18838  evl1gsumdlem  18887  pmatcollpw3lem  19749  pptbas  19965  2ndcctbss  20412  txcmplem1  20598  qtopeu  20673  alexsubALTlem3  21006  ustuqtop5  21202  psmetdmdm  21263  xmetdmdm  21292  pcopt  21995  pcorevlem  21999  voliunlem1  22445  i1fima2  22579  iblabs  22728  dveflem  22873  deg1val  22987  abssinper  23415  mulcxplem  23571  dvatan  23803  lgamgulmlem2  23897  lgamgulmlem5  23900  lgseisenlem1  24219  dchrisumlem1  24269  pntlemr  24382  krippenlem  24677  usgra2wlkspthlem1  25289  wlknwwlknsur  25382  grporndm  25880  ismgmOLD  25990  ismndo2  26015  vafval  26164  smfval  26166  hvmul0  26619  cmcmlem  27186  cmbr3i  27195  nmbdfnlbi  27644  nmcfnlbi  27647  nmopcoadji  27696  pjin2i  27788  hst1h  27822  xaddeq0  28280  archirngz  28457  esumcst  28836  eulerpartlems  29145  dstfrvunirn  29259  sgnmul  29365  subfacp1lem5  29859  cvmliftlem10  29969  ghomfo  30261  fnessref  30962  fnemeet2  30972  poimirlem4  31851  poimirlem19  31866  poimirlem20  31867  poimirlem23  31870  poimirlem24  31871  poimirlem25  31872  poimirlem28  31875  ovoliunnfl  31889  voliunnfl  31891  volsupnfl  31892  itg2addnclem  31900  itg2addnc  31903  iblabsnc  31913  iblmulc2nc  31914  sdclem2  31978  blbnd  32026  tendo0co2  34267  dvhfvadd  34571  dvh4dimN  34927  mzpcompact2lem  35505  diophrw  35513  eldioph2  35516  pellexlem5  35590  pell1qr1  35630  rmxy0  35684  cncfuni  37647  cncfiooicclem1  37654  fourierdlem38  37891  fourierdlem60  37913  fourierdlem61  37914  fourierdlem79  37932  fourierdlem112  37965  fourierswlem  37977  fouriersw  37978  cshword2  38791  resresdm  38817  cusgredg  39230  cusgrsizeindb0  39248  uhgrepe  39291  usgfis  39359  usgfisALT  39363  nn0sumshdiglem1  40035