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

Theorem syl5eqr 2426
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 2384 . 2  |-  A  =  B
3 syl5eqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5eq 2424 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  3eqtr3g  2435  csbeq1a  3195  ssdifeq0  3646  pofun  4453  opabbi2dv  4955  fresin  5545  fresaunres2  5548  f1imacnv  5624  foimacnv  5625  funfv  5722  dffv2  5728  fsn2  5840  fnexALT  5894  funiunfvf  5928  fcof1o  5958  f1opw2  6230  fparlem3  6380  fparlem4  6381  riotaxfrd  6510  seqomlem1  6636  seqomlem4  6639  oasuc  6697  oesuclem  6698  omsuc  6699  onasuc  6701  onmsuc  6702  eqerlem  6866  pmresg  6970  fopwdom  7145  sbthlem8  7153  sbthlem9  7154  fodomr  7187  domss2  7195  mapen  7200  enp1i  7272  xpfi  7307  fiint  7312  f1opwfi  7338  marypha1lem  7366  unxpwdom  7483  cantnfval2  7550  mapfien  7579  cnfcom2lem  7584  infxpenlem  7821  cdainf  7998  isf34lem3  8181  isf34lem5  8184  axdc4lem  8261  ttukeylem6  8320  rankcf  8578  tskuni  8584  gruima  8603  dmrecnq  8771  ltexnq  8778  reclem3pr  8852  pn0sr  8902  mulgt0sr  8906  recdiv  9645  max0sub  10707  rexmul  10775  xmulmnf1  10780  xmulm1  10785  prunioo  10950  fseq1p1m1  11045  fzshftral  11057  seqp1i  11259  seqf1olem2  11283  seqfeq4  11292  binom3  11420  expmulnbnd  11431  discr  11436  bcn2  11530  hashun2  11577  hashun3  11578  hashdif  11598  hashgt12el  11602  hashgt12el2  11603  hashfacen  11623  wrdeqs1cat  11709  s2prop  11781  s4prop  11782  cnrecnv  11890  rddif  12064  amgm2  12093  rlimres  12272  lo1res  12273  iseraltlem2  12396  iseralt  12398  fsumss  12439  fsumcl2lem  12445  isumclim3  12463  fsumcnv  12477  fsumtscopo  12501  fsumiun  12520  arisum2  12560  geoisum1c  12577  sinhval  12675  cos01bnd  12707  ruclem6  12754  sqr2irrlem  12767  sadadd2lem2  12882  eucalgval  12993  pcid  13166  prmreclem4  13207  4sqlem15  13247  4sqlem16  13248  ramcl  13317  strfv2d  13419  setsid  13428  imasvscafn  13682  xpsc0  13705  xpsc1  13706  xpsff1o  13713  xpsaddlem  13720  xpsvsca  13724  xpsle  13726  mreexexlem2d  13790  mreexexlem4d  13792  sscres  13943  xpcid  14206  evlfcllem  14238  hofcl  14276  isacs5lem  14515  frmdup3  14731  cayleylem2  15031  pgp0  15150  sylow3lem2  15182  lsmdisjr  15236  lsmdisj2r  15237  subgdisj2  15244  efgval  15269  frgpuplem  15324  frgpup2  15328  gsumval3  15434  gsumzres  15437  gsum2d2lem  15467  dprdf1  15511  dmdprdsplit2lem  15523  dmdprdsplit2  15524  ablfaclem3  15565  prdsmgp  15636  unitgrp  15692  crng2idl  16230  psrass1lem  16362  gsumfsum  16682  zrhval  16705  zlmval  16713  chrid  16724  znleval  16751  ocv1  16822  baspartn  16935  mretopd  17072  ordtcld1  17176  ordtcld2  17177  leordtvallem1  17189  leordtvallem2  17190  paste  17273  imacmp  17375  cmpsub  17378  uncon  17406  1stckgen  17500  ptbasfi  17527  txcld  17549  ptclsg  17561  txdis1cn  17581  ptrescn  17585  hausdiag  17591  txkgen  17598  xkoptsub  17600  xkococnlem  17605  cnmpt21  17617  cnmpt22  17620  tgqtop  17658  qtoprest  17663  kqdisj  17678  hmeores  17717  hmphindis  17743  pt1hmeo  17752  ptuncnv  17753  ptunhmeo  17754  xpstopnlem1  17755  xkohmeo  17761  alexsublem  17989  ptcmplem2  17998  tmdcn2  18033  cldsubg  18054  divstgplem  18064  tsmsres  18087  ustbas2  18169  ressuss  18207  metreslem  18293  xpsdsval  18312  prdsxmslem2  18442  txmetcnp  18460  tngngp  18559  remetdval  18684  cnheibor  18844  evth2  18849  pcoass  18913  iscmet3  19110  minveclem2  19187  cmmbl  19289  nulmbl2  19291  volinun  19300  voliunlem1  19304  volsup  19310  ovolioo  19322  uniiccdif  19330  uniioombllem2  19335  uniioombllem3  19337  uniioombllem4  19338  uniioombllem5  19339  ismbf3d  19406  itg2uba  19495  itg2i1fseq  19507  itgsplitioo  19589  limcflf  19628  cnplimc  19634  limcun  19642  dvfval  19644  dvres  19658  dvres3a  19661  dvnp1  19671  dvn1  19672  dvexp3  19722  dvsincos  19725  mvth  19736  c1lip2  19742  dvfsumlem2  19771  itgsubstlem  19792  itgsubst  19793  evl1var  19812  pf1mpf  19832  pf1ind  19835  deg1val  19879  coeeq2  20021  dgreq0  20043  dgrcolem2  20052  vieta1  20089  ulm2  20161  radcnv0  20192  abelthlem2  20208  tanarg  20374  advlogexp  20406  efopn  20409  logtayl  20411  cxpcn3  20492  ang180lem3  20513  quad2  20539  mcubic  20547  binom4  20550  dquart  20553  quart1lem  20555  quart1  20556  quartlem1  20557  asinlem3a  20570  efiatan  20612  tanatan  20619  atanbndlem  20625  dvatan  20635  ftalem3  20717  ftalem5  20719  basellem3  20725  mumullem2  20823  musum  20836  chtublem  20855  perfectlem2  20874  bposlem6  20933  bposlem9  20936  1lgs  20981  lgs1  20982  lgseisenlem1  20993  lgseisenlem2  20994  lgseisenlem3  20995  lgsquadlem2  20999  lgsquad2lem2  21003  2sqblem  21021  rpvmasum2  21066  log2sumbnd  21098  vdgrun  21513  vdgrfiun  21514  nvpi  21996  nvop  22007  phop  22160  minvecolem2  22218  hi01  22439  pjchi  22775  chjidm  22863  mayete3i  23071  mayete3iOLD  23072  ho0val  23094  lnop0  23310  adjbdlnb  23428  pjin2i  23537  mdslmd3i  23676  mdexchi  23679  imadifxp  23874  fimacnvinrn  23883  fmptpr  23897  iocinif  23973  difioo  23974  ofldchr  24063  logb2aval  24180  indf1ofs  24212  hasheuni  24264  esumcvg2  24266  measxun2  24351  measunl  24357  measinblem  24361  probdif  24450  cndprobval  24463  ballotlemic  24536  subfacp1lem1  24637  subfacp1lem3  24640  subfacp1lem5  24642  cvmscld  24732  cvmlift2lem9a  24762  cvmlift2lem9  24770  relexpadd  24910  fprodss  25046  fprodser  25047  fprodcl2lem  25048  fprodsplit  25061  fprodn0  25075  iprodclim3  25078  risefac1  25108  fallfac1  25109  nofulllem5  25377  bpolyval  25802  bpoly3  25811  bpoly4  25812  fsumcube  25813  voliunnfl  25948  volsupnfl  25949  itg2addnclem2  25951  itg2addnc  25952  itgaddnclem2  25957  dvreacos  25974  areacirclem6  25980  cocnv  26111  istotbnd3  26164  ssbnd  26181  diophin  26515  monotuz  26688  monotoddzzfi  26689  oddcomabszz  26691  fnwe2val  26808  lnmlmic  26848  ellspd  26916  f1omvdco2  27053  symggen  27073  psgnunilem1  27078  mamuvs2  27126  fiuneneq  27175  cytpval  27190  stoweidlem50  27460  bnj1415  28738  osumcllem9N  30129  4atexlemex2  30236  cdleme20j  30483  cdlemg47  30901  diaintclN  31224  dibintclN  31333  dihintcl  31510  lclkrlem2e  31677  lclkrlem2p  31688  lcfrlem31  31739
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2373
  Copyright terms: Public domain W3C validator