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

Theorem syl5eqr 2329
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5eqr.1  |-  B  =  A
syl5eqr.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
syl5eqr  |-  ( ph  ->  A  =  C )

Proof of Theorem syl5eqr
StepHypRef Expression
1 syl5eqr.1 . . 3  |-  B  =  A
21eqcomi 2287 . 2  |-  A  =  B
3 syl5eqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5eq 2327 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  3eqtr3g  2338  csbeq1a  3089  ssdifeq0  3536  pofun  4330  opabbi2dv  4833  fresin  5410  fresaunres2  5413  f1imacnv  5489  foimacnv  5490  funfv  5586  dffv2  5592  fsn2  5698  fnexALT  5742  funiunfvf  5775  fcof1o  5803  f1opw2  6071  fparlem3  6220  fparlem4  6221  riotaxfrd  6336  seqomlem1  6462  seqomlem4  6465  oasuc  6523  oesuclem  6524  omsuc  6525  onasuc  6527  onmsuc  6528  eqerlem  6692  pmresg  6795  fopwdom  6970  sbthlem8  6978  sbthlem9  6979  fodomr  7012  domss2  7020  mapen  7025  enp1i  7093  xpfi  7128  fiint  7133  f1opwfi  7159  marypha1lem  7186  unxpwdom  7303  cantnfval2  7370  mapfien  7399  cnfcom2lem  7404  infxpenlem  7641  cdainf  7818  isf34lem3  8001  isf34lem5  8004  axdc4lem  8081  ttukeylem6  8141  rankcf  8399  tskuni  8405  gruima  8424  dmrecnq  8592  ltexnq  8599  reclem3pr  8673  pn0sr  8723  mulgt0sr  8727  recdiv  9466  max0sub  10523  rexmul  10591  xmulmnf1  10596  xmulm1  10601  prunioo  10764  fseq1p1m1  10857  fzshftral  10869  seqp1i  11062  seqf1olem2  11086  seqfeq4  11095  binom3  11222  expmulnbnd  11233  discr  11238  bcn2  11331  hashun2  11365  hashun3  11366  hashdif  11375  hashfacen  11392  wrdeqs1cat  11475  cnrecnv  11650  rddif  11824  amgm2  11853  rlimres  12032  lo1res  12033  iseraltlem2  12155  iseralt  12157  fsumss  12198  fsumcl2lem  12204  isumclim3  12222  fsumcnv  12236  fsumtscopo  12260  fsumiun  12279  arisum2  12319  geoisum1c  12336  sinhval  12434  cos01bnd  12466  ruclem6  12513  sqr2irrlem  12526  bitsinv1  12633  sadadd2lem2  12641  eucalgval  12752  pcid  12925  prmreclem4  12966  4sqlem15  13006  4sqlem16  13007  ramcl  13076  strfv2d  13178  setsid  13187  imasvscafn  13439  xpsc0  13462  xpsc1  13463  xpsff1o  13470  xpsaddlem  13477  xpsvsca  13481  xpsle  13483  mreexexlem2d  13547  mreexexlem4d  13549  sscres  13700  xpcid  13963  evlfcllem  13995  hofcl  14033  isacs5lem  14272  frmdup3  14488  cayleylem2  14788  pgp0  14907  sylow3lem2  14939  lsmdisjr  14993  lsmdisj2r  14994  subgdisj2  15001  efgval  15026  frgpuplem  15081  frgpup2  15085  gsumval3  15191  gsumzres  15194  gsum2d2lem  15224  dprdf1  15268  dmdprdsplit2lem  15280  dmdprdsplit2  15281  ablfaclem3  15322  prdsmgp  15393  unitgrp  15449  crng2idl  15991  psrass1lem  16123  gsumfsum  16439  zrhval  16462  zlmval  16470  chrid  16481  znleval  16508  ocv1  16579  baspartn  16692  mretopd  16829  ordtcld1  16927  ordtcld2  16928  leordtvallem1  16940  leordtvallem2  16941  paste  17022  imacmp  17124  cmpsub  17127  uncon  17155  1stckgen  17249  ptbasfi  17276  txcld  17298  ptclsg  17309  txdis1cn  17329  ptrescn  17333  hausdiag  17339  txkgen  17346  xkoptsub  17348  xkococnlem  17353  cnmpt21  17365  cnmpt22  17368  tgqtop  17403  qtoprest  17408  kqdisj  17423  hmeores  17462  hmphindis  17488  pt1hmeo  17497  ptuncnv  17498  ptunhmeo  17499  xpstopnlem1  17500  xkohmeo  17506  alexsublem  17738  ptcmplem2  17747  tmdcn2  17772  cldsubg  17793  divstgplem  17803  tsmsres  17826  metreslem  17926  xpsdsval  17945  prdsxmslem2  18075  txmetcnp  18093  tngngp  18170  remetdval  18295  cnheibor  18453  evth2  18458  pcoass  18522  iscmet3  18719  minveclem2  18790  cmmbl  18892  nulmbl2  18894  volinun  18903  voliunlem1  18907  volsup  18913  ovolioo  18925  uniiccdif  18933  uniioombllem2  18938  uniioombllem3  18940  uniioombllem4  18941  uniioombllem5  18942  ismbf3d  19009  itg2uba  19098  itg2i1fseq  19110  itgsplitioo  19192  limcflf  19231  cnplimc  19237  limcun  19245  dvfval  19247  dvres  19261  dvres3a  19264  dvnp1  19274  dvn1  19275  dvexp3  19325  dvsincos  19328  mvth  19339  c1lip2  19345  dvfsumlem2  19374  itgsubstlem  19395  itgsubst  19396  evl1var  19415  pf1mpf  19435  pf1ind  19438  deg1val  19482  coeeq2  19624  dgreq0  19646  dgrcolem2  19655  vieta1  19692  ulm2  19764  radcnv0  19792  abelthlem2  19808  tanarg  19970  advlogexp  20002  efopn  20005  logtayl  20007  cxpcn3  20088  ang180lem3  20109  quad2  20135  mcubic  20143  binom4  20146  dquart  20149  quart1lem  20151  quart1  20152  quartlem1  20153  asinlem3a  20166  efiatan  20208  tanatan  20215  atanbndlem  20221  dvatan  20231  ftalem3  20312  ftalem5  20314  basellem3  20320  mumullem2  20418  musum  20431  chtublem  20450  perfectlem2  20469  bposlem6  20528  bposlem9  20531  1lgs  20576  lgs1  20577  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem3  20590  lgsquadlem2  20594  lgsquad2lem2  20598  2sqblem  20616  rpvmasum2  20661  log2sumbnd  20693  nvpi  21232  nvop  21243  phop  21396  minvecolem2  21454  hi01  21675  pjchi  22011  chjidm  22099  mayete3i  22307  mayete3iOLD  22308  ho0val  22330  lnop0  22546  adjbdlnb  22664  pjin2i  22773  mdslmd3i  22912  mdexchi  22915  ballotlemic  23065  difeq  23128  fimacnvinrn  23199  fmptpr  23214  iocinif  23274  difioo  23275  logb2aval  23393  hasheuni  23453  esumcvg2  23455  measxun2  23538  measinblem  23547  indf1ofs  23609  probdif  23623  cndprobval  23636  subfacp1lem1  23710  subfacp1lem3  23713  subfacp1lem5  23715  cvmscld  23804  cvmlift2lem9a  23834  cvmlift2lem9  23842  vdgrun  23893  relexpadd  24035  nofulllem5  24360  bpolyval  24784  bpoly3  24793  bpoly4  24794  fsumcube  24795  dvreacos  24924  areacirclem6  24930  f2imacnv  25052  mapex2  25140  islatalg  25183  clfsebs  25347  fincmpzer  25350  islimrs  25580  ishomb  25788  isfuna  25834  valtar  25883  vtarsu  25886  cocnv  26393  istotbnd3  26495  ssbnd  26512  diophin  26852  monotuz  27026  monotoddzzfi  27027  oddcomabszz  27029  fnwe2val  27146  lnmlmic  27186  ellspd  27254  f1omvdco2  27391  symggen  27411  psgnunilem1  27416  mamuvs2  27464  fiuneneq  27513  cytpval  27528  stoweidlem50  27799  s2prop  28089  s4prop  28090  bnj1415  29068  osumcllem9N  30153  4atexlemex2  30260  cdleme20j  30507  cdlemg47  30925  diaintclN  31248  dibintclN  31357  dihintcl  31534  lclkrlem2e  31701  lclkrlem2p  31712  lcfrlem31  31763
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator