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

Theorem syl5eqr 2668
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5eqr.1 𝐵 = 𝐴
syl5eqr.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
syl5eqr (𝜑𝐴 = 𝐶)

Proof of Theorem syl5eqr
StepHypRef Expression
1 syl5eqr.1 . . 3 𝐵 = 𝐴
21eqcomi 2629 . 2 𝐴 = 𝐵
3 syl5eqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5eq 2666 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:  3eqtr3g  2677  csbeq1a  3535  ssdifeq0  4042  pofun  5041  opabbi2dv  5260  funcnvpr  5938  funcnvtp  5939  funcnvqp  5940  funcnvqpOLD  5941  fresin  6060  fresaunres2  6063  f1imacnv  6140  foimacnv  6141  funfv  6252  dffv2  6258  fimacnvinrn  6334  fsn2  6388  funiunfvf  6492  fcof1oinvd  6533  riotaxfrd  6627  f1opw2  6873  fnexALT  7117  fparlem3  7264  fparlem4  7265  mpt2curryd  7380  seqomlem1  7530  seqomlem4  7533  oasuc  7589  oesuclem  7590  omsuc  7591  onasuc  7593  onmsuc  7594  eqerlem  7761  pmresg  7870  fopwdom  8053  sbthlem8  8062  sbthlem9  8063  fodomr  8096  domss2  8104  mapen  8109  enp1i  8180  xpfi  8216  fiint  8222  f1opwfi  8255  mapfien  8298  marypha1lem  8324  unxpwdom  8479  cantnfval2  8551  infxpenlem  8821  cdainf  8999  isf34lem3  9182  isf34lem5  9185  axdc4lem  9262  ttukeylem6  9321  rankcf  9584  tskuni  9590  gruima  9609  dmrecnq  9775  ltexnq  9782  reclem3pr  9856  pn0sr  9907  mulgt0sr  9911  recdiv  10716  2resupmax  12004  max0sub  12012  rexmul  12086  xmulmnf1  12091  xmulm1  12096  prunioo  12286  fseq1p1m1  12398  fzshftral  12412  seqp1i  12800  seqf1olem2  12824  seqfeq4  12833  binom3  12968  expmulnbnd  12979  discr  12984  bcn2  13089  hashun2  13155  hashun3  13156  hashdif  13184  hashgt12el  13193  hashgt12el2  13194  hashfacen  13221  wrdeqs1cat  13456  swrdccat3a  13475  s2prop  13633  s4prop  13636  s3sndisj  13687  s3iunsndisj  13688  cnrecnv  13886  rddif  14061  amgm2  14090  rlimres  14270  lo1res  14271  iseraltlem2  14394  iseralt  14396  fsumss  14437  fsumcl2lem  14443  isumclim3  14471  fsumcnv  14485  telfsumo  14515  fsumiun  14534  arisum2  14574  geoisum1c  14592  fprodss  14659  fprodser  14660  fprodcl2lem  14661  fprodsplit  14677  fprodn0  14690  fprodcnv  14694  iprodclim3  14712  risefac1  14745  fallfac1  14746  bpolyval  14761  bpoly3  14770  bpoly4  14771  fsumcube  14772  sinhval  14865  cos01bnd  14897  ruclem6  14945  sqrt2irrlemOLD  14959  sadadd2lem2  15153  eucalgval  15276  pcid  15558  prmreclem4  15604  4sqlem15  15644  4sqlem16  15645  ramcl  15714  strfv2d  15886  setsid  15895  imasvscafn  16178  xpsc0  16201  xpsc1  16202  xpsff1o  16209  xpsaddlem  16216  xpsvsca  16220  xpsle  16222  mreexexlem2d  16286  mreexexlem4d  16288  sscres  16464  xpcid  16810  evlfcllem  16842  hofcl  16880  isacs5lem  17150  frmdup3lem  17384  cayleylem2  17814  f1omvdco2  17849  symggen  17871  psgnunilem1  17894  pgp0  17992  sylow3lem2  18024  lsmdisjr  18078  lsmdisj2r  18079  subgdisj2  18086  efgval  18111  frgpuplem  18166  frgpup2  18170  gsumval3  18289  gsumzres  18291  gsum2d2lem  18353  dprdf1  18413  dmdprdsplit2lem  18425  dmdprdsplit2  18426  ablfaclem3  18467  prdsmgp  18591  unitgrp  18648  crng2idl  19220  psrass1lem  19358  evl1var  19681  pf1mpf  19697  pf1ind  19700  gsumfsum  19794  chrid  19856  znleval  19884  ocv1  20004  frlmip  20098  ellspd  20122  mamuvs2  20193  madurid  20431  baspartn  20739  mretopd  20877  ordtcld1  20982  ordtcld2  20983  leordtvallem1  20995  leordtvallem2  20996  paste  21079  imacmp  21181  cmpsub  21184  unconn  21213  1stckgen  21338  ptbasfi  21365  txcld  21387  ptclsg  21399  txdis1cn  21419  ptrescn  21423  hausdiag  21429  txkgen  21436  xkoptsub  21438  xkococnlem  21443  cnmpt21  21455  cnmpt22  21458  tgqtop  21496  qtoprest  21501  kqdisj  21516  hmeores  21555  hmphindis  21581  pt1hmeo  21590  ptuncnv  21591  ptunhmeo  21592  xpstopnlem1  21593  xkohmeo  21599  alexsublem  21829  ptcmplem2  21838  tmdcn2  21874  cldsubg  21895  qustgplem  21905  tsmsres  21928  ustbas2  22010  ressuss  22048  metreslem  22148  xpsdsval  22167  prdsxmslem2  22315  txmetcnp  22333  tngngp  22439  nrmtngdist  22442  remetdval  22573  cnheibor  22735  evth2  22740  pcoass  22805  ncvspi  22937  iscmet3  23072  rrxip  23159  minveclem2  23178  cmmbl  23283  nulmbl2  23285  volinun  23295  voliunlem1  23299  volsup  23305  ovolioo  23317  uniiccdif  23327  uniioombllem2  23332  uniioombllem3  23334  uniioombllem4  23335  uniioombllem5  23336  ismbf3d  23402  itg2uba  23491  itg2i1fseq  23503  itgsplitioo  23585  limcflf  23626  cnplimc  23632  limcun  23640  dvfval  23642  dvres  23656  dvres3a  23659  dvnp1  23669  dvn1  23670  dvexp3  23722  dvsincos  23725  mvth  23736  c1lip2  23742  dvfsumlem2  23771  itgsubstlem  23792  itgsubst  23793  coeeq2  23979  dgreq0  24002  dgrcolem2  24011  vieta1  24048  ulm2  24120  radcnv0  24151  abelthlem2  24167  tanarg  24346  advlogexp  24382  efopn  24385  logtayl  24387  cxpcn3  24470  ang180lem3  24522  quad2  24547  mcubic  24555  binom4  24558  dquart  24561  quart1lem  24563  quart1  24564  quartlem1  24565  asinlem3a  24578  efiatan  24620  tanatan  24627  atanbndlem  24633  dvatan  24643  ftalem3  24782  ftalem5  24784  basellem3  24790  mumullem2  24887  musum  24898  chtublem  24917  perfectlem2  24936  bposlem6  24995  bposlem9  24998  1lgs  25046  lgs1  25047  lgseisenlem1  25081  lgseisenlem2  25082  lgseisenlem3  25083  lgsquadlem2  25087  lgsquad2lem2  25091  2sqblem  25137  rpvmasum2  25182  log2sumbnd  25214  opphllem3  25622  vtxdun  26358  wspn0  26801  eucrct2eupth  27085  numclwwlkovf2num  27190  nvpi  27492  nvop  27501  phop  27643  minvecolem2  27701  hi01  27923  pjchi  28261  chjidm  28349  mayete3i  28557  ho0val  28579  lnop0  28795  adjbdlnb  28913  pjin2i  29022  mdslmd3i  29161  mdexchi  29164  imadifxp  29386  fcoinver  29390  padct  29471  fcobijfs  29475  ffsrn  29478  iocinif  29517  difioo  29518  gsummpt2co  29754  ofldchr  29788  symgfcoeu  29819  pmtrprfv2  29822  smatlem  29837  fvproj  29873  indf1ofs  30062  esumpad2  30092  hasheuni  30121  esumcvg2  30123  esum2dlem  30128  sigapildsys  30199  measxun2  30247  measunl  30253  measinblem  30257  carsgclctunlem1  30353  carsgclctunlem3  30356  sibfof  30376  sitgclg  30378  eulerpartlemgf  30415  probdif  30456  cndprobval  30469  ballotlemic  30542  signsvtn0  30621  signstres  30626  chtvalz  30681  hgt750lemd  30700  bnj1415  31080  subfacp1lem1  31135  subfacp1lem3  31138  subfacp1lem5  31140  cvmscld  31229  cvmlift2lem9a  31259  cvmlift2lem9  31267  noetalem3  31839  fwddifnp1  32247  csbpredg  33143  finxpreclem5  33203  ptrest  33379  poimirlem2  33382  poimirlem3  33383  poimirlem6  33386  poimirlem7  33387  poimirlem9  33389  poimirlem11  33391  poimirlem12  33392  poimirlem16  33396  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  poimirlem24  33404  poimirlem25  33405  poimirlem27  33407  poimirlem28  33408  poimirlem29  33409  poimirlem31  33411  voliunnfl  33424  volsupnfl  33425  mbfresfi  33427  itg2addnclem2  33433  itg2addnclem3  33434  ftc1anclem5  33460  dvacos  33468  areacirclem5  33475  cocnv  33491  istotbnd3  33541  ssbnd  33558  fsumshftdOLD  34057  osumcllem9N  35069  4atexlemex2  35176  cdleme20j  35425  cdlemg47  35843  diaintclN  36166  dibintclN  36275  dihintcl  36452  lclkrlem2e  36619  lclkrlem2p  36630  lcfrlem31  36681  diophin  37155  monotuz  37325  monotoddzzfi  37326  oddcomabszz  37328  fnwe2val  37438  lnmlmic  37477  fiuneneq  37594  cytpval  37606  ntrkbimka  38156  ntrneifv2  38198  radcnvrat  38333  nzprmdif  38338  binomcxplemnotnn0  38375  ioccncflimc  39861  icocncflimc  39865  stoweidlem50  40030  fourierdlem89  40175  fourierdlem90  40176  fourierdlem91  40177  fourierdlem107  40193  perfectALTVlem2  41396  elsprel  41490  logb2aval  42270  aacllem  42312
  Copyright terms: Public domain W3C validator