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

Theorem syl6req 2702
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 2701 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2657 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  syl6reqr  2704  csbin  4043  csbif  4171  csbuni  4498  csbima12  5518  somincom  5565  resresdm  5664  csbfv12  6269  opabiotafun  6298  fvmptrabfv  6348  fndifnfp  6483  elxp4  7152  elxp5  7153  fo1stres  7236  fo2ndres  7237  eloprabi  7277  fo2ndf  7329  seqomlem2  7591  oev2  7648  odi  7704  fundmen  8071  xpsnen  8085  xpassen  8095  ac6sfi  8245  infeq5  8572  alephsuc3  9440  rankcf  9637  ine0  10503  nn0n0n1ge2  11396  fzval2  12367  fseq1p1m1  12452  fzosplitprm1  12618  hashfun  13262  hashf1  13279  hashtpg  13305  cshword  13583  wrd2pr2op  13733  wrd3tpop  13737  fsum2dlem  14545  fprod2dlem  14754  ef4p  14887  sin01bnd  14959  odd2np1  15112  bitsinvp1  15218  smumullem  15261  oppcmon  16445  issubc2  16543  curf1cl  16915  curfcl  16919  cnvtsr  17269  sylow1lem1  18059  sylow2a  18080  coe1fzgsumdlem  19719  evl1gsumdlem  19768  pmatcollpw3lem  20636  pptbas  20860  2ndcctbss  21306  txcmplem1  21492  qtopeu  21567  alexsubALTlem3  21900  ustuqtop5  22096  psmetdmdm  22157  xmetdmdm  22187  pcopt  22868  pcorevlem  22872  voliunlem1  23364  i1fima2  23491  iblabs  23640  dveflem  23787  deg1val  23901  abssinper  24315  mulcxplem  24475  dvatan  24707  lgamgulmlem2  24801  lgamgulmlem5  24804  lgseisenlem1  25145  dchrisumlem1  25223  pntlemr  25336  krippenlem  25630  cusgredg  26376  cusgrsizeindb0  26401  wlknwwlksnsur  26844  clwwlknonmpt2  27062  numclwwlk3lemlem  27370  grporndm  27492  vafval  27586  smfval  27588  hvmul0  28009  cmcmlem  28578  cmbr3i  28587  nmbdfnlbi  29036  nmcfnlbi  29039  nmopcoadji  29088  pjin2i  29180  hst1h  29214  xaddeq0  29646  archirngz  29871  esumcst  30253  eulerpartlems  30550  dstfrvunirn  30664  sgnmul  30732  subfacp1lem5  31292  cvmliftlem10  31402  fnessref  32477  fnemeet2  32487  poimirlem4  33543  poimirlem19  33558  poimirlem20  33559  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem28  33567  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  itg2addnclem  33591  itg2addnc  33594  iblabsnc  33604  iblmulc2nc  33605  sdclem2  33668  blbnd  33716  ismgmOLD  33779  ismndo2  33803  rnresequniqs  34243  tendo0co2  36393  dvhfvadd  36697  dvh4dimN  37053  mzpcompact2lem  37631  diophrw  37639  eldioph2  37642  pellexlem5  37714  pell1qr1  37752  rmxy0  37805  cncfuni  40417  cncfiooicclem1  40424  fourierdlem38  40680  fourierdlem60  40701  fourierdlem61  40702  fourierdlem79  40720  fourierdlem112  40753  fourierswlem  40765  fouriersw  40766  fvmptrab  41631  fvmptrabdm  41632  cshword2  41762  fmtnofac2  41806  nn0sumshdiglem1  42740
  Copyright terms: Public domain W3C validator