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

Theorem syl5eqr 2658
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 2619 . 2 𝐴 = 𝐵
3 syl5eqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5eq 2656 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-cleq 2603
This theorem is referenced by:  3eqtr3g  2667  csbeq1a  3508  ssdifeq0  4003  pofun  4975  opabbi2dv  5193  funcnvpr  5864  funcnvtp  5865  funcnvqp  5866  funcnvqpOLD  5867  fresin  5986  fresaunres2  5989  f1imacnv  6066  foimacnv  6067  funfv  6175  dffv2  6181  fimacnvinrn  6256  fsn2  6309  funiunfvf  6411  fcof1oinvd  6448  riotaxfrd  6541  f1opw2  6786  fnexALT  7025  fparlem3  7166  fparlem4  7167  mpt2curryd  7282  seqomlem1  7432  seqomlem4  7435  oasuc  7491  oesuclem  7492  omsuc  7493  onasuc  7495  onmsuc  7496  eqerlem  7663  pmresg  7771  fopwdom  7953  sbthlem8  7962  sbthlem9  7963  fodomr  7996  domss2  8004  mapen  8009  enp1i  8080  xpfi  8116  fiint  8122  f1opwfi  8153  mapfien  8196  marypha1lem  8222  unxpwdom  8377  cantnfval2  8449  infxpenlem  8719  cdainf  8897  isf34lem3  9080  isf34lem5  9083  axdc4lem  9160  ttukeylem6  9219  rankcf  9478  tskuni  9484  gruima  9503  dmrecnq  9669  ltexnq  9676  reclem3pr  9750  pn0sr  9801  mulgt0sr  9805  recdiv  10610  2resupmax  11893  max0sub  11901  rexmul  11973  xmulmnf1  11978  xmulm1  11983  prunioo  12172  fseq1p1m1  12283  fzshftral  12297  seqp1i  12679  seqf1olem2  12703  seqfeq4  12712  binom3  12847  expmulnbnd  12858  discr  12863  bcn2  12968  hashun2  13033  hashun3  13034  hashdif  13062  hashgt12el  13070  hashgt12el2  13071  hashfacen  13095  wrdeqs1cat  13326  swrdccat3a  13345  s2prop  13502  s4prop  13505  s3sndisj  13554  s3iunsndisj  13555  cnrecnv  13753  rddif  13928  amgm2  13957  rlimres  14137  lo1res  14138  iseraltlem2  14261  iseralt  14263  fsumss  14303  fsumcl2lem  14309  isumclim3  14332  fsumcnv  14346  telfsumo  14375  fsumiun  14394  arisum2  14432  geoisum1c  14450  fprodss  14517  fprodser  14518  fprodcl2lem  14519  fprodsplit  14535  fprodn0  14548  fprodcnv  14552  iprodclim3  14570  risefac1  14603  fallfac1  14604  bpolyval  14619  bpoly3  14628  bpoly4  14629  fsumcube  14630  sinhval  14723  cos01bnd  14755  ruclem6  14803  sqr2irrlem  14816  sadadd2lem2  15010  eucalgval  15133  pcid  15415  prmreclem4  15461  4sqlem15  15501  4sqlem16  15502  ramcl  15571  strfv2d  15733  setsid  15742  imasvscafn  16020  xpsc0  16043  xpsc1  16044  xpsff1o  16051  xpsaddlem  16058  xpsvsca  16062  xpsle  16064  mreexexlem2d  16128  mreexexlem4d  16130  sscres  16306  xpcid  16652  evlfcllem  16684  hofcl  16722  isacs5lem  16992  frmdup3lem  17226  cayleylem2  17656  f1omvdco2  17691  symggen  17713  psgnunilem1  17736  pgp0  17834  sylow3lem2  17866  lsmdisjr  17920  lsmdisj2r  17921  subgdisj2  17928  efgval  17953  frgpuplem  18008  frgpup2  18012  gsumval3  18131  gsumzres  18133  gsum2d2lem  18195  dprdf1  18255  dmdprdsplit2lem  18267  dmdprdsplit2  18268  ablfaclem3  18309  prdsmgp  18433  unitgrp  18490  crng2idl  19060  psrass1lem  19198  evl1var  19521  pf1mpf  19537  pf1ind  19540  gsumfsum  19632  chrid  19694  znleval  19722  ocv1  19842  frlmip  19936  ellspd  19960  mamuvs2  20031  madurid  20269  baspartn  20569  mretopd  20706  ordtcld1  20811  ordtcld2  20812  leordtvallem1  20824  leordtvallem2  20825  paste  20908  imacmp  21010  cmpsub  21013  uncon  21042  1stckgen  21167  ptbasfi  21194  txcld  21216  ptclsg  21228  txdis1cn  21248  ptrescn  21252  hausdiag  21258  txkgen  21265  xkoptsub  21267  xkococnlem  21272  cnmpt21  21284  cnmpt22  21287  tgqtop  21325  qtoprest  21330  kqdisj  21345  hmeores  21384  hmphindis  21410  pt1hmeo  21419  ptuncnv  21420  ptunhmeo  21421  xpstopnlem1  21422  xkohmeo  21428  alexsublem  21658  ptcmplem2  21667  tmdcn2  21703  cldsubg  21724  qustgplem  21734  tsmsres  21757  ustbas2  21839  ressuss  21877  metreslem  21977  xpsdsval  21996  prdsxmslem2  22144  txmetcnp  22162  tngngp  22268  nrmtngdist  22271  remetdval  22400  cnheibor  22562  evth2  22567  pcoass  22632  ncvspi  22764  iscmet3  22899  rrxip  22986  minveclem2  23005  cmmbl  23109  nulmbl2  23111  volinun  23121  voliunlem1  23125  volsup  23131  ovolioo  23143  uniiccdif  23152  uniioombllem2  23157  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  ismbf3d  23227  itg2uba  23316  itg2i1fseq  23328  itgsplitioo  23410  limcflf  23451  cnplimc  23457  limcun  23465  dvfval  23467  dvres  23481  dvres3a  23484  dvnp1  23494  dvn1  23495  dvexp3  23545  dvsincos  23548  mvth  23559  c1lip2  23565  dvfsumlem2  23594  itgsubstlem  23615  itgsubst  23616  coeeq2  23802  dgreq0  23825  dgrcolem2  23834  vieta1  23871  ulm2  23943  radcnv0  23974  abelthlem2  23990  tanarg  24169  advlogexp  24201  efopn  24204  logtayl  24206  cxpcn3  24289  ang180lem3  24341  quad2  24366  mcubic  24374  binom4  24377  dquart  24380  quart1lem  24382  quart1  24383  quartlem1  24384  asinlem3a  24397  efiatan  24439  tanatan  24446  atanbndlem  24452  dvatan  24462  ftalem3  24601  ftalem5  24603  basellem3  24609  mumullem2  24706  musum  24717  chtublem  24736  perfectlem2  24755  bposlem6  24814  bposlem9  24817  1lgs  24865  lgs1  24866  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgsquadlem2  24906  lgsquad2lem2  24910  2sqblem  24956  rpvmasum2  25001  log2sumbnd  25033  opphllem3  25441  vdgrun  26428  vdgrfiun  26429  numclwwlkovf2num  26612  nvpi  26906  nvop  26915  phop  27057  minvecolem2  27115  hi01  27337  pjchi  27675  chjidm  27763  mayete3i  27971  ho0val  27993  lnop0  28209  adjbdlnb  28327  pjin2i  28436  mdslmd3i  28575  mdexchi  28578  imadifxp  28796  fcoinver  28798  padct  28885  fcobijfs  28889  ffsrn  28892  iocinif  28933  difioo  28934  gsummpt2co  29111  ofldchr  29145  symgfcoeu  29176  pmtrprfv2  29179  smatlem  29191  fvproj  29227  indf1ofs  29415  esumpad2  29445  hasheuni  29474  esumcvg2  29476  esum2dlem  29481  sigapildsys  29552  measxun2  29600  measunl  29606  measinblem  29610  carsgclctunlem1  29706  carsgclctunlem3  29709  sibfof  29729  sitgclg  29731  eulerpartlemgf  29768  probdif  29809  cndprobval  29822  ballotlemic  29895  signsvtn0  29973  signstres  29978  bnj1415  30360  subfacp1lem1  30415  subfacp1lem3  30418  subfacp1lem5  30420  cvmscld  30509  cvmlift2lem9a  30539  cvmlift2lem9  30547  nofulllem5  31105  fwddifnp1  31442  csbpredg  32348  finxpreclem5  32408  ptrest  32578  poimirlem2  32581  poimirlem3  32582  poimirlem6  32585  poimirlem7  32586  poimirlem9  32588  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem24  32603  poimirlem25  32604  poimirlem27  32606  poimirlem28  32607  poimirlem29  32608  poimirlem31  32610  voliunnfl  32623  volsupnfl  32624  mbfresfi  32626  itg2addnclem2  32632  itg2addnclem3  32633  ftc1anclem5  32659  dvacos  32667  areacirclem5  32674  cocnv  32690  istotbnd3  32740  ssbnd  32757  fsumshftdOLD  33256  osumcllem9N  34268  4atexlemex2  34375  cdleme20j  34624  cdlemg47  35042  diaintclN  35365  dibintclN  35474  dihintcl  35651  lclkrlem2e  35818  lclkrlem2p  35829  lcfrlem31  35880  diophin  36354  monotuz  36524  monotoddzzfi  36525  oddcomabszz  36527  fnwe2val  36637  lnmlmic  36676  fiuneneq  36794  cytpval  36806  ntrkbimka  37356  ntrneifv2  37398  radcnvrat  37535  nzprmdif  37540  binomcxplemnotnn0  37577  ioccncflimc  38771  icocncflimc  38775  stoweidlem50  38943  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem107  39106  perfectALTVlem2  40165  vtxdun  40696  wspn0  41131  eucrct2eupth  41413  frgrwopreglem2  41482  av-numclwwlkovf2num  41516  logb2aval  42314  aacllem  42356
  Copyright terms: Public domain W3C validator