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

Theorem syl5eqr 2699
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 2660 . 2 𝐴 = 𝐵
3 syl5eqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5eq 2697 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:  3eqtr3g  2708  csbeq1a  3575  ssdifeq0  4084  pofun  5080  opabbi2dv  5304  cnvsng  5652  funcnvpr  5988  funcnvtp  5989  funcnvqp  5990  funcnvqpOLD  5991  fresin  6111  fresaunres2  6114  f1imacnv  6191  foimacnv  6192  funfv  6304  dffv2  6310  fimacnvinrn  6388  fsn2  6443  funiunfvf  6547  fcof1oinvd  6588  riotaxfrd  6682  f1opw2  6930  fnexALT  7174  fparlem3  7324  fparlem4  7325  mpt2curryd  7440  seqomlem1  7590  seqomlem4  7593  oasuc  7649  oesuclem  7650  omsuc  7651  onasuc  7653  onmsuc  7654  eqerlem  7821  pmresg  7927  fopwdom  8109  sbthlem8  8118  sbthlem9  8119  fodomr  8152  domss2  8160  mapen  8165  enp1i  8236  xpfi  8272  fiint  8278  f1opwfi  8311  mapfien  8354  marypha1lem  8380  unxpwdom  8535  cantnfval2  8604  infxpenlem  8874  cdainf  9052  isf34lem3  9235  isf34lem5  9238  axdc4lem  9315  ttukeylem6  9374  rankcf  9637  tskuni  9643  gruima  9662  dmrecnq  9828  ltexnq  9835  reclem3pr  9909  pn0sr  9960  mulgt0sr  9964  recdiv  10769  2resupmax  12057  max0sub  12065  rexmul  12139  xmulmnf1  12144  xmulm1  12149  prunioo  12339  fseq1p1m1  12452  fzshftral  12466  seqp1i  12857  seqf1olem2  12881  seqfeq4  12890  binom3  13025  expmulnbnd  13036  discr  13041  bcn2  13146  hashun2  13210  hashun3  13211  hashdif  13239  hashgt12el  13248  hashgt12el2  13249  hashfacen  13276  wrdeqs1cat  13520  swrdccat3a  13540  s2prop  13698  s4prop  13701  s3sndisj  13752  s3iunsndisj  13753  cnrecnv  13949  rddif  14124  amgm2  14153  rlimres  14333  lo1res  14334  iseraltlem2  14457  iseralt  14459  fsumss  14500  fsumcl2lem  14506  isumclim3  14534  fsumcnv  14548  telfsumo  14578  fsumiun  14597  arisum2  14637  geoisum1c  14655  fprodss  14722  fprodser  14723  fprodcl2lem  14724  fprodsplit  14740  fprodn0  14753  fprodcnv  14757  iprodclim3  14775  risefac1  14808  fallfac1  14809  bpolyval  14824  bpoly3  14833  bpoly4  14834  fsumcube  14835  sinhval  14928  cos01bnd  14960  ruclem6  15008  sqrt2irrlemOLD  15022  sadadd2lem2  15219  eucalgval  15342  pcid  15624  prmreclem4  15670  4sqlem15  15710  4sqlem16  15711  ramcl  15780  strfv2d  15952  setsid  15961  imasvscafn  16244  xpsc0  16267  xpsc1  16268  xpsff1o  16275  xpsaddlem  16282  xpsvsca  16286  xpsle  16288  mreexexlem2d  16352  mreexexlem4d  16354  sscres  16530  xpcid  16876  evlfcllem  16908  hofcl  16946  isacs5lem  17216  frmdup3lem  17450  cayleylem2  17879  f1omvdco2  17914  symggen  17936  psgnunilem1  17959  pgp0  18057  sylow3lem2  18089  lsmdisjr  18143  lsmdisj2r  18144  subgdisj2  18151  efgval  18176  frgpuplem  18231  frgpup2  18235  gsumval3  18354  gsumzres  18356  gsum2d2lem  18418  dprdf1  18478  dmdprdsplit2lem  18490  dmdprdsplit2  18491  ablfaclem3  18532  prdsmgp  18656  unitgrp  18713  crng2idl  19287  psrass1lem  19425  evl1var  19748  pf1mpf  19764  pf1ind  19767  gsumfsum  19861  chrid  19923  znleval  19951  ocv1  20071  frlmip  20165  ellspd  20189  mamuvs2  20260  madurid  20498  baspartn  20806  mretopd  20944  ordtcld1  21049  ordtcld2  21050  leordtvallem1  21062  leordtvallem2  21063  paste  21146  imacmp  21248  cmpsub  21251  unconn  21280  1stckgen  21405  ptbasfi  21432  txcld  21454  ptclsg  21466  txdis1cn  21486  ptrescn  21490  hausdiag  21496  txkgen  21503  xkoptsub  21505  xkococnlem  21510  cnmpt21  21522  cnmpt22  21525  tgqtop  21563  qtoprest  21568  kqdisj  21583  hmeores  21622  hmphindis  21648  pt1hmeo  21657  ptuncnv  21658  ptunhmeo  21659  xpstopnlem1  21660  xkohmeo  21666  alexsublem  21895  ptcmplem2  21904  tmdcn2  21940  cldsubg  21961  qustgplem  21971  tsmsres  21994  ustbas2  22076  ressuss  22114  metreslem  22214  xpsdsval  22233  prdsxmslem2  22381  txmetcnp  22399  tngngp  22505  nrmtngdist  22508  remetdval  22639  cnheibor  22801  evth2  22806  pcoass  22870  ncvspi  23002  iscmet3  23137  rrxip  23224  minveclem2  23243  cmmbl  23348  nulmbl2  23350  volinun  23360  voliunlem1  23364  volsup  23370  ovolioo  23382  uniiccdif  23392  uniioombllem2  23397  uniioombllem3  23399  uniioombllem4  23400  uniioombllem5  23401  ismbf3d  23466  itg2uba  23555  itg2i1fseq  23567  itgsplitioo  23649  limcflf  23690  cnplimc  23696  limcun  23704  dvfval  23706  dvres  23720  dvres3a  23723  dvnp1  23733  dvn1  23734  dvexp3  23786  dvsincos  23789  mvth  23800  c1lip2  23806  dvfsumlem2  23835  itgsubstlem  23856  itgsubst  23857  coeeq2  24043  dgreq0  24066  dgrcolem2  24075  vieta1  24112  ulm2  24184  radcnv0  24215  abelthlem2  24231  tanarg  24410  advlogexp  24446  efopn  24449  logtayl  24451  cxpcn3  24534  ang180lem3  24586  quad2  24611  mcubic  24619  binom4  24622  dquart  24625  quart1lem  24627  quart1  24628  quartlem1  24629  asinlem3a  24642  efiatan  24684  tanatan  24691  atanbndlem  24697  dvatan  24707  ftalem3  24846  ftalem5  24848  basellem3  24854  mumullem2  24951  musum  24962  chtublem  24981  perfectlem2  25000  bposlem6  25059  bposlem9  25062  1lgs  25110  lgs1  25111  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgsquadlem2  25151  lgsquad2lem2  25155  2sqblem  25201  rpvmasum2  25246  log2sumbnd  25278  opphllem3  25686  vtxdun  26433  clwwlknon2num  27079  eucrct2eupth  27223  nvpi  27650  nvop  27659  phop  27801  minvecolem2  27859  hi01  28081  pjchi  28419  chjidm  28507  mayete3i  28715  ho0val  28737  lnop0  28953  adjbdlnb  29071  pjin2i  29180  mdslmd3i  29319  mdexchi  29322  imadifxp  29540  fcoinver  29544  padct  29625  f1od2  29627  fcobijfs  29629  ffsrn  29632  iocinif  29671  difioo  29672  gsummpt2co  29908  ofldchr  29942  symgfcoeu  29973  pmtrprfv2  29976  smatlem  29991  fvproj  30027  indf1ofs  30216  esumpad2  30246  hasheuni  30275  esumcvg2  30277  esum2dlem  30282  sigapildsys  30353  measxun2  30401  measunl  30407  measinblem  30411  carsgclctunlem1  30507  carsgclctunlem3  30510  sibfof  30530  sitgclg  30532  eulerpartlemgf  30569  probdif  30610  cndprobval  30623  ballotlemic  30696  signsvtn0  30775  signstres  30780  chtvalz  30835  hgt750lemd  30854  bnj1415  31232  subfacp1lem1  31287  subfacp1lem3  31290  subfacp1lem5  31292  cvmscld  31381  cvmlift2lem9a  31411  cvmlift2lem9  31419  noetalem3  31990  fwddifnp1  32397  csbpredg  33302  finxpreclem5  33362  ptrest  33538  poimirlem2  33541  poimirlem3  33542  poimirlem6  33545  poimirlem7  33546  poimirlem9  33548  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem24  33563  poimirlem25  33564  poimirlem27  33566  poimirlem28  33567  poimirlem29  33568  poimirlem31  33570  voliunnfl  33583  volsupnfl  33584  mbfresfi  33586  itg2addnclem2  33592  itg2addnclem3  33593  ftc1anclem5  33619  dvacos  33627  areacirclem5  33634  cocnv  33650  istotbnd3  33700  ssbnd  33717  eccnvepres3  34191  symrelim  34445  osumcllem9N  35568  4atexlemex2  35675  cdleme20j  35923  cdlemg47  36341  diaintclN  36664  dibintclN  36773  dihintcl  36950  lclkrlem2e  37117  lclkrlem2p  37128  lcfrlem31  37179  diophin  37653  monotuz  37823  monotoddzzfi  37824  oddcomabszz  37826  fnwe2val  37936  lnmlmic  37975  fiuneneq  38092  cytpval  38104  ntrkbimka  38653  ntrneifv2  38695  radcnvrat  38830  nzprmdif  38835  binomcxplemnotnn0  38872  ioccncflimc  40416  icocncflimc  40420  stoweidlem50  40585  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem107  40748  perfectALTVlem2  41956  elsprel  42050  logb2aval  42833  aacllem  42875
  Copyright terms: Public domain W3C validator