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

Theorem syl5eqr 2481
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 2439 . 2  |-  A  =  B
3 syl5eqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5eq 2479 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  3eqtr3g  2490  csbeq1a  3251  ssdifeq0  3702  pofun  4511  opabbi2dv  5014  fresin  5604  fresaunres2  5607  f1imacnv  5683  foimacnv  5684  funfv  5782  dffv2  5788  fsn2  5900  fnexALT  5954  funiunfvf  5988  fcof1o  6018  f1opw2  6290  fparlem3  6440  fparlem4  6441  riotaxfrd  6573  seqomlem1  6699  seqomlem4  6702  oasuc  6760  oesuclem  6761  omsuc  6762  onasuc  6764  onmsuc  6765  eqerlem  6929  pmresg  7033  fopwdom  7208  sbthlem8  7216  sbthlem9  7217  fodomr  7250  domss2  7258  mapen  7263  enp1i  7335  xpfi  7370  fiint  7375  f1opwfi  7402  marypha1lem  7430  unxpwdom  7549  cantnfval2  7616  mapfien  7645  cnfcom2lem  7650  infxpenlem  7887  cdainf  8064  isf34lem3  8247  isf34lem5  8250  axdc4lem  8327  ttukeylem6  8386  rankcf  8644  tskuni  8650  gruima  8669  dmrecnq  8837  ltexnq  8844  reclem3pr  8918  pn0sr  8968  mulgt0sr  8972  recdiv  9712  max0sub  10774  rexmul  10842  xmulmnf1  10847  xmulm1  10852  prunioo  11017  fseq1p1m1  11114  fzshftral  11126  seqp1i  11331  seqf1olem2  11355  seqfeq4  11364  binom3  11492  expmulnbnd  11503  discr  11508  bcn2  11602  hashun2  11649  hashun3  11650  hashdif  11670  hashgt12el  11674  hashgt12el2  11675  hashfacen  11695  wrdeqs1cat  11781  s2prop  11853  s4prop  11854  cnrecnv  11962  rddif  12136  amgm2  12165  rlimres  12344  lo1res  12345  iseraltlem2  12468  iseralt  12470  fsumss  12511  fsumcl2lem  12517  isumclim3  12535  fsumcnv  12549  fsumtscopo  12573  fsumiun  12592  arisum2  12632  geoisum1c  12649  sinhval  12747  cos01bnd  12779  ruclem6  12826  sqr2irrlem  12839  sadadd2lem2  12954  eucalgval  13065  pcid  13238  prmreclem4  13279  4sqlem15  13319  4sqlem16  13320  ramcl  13389  strfv2d  13491  setsid  13500  imasvscafn  13754  xpsc0  13777  xpsc1  13778  xpsff1o  13785  xpsaddlem  13792  xpsvsca  13796  xpsle  13798  mreexexlem2d  13862  mreexexlem4d  13864  sscres  14015  xpcid  14278  evlfcllem  14310  hofcl  14348  isacs5lem  14587  frmdup3  14803  cayleylem2  15103  pgp0  15222  sylow3lem2  15254  lsmdisjr  15308  lsmdisj2r  15309  subgdisj2  15316  efgval  15341  frgpuplem  15396  frgpup2  15400  gsumval3  15506  gsumzres  15509  gsum2d2lem  15539  dprdf1  15583  dmdprdsplit2lem  15595  dmdprdsplit2  15596  ablfaclem3  15637  prdsmgp  15708  unitgrp  15764  crng2idl  16302  psrass1lem  16434  gsumfsum  16758  zrhval  16781  zlmval  16789  chrid  16800  znleval  16827  ocv1  16898  baspartn  17011  mretopd  17148  ordtcld1  17253  ordtcld2  17254  leordtvallem1  17266  leordtvallem2  17267  paste  17350  imacmp  17452  cmpsub  17455  uncon  17484  1stckgen  17578  ptbasfi  17605  txcld  17627  ptclsg  17639  txdis1cn  17659  ptrescn  17663  hausdiag  17669  txkgen  17676  xkoptsub  17678  xkococnlem  17683  cnmpt21  17695  cnmpt22  17698  tgqtop  17736  qtoprest  17741  kqdisj  17756  hmeores  17795  hmphindis  17821  pt1hmeo  17830  ptuncnv  17831  ptunhmeo  17832  xpstopnlem1  17833  xkohmeo  17839  alexsublem  18067  ptcmplem2  18076  tmdcn2  18111  cldsubg  18132  divstgplem  18142  tsmsres  18165  ustbas2  18247  ressuss  18285  metreslem  18384  xpsdsval  18403  prdsxmslem2  18551  txmetcnp  18569  tngngp  18687  remetdval  18812  cnheibor  18972  evth2  18977  pcoass  19041  iscmet3  19238  minveclem2  19319  cmmbl  19421  nulmbl2  19423  volinun  19432  voliunlem1  19436  volsup  19442  ovolioo  19454  uniiccdif  19462  uniioombllem2  19467  uniioombllem3  19469  uniioombllem4  19470  uniioombllem5  19471  ismbf3d  19538  itg2uba  19627  itg2i1fseq  19639  itgsplitioo  19721  limcflf  19760  cnplimc  19766  limcun  19774  dvfval  19776  dvres  19790  dvres3a  19793  dvnp1  19803  dvn1  19804  dvexp3  19854  dvsincos  19857  mvth  19868  c1lip2  19874  dvfsumlem2  19903  itgsubstlem  19924  itgsubst  19925  evl1var  19944  pf1mpf  19964  pf1ind  19967  deg1val  20011  coeeq2  20153  dgreq0  20175  dgrcolem2  20184  vieta1  20221  ulm2  20293  radcnv0  20324  abelthlem2  20340  tanarg  20506  advlogexp  20538  efopn  20541  logtayl  20543  cxpcn3  20624  ang180lem3  20645  quad2  20671  mcubic  20679  binom4  20682  dquart  20685  quart1lem  20687  quart1  20688  quartlem1  20689  asinlem3a  20702  efiatan  20744  tanatan  20751  atanbndlem  20757  dvatan  20767  ftalem3  20849  ftalem5  20851  basellem3  20857  mumullem2  20955  musum  20968  chtublem  20987  perfectlem2  21006  bposlem6  21065  bposlem9  21068  1lgs  21113  lgs1  21114  lgseisenlem1  21125  lgseisenlem2  21126  lgseisenlem3  21127  lgsquadlem2  21131  lgsquad2lem2  21135  2sqblem  21153  rpvmasum2  21198  log2sumbnd  21230  vdgrun  21664  vdgrfiun  21665  nvpi  22147  nvop  22158  phop  22311  minvecolem2  22369  hi01  22590  pjchi  22926  chjidm  23014  mayete3i  23222  mayete3iOLD  23223  ho0val  23245  lnop0  23461  adjbdlnb  23579  pjin2i  23688  mdslmd3i  23827  mdexchi  23830  imadifxp  24030  fimacnvinrn  24039  fmptpr  24054  iocinif  24136  difioo  24137  ofldchr  24236  logb2aval  24383  indf1ofs  24415  hasheuni  24467  esumcvg2  24469  measxun2  24556  measunl  24562  measinblem  24566  sibfof  24646  sitgclg  24648  probdif  24670  cndprobval  24683  ballotlemic  24756  subfacp1lem1  24857  subfacp1lem3  24860  subfacp1lem5  24862  cvmscld  24952  cvmlift2lem9a  24982  cvmlift2lem9  24990  relexpadd  25130  fprodss  25266  fprodser  25267  fprodcl2lem  25268  fprodsplit  25281  fprodn0  25295  fprodcnv  25299  iprodclim3  25305  risefac1  25341  fallfac1  25342  nofulllem5  25653  bpolyval  26087  bpoly3  26096  bpoly4  26097  fsumcube  26098  voliunnfl  26240  volsupnfl  26241  mbfresfi  26243  itg2addnclem2  26247  itg2addnclem3  26248  ftc1anclem5  26274  dvreacos  26281  areacirclem6  26287  cocnv  26418  istotbnd3  26471  ssbnd  26488  diophin  26822  monotuz  26995  monotoddzzfi  26996  oddcomabszz  26998  fnwe2val  27115  lnmlmic  27154  ellspd  27222  f1omvdco2  27359  symggen  27379  psgnunilem1  27384  mamuvs2  27432  fiuneneq  27481  cytpval  27496  stoweidlem50  27766  swrdccat3a  28183  bnj1415  29344  osumcllem9N  30698  4atexlemex2  30805  cdleme20j  31052  cdlemg47  31470  diaintclN  31793  dibintclN  31902  dihintcl  32079  lclkrlem2e  32246  lclkrlem2p  32257  lcfrlem31  32308
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator