MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6req Structured version   Visualization version   GIF version

Theorem syl6req 2876
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
StepHypRef Expression
1 syl6req.1 . . 3 (𝜑𝐴 = 𝐵)
2 syl6req.2 . . 3 𝐵 = 𝐶
31, 2syl6eq 2875 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2830 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817
This theorem is referenced by:  syl6reqr  2878  csbin  4374  csbif  4505  csbuni  4854  csbima12  5935  somincom  5982  resresdm  6078  csbfv12  6702  opabiotafun  6733  fvmptrabfv  6788  fndifnfp  6927  elxp4  7619  elxp5  7620  fo1stres  7707  fo2ndres  7708  eloprabi  7753  fo2ndf  7809  seqomlem2  8079  oev2  8140  odi  8197  fundmen  8575  xpsnen  8593  xpassen  8603  ac6sfi  8755  infeq5  9093  alephsuc3  9996  rankcf  10193  ine0  11069  nn0n0n1ge2  11957  fzval2  12895  fseq1p1m1  12983  fzosplitprm1  13149  hashfun  13801  hashf1  13818  hashtpg  13846  cshword  14151  wrd2pr2op  14303  wrd3tpop  14308  fsum2dlem  15123  fprod2dlem  15332  ef4p  15464  sin01bnd  15536  odd2np1  15688  bitsinvp1  15794  smumullem  15837  oppcmon  17006  issubc2  17104  curf1cl  17476  curfcl  17480  cnvtsr  17830  sylow1lem1  18721  sylow2a  18742  ablsimpgfindlem1  19227  coe1fzgsumdlem  20464  evl1gsumdlem  20514  pmatcollpw3lem  21386  pptbas  21611  2ndcctbss  22058  txcmplem1  22244  qtopeu  22319  alexsubALTlem3  22652  ustuqtop5  22849  psmetdmdm  22910  xmetdmdm  22940  pcopt  23625  pcorevlem  23629  voliunlem1  24152  i1fima2  24281  iblabs  24430  dveflem  24580  deg1val  24695  abssinper  25111  mulcxplem  25273  dvatan  25519  lgamgulmlem2  25613  lgamgulmlem5  25616  lgseisenlem1  25957  dchrisumlem1  26071  pntlemr  26184  krippenlem  26482  cusgredg  27212  cusgrsizeindb0  27237  numclwlk1lem1  28152  numclwwlk3lem2lem  28166  grporndm  28291  vafval  28384  smfval  28386  hvmul0  28805  cmcmlem  29372  cmbr3i  29381  nmbdfnlbi  29830  nmcfnlbi  29833  nmopcoadji  29882  pjin2i  29974  hst1h  30008  xaddeq0  30483  cycpmconjslem1  30823  archirngz  30845  esumcst  31349  eulerpartlems  31645  dstfrvunirn  31759  sgnmul  31827  subfacp1lem5  32458  cvmliftlem10  32568  fnessref  33732  fnemeet2  33742  poimirlem4  34973  poimirlem19  34988  poimirlem20  34989  poimirlem23  34992  poimirlem24  34993  poimirlem25  34994  poimirlem28  34997  ovoliunnfl  35011  voliunnfl  35013  volsupnfl  35014  itg2addnclem  35020  itg2addnc  35023  iblabsnc  35033  iblmulc2nc  35034  sdclem2  35092  blbnd  35137  ismgmOLD  35200  ismndo2  35224  rnresequniqs  35661  tendo0co2  37996  dvhfvadd  38299  dvh4dimN  38655  mzpcompact2lem  39548  diophrw  39556  eldioph2  39559  pellexlem5  39630  pell1qr1  39668  rmxy0  39720  wessf1ornlem  41676  cncfuni  42394  cncfiooicclem1  42401  fourierdlem38  42653  fourierdlem60  42674  fourierdlem61  42675  fourierdlem79  42693  fourierdlem112  42726  fourierswlem  42738  fouriersw  42739  fvmptrab  43714  fvmptrabdm  43715  fmtnofac2  43952  nn0sumshdiglem1  44900
  Copyright terms: Public domain W3C validator