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

Theorem syl5eqr 2809
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 2770 . 2 𝐴 = 𝐵
3 syl5eqr.2 . 2 (𝜑𝐵 = 𝐶)
42, 3syl5eq 2807 1 (𝜑𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2754
This theorem is referenced by:  3eqtr3g  2818  csbeq1a  3684  ssdifeq0  4196  pofun  5204  opabbi2dv  5428  cnvsng  5776  funcnvpr  6112  funcnvtp  6113  funcnvqp  6114  funcnvqpOLD  6115  fresin  6235  fresaunres2  6238  f1imacnv  6316  foimacnv  6317  funfv  6429  dffv2  6435  fimacnvinrn  6513  fsn2  6568  funiunfvf  6672  fcof1oinvd  6713  riotaxfrd  6807  f1opw2  7055  fnexALT  7299  fparlem3  7449  fparlem4  7450  mpt2curryd  7566  seqomlem1  7716  seqomlem4  7719  oasuc  7776  oesuclem  7777  omsuc  7778  onasuc  7780  onmsuc  7781  eqerlem  7948  pmresg  8054  fopwdom  8236  sbthlem8  8245  sbthlem9  8246  fodomr  8279  domss2  8287  mapen  8292  enp1i  8363  xpfi  8399  fiint  8405  f1opwfi  8438  mapfien  8481  marypha1lem  8507  unxpwdom  8662  cantnfval2  8742  infxpenlem  9047  cdainf  9227  isf34lem3  9410  isf34lem5  9413  axdc4lem  9490  ttukeylem6  9549  rankcf  9812  tskuni  9818  gruima  9837  dmrecnq  10003  ltexnq  10010  reclem3pr  10084  pn0sr  10135  mulgt0sr  10139  recdiv  10944  2resupmax  12233  max0sub  12241  rexmul  12315  xmulmnf1  12320  xmulm1  12325  prunioo  12515  fseq1p1m1  12628  fzshftral  12642  seqp1i  13032  seqf1olem2  13056  seqfeq4  13065  binom3  13200  expmulnbnd  13211  discr  13216  bcn2  13321  hashun2  13385  hashun3  13386  hashdif  13414  hashgt12el  13423  hashgt12el2  13424  hashfacen  13451  wrdeqs1cat  13695  swrdccat3a  13715  s2prop  13873  s4prop  13876  s3sndisj  13928  s3iunsndisj  13929  cnrecnv  14125  rddif  14300  amgm2  14329  rlimres  14509  lo1res  14510  iseraltlem2  14633  iseralt  14635  fsumss  14676  fsumcl2lem  14682  isumclim3  14710  fsumcnv  14724  telfsumo  14754  fsumiun  14773  arisum2  14813  geoisum1c  14831  fprodss  14898  fprodser  14899  fprodcl2lem  14900  fprodsplit  14916  fprodn0  14929  fprodcnv  14933  iprodclim3  14951  risefac1  14984  fallfac1  14985  bpolyval  15000  bpoly3  15009  bpoly4  15010  fsumcube  15011  sinhval  15104  cos01bnd  15136  ruclem6  15184  sqrt2irrlemOLD  15198  sadadd2lem2  15395  eucalgval  15518  pcid  15800  prmreclem4  15846  4sqlem15  15886  4sqlem16  15887  ramcl  15956  strfv2d  16128  setsid  16137  imasvscafn  16420  xpsc0  16443  xpsc1  16444  xpsff1o  16451  xpsaddlem  16458  xpsvsca  16462  xpsle  16464  mreexexlem2d  16528  mreexexlem4d  16530  sscres  16705  xpcid  17051  evlfcllem  17083  hofcl  17121  isacs5lem  17391  frmdup3lem  17625  cayleylem2  18054  f1omvdco2  18089  symggen  18111  psgnunilem1  18134  pgp0  18232  sylow3lem2  18264  lsmdisjr  18318  lsmdisj2r  18319  subgdisj2  18326  efgval  18351  frgpuplem  18406  frgpup2  18410  gsumval3  18529  gsumzres  18531  gsum2d2lem  18593  dprdf1  18653  dmdprdsplit2lem  18665  dmdprdsplit2  18666  ablfaclem3  18707  prdsmgp  18831  unitgrp  18888  crng2idl  19462  psrass1lem  19600  evl1var  19923  pf1mpf  19939  pf1ind  19942  gsumfsum  20036  chrid  20098  znleval  20126  ocv1  20246  frlmip  20340  ellspd  20364  mamuvs2  20435  madurid  20673  baspartn  20981  mretopd  21119  ordtcld1  21224  ordtcld2  21225  leordtvallem1  21237  leordtvallem2  21238  paste  21321  imacmp  21423  cmpsub  21426  unconn  21455  1stckgen  21580  ptbasfi  21607  txcld  21629  ptclsg  21641  txdis1cn  21661  ptrescn  21665  hausdiag  21671  txkgen  21678  xkoptsub  21680  xkococnlem  21685  cnmpt21  21697  cnmpt22  21700  tgqtop  21738  qtoprest  21743  kqdisj  21758  hmeores  21797  hmphindis  21823  pt1hmeo  21832  ptuncnv  21833  ptunhmeo  21834  xpstopnlem1  21835  xkohmeo  21841  alexsublem  22070  ptcmplem2  22079  tmdcn2  22115  cldsubg  22136  qustgplem  22146  tsmsres  22169  ustbas2  22251  ressuss  22289  metreslem  22389  xpsdsval  22408  prdsxmslem2  22556  txmetcnp  22574  tngngp  22680  nrmtngdist  22683  remetdval  22814  cnheibor  22976  evth2  22981  pcoass  23045  ncvspi  23177  iscmet3  23312  rrxip  23399  minveclem2  23418  cmmbl  23523  nulmbl2  23525  volinun  23535  voliunlem1  23539  volsup  23545  ovolioo  23557  uniiccdif  23567  uniioombllem2  23572  uniioombllem3  23574  uniioombllem4  23575  uniioombllem5  23576  ismbf3d  23641  itg2uba  23730  itg2i1fseq  23742  itgsplitioo  23824  limcflf  23865  cnplimc  23871  limcun  23879  dvfval  23881  dvres  23895  dvres3a  23898  dvnp1  23908  dvn1  23909  dvexp3  23961  dvsincos  23964  mvth  23975  c1lip2  23981  dvfsumlem2  24010  itgsubstlem  24031  itgsubst  24032  coeeq2  24218  dgreq0  24241  dgrcolem2  24250  vieta1  24287  ulm2  24359  radcnv0  24390  abelthlem2  24406  tanarg  24586  advlogexp  24622  efopn  24625  logtayl  24627  cxpcn3  24710  ang180lem3  24762  quad2  24787  mcubic  24795  binom4  24798  dquart  24801  quart1lem  24803  quart1  24804  quartlem1  24805  asinlem3a  24818  efiatan  24860  tanatan  24867  atanbndlem  24873  dvatan  24883  ftalem3  25022  ftalem5  25024  basellem3  25030  mumullem2  25127  musum  25138  chtublem  25157  perfectlem2  25176  bposlem6  25235  bposlem9  25238  1lgs  25286  lgs1  25287  lgseisenlem1  25321  lgseisenlem2  25322  lgseisenlem3  25323  lgsquadlem2  25327  lgsquad2lem2  25331  2sqblem  25377  rpvmasum2  25422  log2sumbnd  25454  opphllem3  25862  vtxdun  26609  clwwlknon2num  27275  eucrct2eupth  27419  nvpi  27853  nvop  27862  phop  28004  minvecolem2  28062  hi01  28284  pjchi  28622  chjidm  28710  mayete3i  28918  ho0val  28940  lnop0  29156  adjbdlnb  29274  pjin2i  29383  mdslmd3i  29522  mdexchi  29525  imadifxp  29743  fcoinver  29747  padct  29828  f1od2  29830  fcobijfs  29832  ffsrn  29835  iocinif  29874  difioo  29875  gsummpt2co  30111  ofldchr  30145  symgfcoeu  30176  pmtrprfv2  30179  smatlem  30194  fvproj  30230  indf1ofs  30419  esumpad2  30449  hasheuni  30478  esumcvg2  30480  esum2dlem  30485  sigapildsys  30556  measxun2  30604  measunl  30610  measinblem  30614  carsgclctunlem1  30710  carsgclctunlem3  30713  sibfof  30733  sitgclg  30735  eulerpartlemgf  30772  probdif  30813  cndprobval  30826  ballotlemic  30899  signsvtn0  30978  signstres  30983  chtvalz  31038  hgt750lemd  31057  bnj1415  31435  subfacp1lem1  31490  subfacp1lem3  31493  subfacp1lem5  31495  cvmscld  31584  cvmlift2lem9a  31614  cvmlift2lem9  31622  noetalem3  32193  fwddifnp1  32600  csbpredg  33502  finxpreclem5  33562  ptrest  33740  poimirlem2  33743  poimirlem3  33744  poimirlem6  33747  poimirlem7  33748  poimirlem9  33750  poimirlem11  33752  poimirlem12  33753  poimirlem16  33757  poimirlem17  33758  poimirlem19  33760  poimirlem20  33761  poimirlem24  33765  poimirlem25  33766  poimirlem27  33768  poimirlem28  33769  poimirlem29  33770  poimirlem31  33772  voliunnfl  33785  volsupnfl  33786  mbfresfi  33788  itg2addnclem2  33794  itg2addnclem3  33795  ftc1anclem5  33821  dvacos  33829  areacirclem5  33836  cocnv  33852  istotbnd3  33902  ssbnd  33919  eccnvepres3  34393  symrelim  34647  osumcllem9N  35772  4atexlemex2  35879  cdleme20j  36127  cdlemg47  36545  diaintclN  36868  dibintclN  36977  dihintcl  37154  lclkrlem2e  37321  lclkrlem2p  37332  lcfrlem31  37383  diophin  37857  monotuz  38027  monotoddzzfi  38028  oddcomabszz  38030  fnwe2val  38140  lnmlmic  38179  fiuneneq  38296  cytpval  38308  ntrkbimka  38857  ntrneifv2  38899  radcnvrat  39034  nzprmdif  39039  binomcxplemnotnn0  39076  ioccncflimc  40620  icocncflimc  40624  stoweidlem50  40789  fourierdlem89  40934  fourierdlem90  40935  fourierdlem91  40936  fourierdlem107  40952  perfectALTVlem2  42160  elsprel  42254  logb2aval  43037  aacllem  43079
  Copyright terms: Public domain W3C validator