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

Theorem syl5reqr 2700
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 2660 . 2 𝐴 = 𝐵
3 syl5reqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5req 2698 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:  resdmdfsn  5480  f0dom0  6127  f1o00  6209  fmpt  6421  fmptsn  6474  fninfp  6481  bm2.5ii  7048  frnsuppeq  7352  mapsn  7941  sbthlem4  8114  sbthlem6  8116  findcard2s  8242  elfiun  8377  cnfcom2  8637  rankxplim3  8782  rankxpsuc  8783  pm54.43  8864  axdc3lem4  9313  gruun  9666  recmulnq  9824  reclem3pr  9909  xrmineq  12049  xadddi2  12165  iooval2  12246  hashsng  13197  hashfun  13262  hashbc  13275  isumclim3  14534  isummulc2  14537  iprodclim3  14775  bpolydiflem  14829  bpoly4  14834  fprodefsum  14869  ruclem4  15007  bitsshft  15244  phimullem  15531  pythagtriplem1  15568  1arithlem4  15677  fsets  15938  topnid  16143  pgrpsubgsymg  17874  odhash  18035  gsumzf1o  18359  gsumdifsnd  18406  pgpfaclem1  18526  mplcoe1  19513  mplcoe5  19516  evlslem4  19556  ordtrest2  21056  ufildr  21782  tsmsres  21994  zlmclm  22958  cphipval2  23086  rrxcph  23226  volinun  23360  uniioombllem4  23400  itg1climres  23526  limcco  23702  vieta1lem2  24111  coseq00topi  24299  tangtx  24302  coskpi  24317  advlog  24445  advlogexp  24446  logtayl  24451  logccv  24454  dvcxp1  24526  dvcncxp1  24529  loglesqrt  24544  ang180lem3  24586  dquart  24625  atans2  24703  basellem8  24859  chtub  24982  bposlem6  25059  lgsquadlem2  25151  logdivsum  25267  log2sumbnd  25278  spthispth  26678  2clwwlk2clwwlklem2lem2  27329  ipval3  27692  siii  27836  cm2j  28607  pjssmii  28668  opsqrlem1  29127  hmopidmchi  29138  hmopidmpji  29139  pjcmul1i  29188  mddmd2  29296  cvexchlem  29355  dmdbr6ati  29410  difeq  29481  difuncomp  29495  ffsrn  29632  ordtprsuni  30093  ordtrest2NEW  30097  zzsnm  30133  measun  30402  sxbrsigalem2  30476  carsgsigalem  30505  eulerpartlemgu  30567  gsumnunsn  30743  signsplypnf  30755  logdivsqrle  30856  cvmlift2lem12  31422  nepss  31725  nodenselem5  31963  fwddifnp1  32397  finxpreclem1  33356  finxpreclem3  33360  poimirlem31  33570  ismblfin  33580  dvtan  33590  itg2addnclem3  33593  dvasin  33626  dvacos  33627  dvreasin  33628  dvreacos  33629  areacirclem1  33630  glbconN  34981  pmodl42N  35455  2polssN  35519  cdleme20j  35923  trlcocnv  36325  trlcone  36333  lclkrlem2c  37115  diophrw  37639  wopprc  37914  fsovcnvlem  38624  sineq0ALT  39487  mapsnd  39702  iccdifioo  40059  itgvol0  40502  fourierdlem33  40675  etransclem32  40801  zlmodzxzadd  42461  gsumdifsndf  42469
  Copyright terms: Public domain W3C validator