Theorem syl6req 2673

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 2672	. 2 |- ( ph -> A = C )
4	3	eqcomd 2628	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  syl6reqr  2675  csbin  4010  csbif  4138  csbuni  4466  csbima12  5483  somincom  5530  resresdm  5626  csbfv12  6231  opabiotafun  6259  fndifnfp  6442  elxp4  7110  elxp5  7111  fo1stres  7192  fo2ndres  7193  eloprabi  7232  fo2ndf  7284  seqomlem2  7546  oev2  7603  odi  7659  fundmen  8030  xpsnen  8044  xpassen  8054  ac6sfi  8204  infeq5  8534  alephsuc3  9402  rankcf  9599  ine0  10465  nn0n0n1ge2  11358  fzval2  12329  fseq1p1m1  12414  fzosplitprm1  12578  hashfun  13224  hashf1  13241  hashtpg  13267  cshword  13537  wrd2pr2op  13687  wrd3tpop  13691  fsum2dlem  14501  fprod2dlem  14710  ef4p  14843  sin01bnd  14915  odd2np1  15065  bitsinvp1  15171  smumullem  15214  oppcmon  16398  issubc2  16496  curf1cl  16868  curfcl  16872  cnvtsr  17222  sylow1lem1  18013  sylow2a  18034  coe1fzgsumdlem  19671  evl1gsumdlem  19720  pmatcollpw3lem  20588  pptbas  20812  2ndcctbss  21258  txcmplem1  21444  qtopeu  21519  alexsubALTlem3  21853  ustuqtop5  22049  psmetdmdm  22110  xmetdmdm  22140  pcopt  22822  pcorevlem  22826  voliunlem1  23318  i1fima2  23446  iblabs  23595  dveflem  23742  deg1val  23856  abssinper  24270  mulcxplem  24430  dvatan  24662  lgamgulmlem2  24756  lgamgulmlem5  24759  lgseisenlem1  25100  dchrisumlem1  25178  pntlemr  25291  krippenlem  25585  cusgredg  26320  cusgrsizeindb0  26345  wlknwwlksnsur  26776  grporndm  27364  vafval  27458  smfval  27460  hvmul0  27881  cmcmlem  28450  cmbr3i  28459  nmbdfnlbi  28908  nmcfnlbi  28911  nmopcoadji  28960  pjin2i  29052  hst1h  29086  xaddeq0  29518  archirngz  29743  esumcst  30125  eulerpartlems  30422  dstfrvunirn  30536  sgnmul  30604  subfacp1lem5  31166  cvmliftlem10  31276  fnessref  32352  fnemeet2  32362  poimirlem4  33413  poimirlem19  33428  poimirlem20  33429  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem28  33437  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  itg2addnclem  33461  itg2addnc  33464  iblabsnc  33474  iblmulc2nc  33475  sdclem2  33538  blbnd  33586  ismgmOLD  33649  ismndo2  33673  rnresequniqs  34102  tendo0co2  36076  dvhfvadd  36380  dvh4dimN  36736  mzpcompact2lem  37314  diophrw  37322  eldioph2  37325  pellexlem5  37397  pell1qr1  37435  rmxy0  37488  cncfuni  40099  cncfiooicclem1  40106  fourierdlem38  40362  fourierdlem60  40383  fourierdlem61  40384  fourierdlem79  40402  fourierdlem112  40435  fourierswlem  40447  fouriersw  40448  cshword2  41437  fmtnofac2  41481  nn0sumshdiglem1  42415