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

Theorem syl5reqr 2669
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 2629 . 2 𝐴 = 𝐵
3 syl5reqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5req 2667 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613
This theorem is referenced by:  resdmdfsn  5433  f0dom0  6076  f1o00  6158  fmpt  6367  fmptsn  6418  fninfp  6425  bm2.5ii  6991  frnsuppeq  7292  mapsn  7884  sbthlem4  8058  sbthlem6  8060  findcard2s  8186  elfiun  8321  cnfcom2  8584  rankxplim3  8729  rankxpsuc  8730  pm54.43  8811  axdc3lem4  9260  gruun  9613  recmulnq  9771  reclem3pr  9856  xrmineq  11996  xadddi2  12112  iooval2  12193  hashsng  13142  hashfun  13207  hashbc  13220  isumclim3  14471  isummulc2  14474  iprodclim3  14712  bpolydiflem  14766  bpoly4  14771  fprodefsum  14806  ruclem4  14944  bitsshft  15178  phimullem  15465  pythagtriplem1  15502  1arithlem4  15611  fsets  15872  topnid  16077  pgrpsubgsymg  17809  odhash  17970  gsumzf1o  18294  gsumdifsnd  18341  pgpfaclem1  18461  mplcoe1  19446  mplcoe5  19449  evlslem4  19489  ordtrest2  20989  ufildr  21716  tsmsres  21928  zlmclm  22893  cphipval2  23021  rrxcph  23161  volinun  23295  uniioombllem4  23335  itg1climres  23462  limcco  23638  vieta1lem2  24047  coseq00topi  24235  tangtx  24238  coskpi  24253  advlog  24381  advlogexp  24382  logtayl  24387  logccv  24390  dvcxp1  24462  dvcncxp1  24465  loglesqrt  24480  ang180lem3  24522  dquart  24561  atans2  24639  basellem8  24795  chtub  24918  bposlem6  24995  lgsquadlem2  25087  logdivsum  25203  log2sumbnd  25214  spthispth  26603  ipval3  27534  siii  27678  cm2j  28449  pjssmii  28510  opsqrlem1  28969  hmopidmchi  28980  hmopidmpji  28981  pjcmul1i  29030  mddmd2  29138  cvexchlem  29197  dmdbr6ati  29252  difeq  29327  difuncomp  29341  ffsrn  29478  ordtprsuni  29939  ordtrest2NEW  29943  zzsnm  29979  measun  30248  sxbrsigalem2  30322  carsgsigalem  30351  eulerpartlemgu  30413  gsumnunsn  30589  signsplypnf  30601  logdivsqrle  30702  cvmlift2lem12  31270  nepss  31574  nodenselem5  31812  fwddifnp1  32247  finxpreclem1  33197  finxpreclem3  33201  poimirlem31  33411  ismblfin  33421  dvtan  33431  itg2addnclem3  33434  dvasin  33467  dvacos  33468  dvreasin  33469  dvreacos  33470  areacirclem1  33471  glbconN  34482  pmodl42N  34956  2polssN  35020  cdleme20j  35425  trlcocnv  35827  trlcone  35835  lclkrlem2c  36617  diophrw  37141  wopprc  37416  fsovcnvlem  38127  sineq0ALT  38993  mapsnd  39204  iccdifioo  39544  itgvol0  39947  fourierdlem33  40120  etransclem32  40246  zlmodzxzadd  41901  gsumdifsndf  41909
  Copyright terms: Public domain W3C validator