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

Theorem syl5eqr 2854
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 2815 . 2 𝐴 = 𝐵
3 syl5eqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5eq 2852 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799
This theorem is referenced by:  3eqtr3g  2863  csbeq1a  3737  ssdifeq0  4247  pofun  5248  opabbi2dv  5473  cnvsng  5828  funcnvpr  6162  funcnvtp  6163  funcnvqp  6164  fresin  6288  fresaunres2  6291  f1imacnv  6369  foimacnv  6370  funfv  6486  dffv2  6492  fimacnvinrn  6570  fsn2  6626  funiunfvf  6731  fcof1oinvd  6772  riotaxfrd  6866  f1opw2  7118  fnexALT  7362  fparlem3  7513  fparlem4  7514  mpt2curryd  7630  seqomlem1  7781  seqomlem4  7784  oasuc  7841  oesuclem  7842  omsuc  7843  onasuc  7845  onmsuc  7846  eqerlem  8013  pmresg  8120  fopwdom  8307  sbthlem8  8316  sbthlem9  8317  fodomr  8350  domss2  8358  mapen  8363  enp1i  8434  xpfi  8470  fiint  8476  f1opwfi  8509  mapfien  8552  marypha1lem  8578  unxpwdom  8733  cantnfval2  8813  infxpenlem  9119  cdainf  9299  isf34lem3  9482  isf34lem5  9485  axdc4lem  9562  ttukeylem6  9621  rankcf  9884  tskuni  9890  gruima  9909  dmrecnq  10075  ltexnq  10082  reclem3pr  10156  pn0sr  10207  mulgt0sr  10211  recdiv  11016  2resupmax  12237  max0sub  12245  rexmul  12319  xmulmnf1  12324  xmulm1  12329  prunioo  12524  fseq1p1m1  12637  fzshftral  12651  seqp1i  13040  seqf1olem2  13064  seqfeq4  13073  binom3  13208  expmulnbnd  13219  discr  13224  bcn2  13326  hashun2  13390  hashun3  13391  hashdif  13418  hashgt12el  13427  hashgt12el2  13428  hashfacen  13455  wrdeqs1cat  13698  swrdccat3a  13718  s2prop  13876  s4prop  13879  s3sndisj  13931  s3iunsndisj  13932  cnrecnv  14128  rddif  14303  amgm2  14332  rlimres  14512  lo1res  14513  iseraltlem2  14636  iseralt  14638  fsumss  14679  fsumcl2lem  14685  isumclim3  14713  fsumcnv  14727  telfsumo  14756  fsumiun  14775  arisum2  14815  geoisum1c  14833  fprodss  14899  fprodser  14900  fprodcl2lem  14901  fprodsplit  14917  fprodn0  14930  fprodcnv  14934  iprodclim3  14951  risefac1  14984  fallfac1  14985  bpolyval  15000  bpoly3  15009  bpoly4  15010  fsumcube  15011  sinhval  15104  cos01bnd  15136  ruclem6  15184  sqrt2irrlemOLD  15198  sadadd2lem2  15391  eucalgval  15514  pcid  15794  prmreclem4  15840  4sqlem15  15880  4sqlem16  15881  ramcl  15950  strfv2d  16116  setsid  16125  imasvscafn  16402  xpsc0  16425  xpsc1  16426  xpsff1o  16433  xpsaddlem  16440  xpsvsca  16444  xpsle  16446  mreexexlem2d  16510  mreexexlem4d  16512  sscres  16687  xpcid  17034  evlfcllem  17066  hofcl  17104  isacs5lem  17374  frmdup3lem  17608  cayleylem2  18034  f1omvdco2  18069  symggen  18091  psgnunilem1  18114  pgp0  18212  sylow3lem2  18244  lsmdisjr  18298  lsmdisj2r  18299  subgdisj2  18306  efgval  18331  frgpuplem  18386  frgpup2  18390  gsumval3  18509  gsumzres  18511  gsum2d2lem  18573  dprdf1  18634  dmdprdsplit2lem  18646  dmdprdsplit2  18647  ablfaclem3  18688  prdsmgp  18812  unitgrp  18869  crng2idl  19448  psrass1lem  19586  evl1var  19908  pf1mpf  19924  pf1ind  19927  gsumfsum  20021  chrid  20083  znleval  20110  ocv1  20233  frlmip  20327  ellspd  20351  mamuvs2  20422  madurid  20661  baspartn  20972  mretopd  21110  ordtcld1  21215  ordtcld2  21216  leordtvallem1  21228  leordtvallem2  21229  paste  21312  imacmp  21414  cmpsub  21417  unconn  21446  1stckgen  21571  ptbasfi  21598  txcld  21620  ptclsg  21632  txdis1cn  21652  ptrescn  21656  hausdiag  21662  txkgen  21669  xkoptsub  21671  xkococnlem  21676  cnmpt21  21688  cnmpt22  21691  tgqtop  21729  qtoprest  21734  kqdisj  21749  hmeores  21788  hmphindis  21814  pt1hmeo  21823  ptuncnv  21824  ptunhmeo  21825  xpstopnlem1  21826  xkohmeo  21832  alexsublem  22061  ptcmplem2  22070  tmdcn2  22106  cldsubg  22127  qustgplem  22137  tsmsres  22160  ustbas2  22242  ressuss  22280  metreslem  22380  xpsdsval  22399  prdsxmslem2  22547  txmetcnp  22565  tngngp  22671  nrmtngdist  22674  remetdval  22805  cnheibor  22967  evth2  22972  pcoass  23036  ncvspi  23168  iscmet3  23303  rrxip  23390  minveclem2  23409  cmmbl  23515  nulmbl2  23517  volinun  23527  voliunlem1  23531  volsup  23537  ovolioo  23549  uniiccdif  23559  uniioombllem2  23564  uniioombllem3  23566  uniioombllem4  23567  uniioombllem5  23568  ismbf3d  23635  itg2uba  23724  itg2i1fseq  23736  itgsplitioo  23818  limcflf  23859  cnplimc  23865  limcun  23873  dvfval  23875  dvres  23889  dvres3a  23892  dvnp1  23902  dvn1  23903  dvexp3  23955  dvsincos  23958  mvth  23969  c1lip2  23975  dvfsumlem2  24004  itgsubstlem  24025  itgsubst  24026  coeeq2  24212  dgreq0  24235  dgrcolem2  24244  vieta1  24281  ulm2  24353  radcnv0  24384  abelthlem2  24400  tanarg  24579  advlogexp  24615  efopn  24618  logtayl  24620  cxpcn3  24703  ang180lem3  24755  quad2  24780  mcubic  24788  binom4  24791  dquart  24794  quart1lem  24796  quart1  24797  quartlem1  24798  asinlem3a  24811  efiatan  24853  tanatan  24860  atanbndlem  24866  dvatan  24876  ftalem3  25015  ftalem5  25017  basellem3  25023  mumullem2  25120  musum  25131  chtublem  25150  perfectlem2  25169  bposlem6  25228  bposlem9  25231  1lgs  25279  lgs1  25280  lgseisenlem1  25314  lgseisenlem2  25315  lgseisenlem3  25316  lgsquadlem2  25320  lgsquad2lem2  25324  2sqblem  25370  rpvmasum2  25415  log2sumbnd  25447  opphllem3  25855  vtxdun  26605  clwwlknon2num  27273  eucrct2eupth  27418  nvpi  27850  nvop  27859  phop  28001  minvecolem2  28059  hi01  28281  pjchi  28619  chjidm  28707  mayete3i  28915  ho0val  28937  lnop0  29153  adjbdlnb  29271  pjin2i  29380  mdslmd3i  29519  mdexchi  29522  imadifxp  29739  fcoinver  29743  padct  29824  f1od2  29826  fcobijfs  29828  ffsrn  29831  iocinif  29870  difioo  29871  gsummpt2co  30105  ofldchr  30139  symgfcoeu  30170  pmtrprfv2  30173  smatlem  30188  fvproj  30224  indf1ofs  30413  esumpad2  30443  hasheuni  30472  esumcvg2  30474  esum2dlem  30479  sigapildsys  30550  measxun2  30598  measunl  30604  measinblem  30608  carsgclctunlem1  30704  carsgclctunlem3  30707  sibfof  30727  sitgclg  30729  eulerpartlemgf  30766  probdif  30807  cndprobval  30820  ballotlemic  30893  signsvtn0  30972  signstres  30977  chtvalz  31032  hgt750lemd  31051  bnj1415  31429  subfacp1lem1  31484  subfacp1lem3  31487  subfacp1lem5  31489  cvmscld  31578  cvmlift2lem9a  31608  cvmlift2lem9  31616  noetalem3  32186  fwddifnp1  32593  csbpredg  33489  finxpreclem5  33548  ptrest  33721  poimirlem2  33724  poimirlem3  33725  poimirlem6  33728  poimirlem7  33729  poimirlem9  33731  poimirlem11  33733  poimirlem12  33734  poimirlem16  33738  poimirlem17  33739  poimirlem19  33741  poimirlem20  33742  poimirlem24  33746  poimirlem25  33747  poimirlem27  33749  poimirlem28  33750  poimirlem29  33751  poimirlem31  33753  voliunnfl  33766  volsupnfl  33767  mbfresfi  33768  itg2addnclem2  33774  itg2addnclem3  33775  ftc1anclem5  33801  dvacos  33809  areacirclem5  33816  cocnv  33832  istotbnd3  33881  ssbnd  33898  eccnvepres3  34367  symrelim  34618  osumcllem9N  35744  4atexlemex2  35851  cdleme20j  36099  cdlemg47  36517  diaintclN  36839  dibintclN  36948  dihintcl  37125  lclkrlem2e  37292  lclkrlem2p  37303  lcfrlem31  37354  diophin  37838  monotuz  38007  monotoddzzfi  38008  oddcomabszz  38010  fnwe2val  38120  lnmlmic  38159  fiuneneq  38276  cytpval  38288  ntrkbimka  38836  ntrneifv2  38878  radcnvrat  39013  nzprmdif  39018  binomcxplemnotnn0  39055  ioccncflimc  40578  icocncflimc  40582  stoweidlem50  40746  fourierdlem89  40891  fourierdlem90  40892  fourierdlem91  40893  fourierdlem107  40909  perfectALTVlem2  42206  elsprel  42293  logb2aval  43076  aacllem  43118
  Copyright terms: Public domain W3C validator