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

Theorem syl6req 2660
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 2659 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2615 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  syl6reqr  2662  csbin  3961  csbif  4087  csbuni  4396  csbima12  5389  somincom  5436  csbfv12  6126  opabiotafun  6154  fndifnfp  6325  elxp4  6980  elxp5  6981  fo1stres  7060  fo2ndres  7061  eloprabi  7098  fo2ndf  7148  seqomlem2  7410  oev2  7467  odi  7523  fundmen  7893  xpsnen  7906  xpassen  7916  ac6sfi  8066  infeq5  8394  alephsuc3  9258  rankcf  9455  ine0  10316  nn0n0n1ge2  11205  fzval2  12155  fseq1p1m1  12238  hashfun  13036  hashf1  13050  hashtpg  13071  cshword  13334  wrd2pr2op  13481  wrd3tpop  13485  fsum2dlem  14289  fprod2dlem  14495  ef4p  14628  sin01bnd  14700  odd2np1  14849  bitsinvp1  14955  smumullem  14998  oppcmon  16167  issubc2  16265  curf1cl  16637  curfcl  16641  cnvtsr  16991  sylow1lem1  17782  sylow2a  17803  coe1fzgsumdlem  19438  evl1gsumdlem  19487  pmatcollpw3lem  20349  pptbas  20564  2ndcctbss  21010  txcmplem1  21196  qtopeu  21271  alexsubALTlem3  21605  ustuqtop5  21801  psmetdmdm  21862  xmetdmdm  21891  pcopt  22561  pcorevlem  22565  voliunlem1  23042  i1fima2  23169  iblabs  23318  dveflem  23463  deg1val  23577  abssinper  23991  mulcxplem  24147  dvatan  24379  lgamgulmlem2  24473  lgamgulmlem5  24476  lgseisenlem1  24817  dchrisumlem1  24895  pntlemr  25008  krippenlem  25303  usgra2wlkspthlem1  25913  wlknwwlknsur  26006  grporndm  26514  vafval  26626  smfval  26628  hvmul0  27071  cmcmlem  27640  cmbr3i  27649  nmbdfnlbi  28098  nmcfnlbi  28101  nmopcoadji  28150  pjin2i  28242  hst1h  28276  xaddeq0  28713  archirngz  28880  esumcst  29258  eulerpartlems  29555  dstfrvunirn  29669  sgnmul  29737  subfacp1lem5  30226  cvmliftlem10  30336  fnessref  31328  fnemeet2  31338  poimirlem4  32379  poimirlem19  32394  poimirlem20  32395  poimirlem23  32398  poimirlem24  32399  poimirlem25  32400  poimirlem28  32403  ovoliunnfl  32417  voliunnfl  32419  volsupnfl  32420  itg2addnclem  32427  itg2addnc  32430  iblabsnc  32440  iblmulc2nc  32441  sdclem2  32504  blbnd  32552  ismgmOLD  32615  ismndo2  32639  tendo0co2  34890  dvhfvadd  35194  dvh4dimN  35550  mzpcompact2lem  36128  diophrw  36136  eldioph2  36139  pellexlem5  36211  pell1qr1  36249  rmxy0  36302  cncfuni  38569  cncfiooicclem1  38576  fourierdlem38  38835  fourierdlem60  38856  fourierdlem61  38857  fourierdlem79  38875  fourierdlem112  38908  fourierswlem  38920  fouriersw  38921  fmtnofac2  39817  cshword2  40098  resresdm  40127  cusgredg  40641  cusgrsizeindb0  40660  wlknwwlksnsur  41082  nn0sumshdiglem1  42208
  Copyright terms: Public domain W3C validator