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

Theorem syl5reqr 2820
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl5reqr.1 𝐵 = 𝐴
syl5reqr.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
syl5reqr (𝜑𝐶 = 𝐴)

Proof of Theorem syl5reqr
StepHypRef Expression
1 syl5reqr.1 . . 3 𝐵 = 𝐴
21eqcomi 2780 . 2 𝐴 = 𝐵
3 syl5reqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5req 2818 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764
This theorem is referenced by:  resdmdfsn  5586  f0dom0  6229  f1o00  6312  fmpt  6523  fmptsn  6577  fninfp  6584  bm2.5ii  7153  frnsuppeq  7458  mapsnd  8051  sbthlem4  8229  sbthlem6  8231  findcard2s  8357  elfiun  8492  cnfcom2  8763  rankxplim3  8908  rankxpsuc  8909  pm54.43  9026  axdc3lem4  9477  gruun  9830  recmulnq  9988  reclem3pr  10073  xrmineq  12216  xadddi2  12332  iooval2  12413  hashsng  13361  hashfun  13426  hashbc  13439  swrds2m  13895  isumclim3  14698  isummulc2  14701  iprodclim3  14937  bpolydiflem  14991  bpoly4  14996  fprodefsum  15031  ruclem4  15169  bitsshft  15405  phimullem  15691  pythagtriplem1  15728  1arithlem4  15837  fsets  16098  topnid  16304  pgrpsubgsymg  18035  odhash  18196  gsumzf1o  18520  gsumdifsnd  18567  pgpfaclem1  18688  mplcoe1  19680  mplcoe5  19683  evlslem4  19723  ordtrest2  21229  ufildr  21955  tsmsres  22167  zlmclm  23131  cphipval2  23259  rrxcph  23399  volinun  23534  uniioombllem4  23574  itg1climres  23701  limcco  23877  vieta1lem2  24286  coseq00topi  24475  tangtx  24478  coskpi  24493  advlog  24621  advlogexp  24622  logtayl  24627  logccv  24630  dvcxp1  24702  dvcncxp1  24705  loglesqrt  24720  ang180lem3  24762  dquart  24801  atans2  24879  basellem8  25035  chtub  25158  bposlem6  25235  lgsquadlem2  25327  logdivsum  25443  log2sumbnd  25454  spthispth  26857  ipval3  27904  siii  28048  cm2j  28819  pjssmii  28880  opsqrlem1  29339  hmopidmchi  29350  hmopidmpji  29351  pjcmul1i  29400  mddmd2  29508  cvexchlem  29567  dmdbr6ati  29622  difeq  29693  difuncomp  29707  ffsrn  29844  ordtprsuni  30305  ordtrest2NEW  30309  zzsnm  30345  measun  30614  sxbrsigalem2  30688  carsgsigalem  30717  eulerpartlemgu  30779  gsumnunsn  30955  signsplypnf  30967  logdivsqrle  31068  cvmlift2lem12  31634  nepss  31937  nodenselem5  32175  fwddifnp1  32609  finxpreclem1  33563  finxpreclem3  33567  poimirlem31  33773  ismblfin  33783  dvtan  33792  itg2addnclem3  33795  dvasin  33828  dvacos  33829  dvreasin  33830  dvreacos  33831  areacirclem1  33832  glbconN  35185  pmodl42N  35659  2polssN  35723  cdleme20j  36127  trlcocnv  36529  trlcone  36537  lclkrlem2c  37319  diophrw  37848  wopprc  38123  fsovcnvlem  38833  sineq0ALT  39695  iccdifioo  40260  itgvol0  40701  fourierdlem33  40874  etransclem32  41000  zlmodzxzadd  42664  gsumdifsndf  42672
  Copyright terms: Public domain W3C validator