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

Theorem syl5reqr 2876
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 2835 . 2 𝐴 = 𝐵
3 syl5reqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5req 2874 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819
This theorem is referenced by:  resdmdfsn  5900  f0dom0  6560  f1o00  6646  fmpt  6870  fmptsn  6925  fninfp  6932  uniordint  7509  frnsuppeq  7833  mapsnd  8439  sbthlem4  8619  sbthlem6  8621  findcard2s  8748  elfiun  8883  cnfcom2  9154  rankxplim3  9299  rankxpsuc  9300  pm54.43  9418  axdc3lem4  9864  gruun  10217  recmulnq  10375  reclem3pr  10460  xrmineq  12563  xadddi2  12680  iooval2  12761  hashsng  13720  hashfun  13788  hashbc  13801  swrds2m  14293  isumclim3  15104  isummulc2  15107  iprodclim3  15344  bpolydiflem  15398  bpoly4  15403  fprodefsum  15438  ruclem4  15577  bitsshft  15814  phimullem  16106  pythagtriplem1  16143  1arithlem4  16252  fsets  16506  topnid  16699  pgrpsubgsymg  18456  odhash  18619  gsumzf1o  18952  gsumdifsnd  19001  pgpfaclem1  19123  fincygsubgodd  19154  subdrgint  19502  mplcoe1  20164  mplcoe5  20167  evlslem4  20206  ordtrest2  21728  ufildr  22455  tsmsres  22667  zlmclm  23631  cphipval2  23759  csschl  23894  rrxcph  23910  volinun  24062  uniioombllem4  24102  itg1climres  24230  limcco  24406  vieta1lem2  24815  coseq00topi  25003  tangtx  25006  coskpi  25023  advlog  25150  advlogexp  25151  logtayl  25156  logccv  25159  dvcxp1  25234  dvcncxp1  25237  loglesqrt  25252  ang180lem3  25302  dquart  25344  atans2  25422  basellem8  25579  chtub  25702  bposlem6  25779  lgsquadlem2  25871  logdivsum  26023  log2sumbnd  26034  spthispth  27421  ipval3  28400  siii  28544  cm2j  29311  pjssmii  29372  opsqrlem1  29831  hmopidmchi  29842  hmopidmpji  29843  pjcmul1i  29892  mddmd2  30000  cvexchlem  30059  dmdbr6ati  30114  difeq  30194  difuncomp  30219  ffsrn  30378  symgcom2  30642  cycpmcl  30672  cycpm2tr  30675  qusdimsum  30910  ordtprsuni  31048  ordtrest2NEW  31052  zzsnm  31088  measun  31356  sxbrsigalem2  31430  carsgsigalem  31459  eulerpartlemgu  31521  gsumnunsn  31697  signsplypnf  31706  logdivsqrle  31807  cvmlift2lem12  32445  satf0suc  32507  nepss  32832  nodenselem5  33076  fwddifnp1  33510  finxpreclem1  34539  finxpreclem3  34543  poimirlem31  34790  ismblfin  34800  dvtan  34809  itg2addnclem3  34812  dvasin  34845  dvacos  34846  dvreasin  34847  dvreacos  34848  areacirclem1  34849  cnvepima  35462  glbconN  36380  pmodl42N  36854  2polssN  36918  cdleme20j  37321  trlcocnv  37723  trlcone  37731  lclkrlem2c  38512  diophrw  39221  wopprc  39492  fsovcnvlem  40224  sineq0ALT  41136  founiiun0  41316  iccdifioo  41656  itgvol0  42118  fourierdlem33  42291  etransclem32  42417  simpcntrab  42993  gsumdifsndf  43920  zlmodzxzadd  44238
  Copyright terms: Public domain W3C validator