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

Theorem syl5eqr 2342
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 2300 . 2  |-  A  =  B
3 syl5eqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5eq 2340 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  3eqtr3g  2351  csbeq1a  3102  ssdifeq0  3549  pofun  4346  opabbi2dv  4849  fresin  5426  fresaunres2  5429  f1imacnv  5505  foimacnv  5506  funfv  5602  dffv2  5608  fsn2  5714  fnexALT  5758  funiunfvf  5791  fcof1o  5819  f1opw2  6087  fparlem3  6236  fparlem4  6237  riotaxfrd  6352  seqomlem1  6478  seqomlem4  6481  oasuc  6539  oesuclem  6540  omsuc  6541  onasuc  6543  onmsuc  6544  eqerlem  6708  pmresg  6811  fopwdom  6986  sbthlem8  6994  sbthlem9  6995  fodomr  7028  domss2  7036  mapen  7041  enp1i  7109  xpfi  7144  fiint  7149  f1opwfi  7175  marypha1lem  7202  unxpwdom  7319  cantnfval2  7386  mapfien  7415  cnfcom2lem  7420  infxpenlem  7657  cdainf  7834  isf34lem3  8017  isf34lem5  8020  axdc4lem  8097  ttukeylem6  8157  rankcf  8415  tskuni  8421  gruima  8440  dmrecnq  8608  ltexnq  8615  reclem3pr  8689  pn0sr  8739  mulgt0sr  8743  recdiv  9482  max0sub  10539  rexmul  10607  xmulmnf1  10612  xmulm1  10617  prunioo  10780  fseq1p1m1  10873  fzshftral  10885  seqp1i  11078  seqf1olem2  11102  seqfeq4  11111  binom3  11238  expmulnbnd  11249  discr  11254  bcn2  11347  hashun2  11381  hashun3  11382  hashdif  11391  hashfacen  11408  wrdeqs1cat  11491  cnrecnv  11666  rddif  11840  amgm2  11869  rlimres  12048  lo1res  12049  iseraltlem2  12171  iseralt  12173  fsumss  12214  fsumcl2lem  12220  isumclim3  12238  fsumcnv  12252  fsumtscopo  12276  fsumiun  12295  arisum2  12335  geoisum1c  12352  sinhval  12450  cos01bnd  12482  ruclem6  12529  sqr2irrlem  12542  bitsinv1  12649  sadadd2lem2  12657  eucalgval  12768  pcid  12941  prmreclem4  12982  4sqlem15  13022  4sqlem16  13023  ramcl  13092  strfv2d  13194  setsid  13203  imasvscafn  13455  xpsc0  13478  xpsc1  13479  xpsff1o  13486  xpsaddlem  13493  xpsvsca  13497  xpsle  13499  mreexexlem2d  13563  mreexexlem4d  13565  sscres  13716  xpcid  13979  evlfcllem  14011  hofcl  14049  isacs5lem  14288  frmdup3  14504  cayleylem2  14804  pgp0  14923  sylow3lem2  14955  lsmdisjr  15009  lsmdisj2r  15010  subgdisj2  15017  efgval  15042  frgpuplem  15097  frgpup2  15101  gsumval3  15207  gsumzres  15210  gsum2d2lem  15240  dprdf1  15284  dmdprdsplit2lem  15296  dmdprdsplit2  15297  ablfaclem3  15338  prdsmgp  15409  unitgrp  15465  crng2idl  16007  psrass1lem  16139  gsumfsum  16455  zrhval  16478  zlmval  16486  chrid  16497  znleval  16524  ocv1  16595  baspartn  16708  mretopd  16845  ordtcld1  16943  ordtcld2  16944  leordtvallem1  16956  leordtvallem2  16957  paste  17038  imacmp  17140  cmpsub  17143  uncon  17171  1stckgen  17265  ptbasfi  17292  txcld  17314  ptclsg  17325  txdis1cn  17345  ptrescn  17349  hausdiag  17355  txkgen  17362  xkoptsub  17364  xkococnlem  17369  cnmpt21  17381  cnmpt22  17384  tgqtop  17419  qtoprest  17424  kqdisj  17439  hmeores  17478  hmphindis  17504  pt1hmeo  17513  ptuncnv  17514  ptunhmeo  17515  xpstopnlem1  17516  xkohmeo  17522  alexsublem  17754  ptcmplem2  17763  tmdcn2  17788  cldsubg  17809  divstgplem  17819  tsmsres  17842  metreslem  17942  xpsdsval  17961  prdsxmslem2  18091  txmetcnp  18109  tngngp  18186  remetdval  18311  cnheibor  18469  evth2  18474  pcoass  18538  iscmet3  18735  minveclem2  18806  cmmbl  18908  nulmbl2  18910  volinun  18919  voliunlem1  18923  volsup  18929  ovolioo  18941  uniiccdif  18949  uniioombllem2  18954  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  ismbf3d  19025  itg2uba  19114  itg2i1fseq  19126  itgsplitioo  19208  limcflf  19247  cnplimc  19253  limcun  19261  dvfval  19263  dvres  19277  dvres3a  19280  dvnp1  19290  dvn1  19291  dvexp3  19341  dvsincos  19344  mvth  19355  c1lip2  19361  dvfsumlem2  19390  itgsubstlem  19411  itgsubst  19412  evl1var  19431  pf1mpf  19451  pf1ind  19454  deg1val  19498  coeeq2  19640  dgreq0  19662  dgrcolem2  19671  vieta1  19708  ulm2  19780  radcnv0  19808  abelthlem2  19824  tanarg  19986  advlogexp  20018  efopn  20021  logtayl  20023  cxpcn3  20104  ang180lem3  20125  quad2  20151  mcubic  20159  binom4  20162  dquart  20165  quart1lem  20167  quart1  20168  quartlem1  20169  asinlem3a  20182  efiatan  20224  tanatan  20231  atanbndlem  20237  dvatan  20247  ftalem3  20328  ftalem5  20330  basellem3  20336  mumullem2  20434  musum  20447  chtublem  20466  perfectlem2  20485  bposlem6  20544  bposlem9  20547  1lgs  20592  lgs1  20593  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem3  20606  lgsquadlem2  20610  lgsquad2lem2  20614  2sqblem  20632  rpvmasum2  20677  log2sumbnd  20709  nvpi  21248  nvop  21259  phop  21412  minvecolem2  21470  hi01  21691  pjchi  22027  chjidm  22115  mayete3i  22323  mayete3iOLD  22324  ho0val  22346  lnop0  22562  adjbdlnb  22680  pjin2i  22789  mdslmd3i  22928  mdexchi  22931  ballotlemic  23081  difeq  23144  fimacnvinrn  23214  fmptpr  23229  iocinif  23289  difioo  23290  logb2aval  23408  hasheuni  23468  esumcvg2  23470  measxun2  23553  measinblem  23562  indf1ofs  23624  probdif  23638  cndprobval  23651  subfacp1lem1  23725  subfacp1lem3  23728  subfacp1lem5  23730  cvmscld  23819  cvmlift2lem9a  23849  cvmlift2lem9  23857  vdgrun  23908  relexpadd  24050  nofulllem5  24431  bpolyval  24856  bpoly3  24865  bpoly4  24866  fsumcube  24867  itg2addnclem2  25004  itg2addnc  25005  itgaddnclem2  25010  dvreacos  25027  areacirclem6  25033  f2imacnv  25155  mapex2  25243  islatalg  25286  clfsebs  25450  fincmpzer  25453  islimrs  25683  ishomb  25891  isfuna  25937  valtar  25986  vtarsu  25989  cocnv  26496  istotbnd3  26598  ssbnd  26615  diophin  26955  monotuz  27129  monotoddzzfi  27130  oddcomabszz  27132  fnwe2val  27249  lnmlmic  27289  ellspd  27357  f1omvdco2  27494  symggen  27514  psgnunilem1  27519  mamuvs2  27567  fiuneneq  27616  cytpval  27631  stoweidlem50  27902  hashgt12el  28218  hashgt12el2  28219  s2prop  28221  s4prop  28222  bnj1415  29384  osumcllem9N  30775  4atexlemex2  30882  cdleme20j  31129  cdlemg47  31547  diaintclN  31870  dibintclN  31979  dihintcl  32156  lclkrlem2e  32323  lclkrlem2p  32334  lcfrlem31  32385
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator