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

Theorem syl5eqr 2437
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 2395 . 2  |-  A  =  B
3 syl5eqr.2 . 2  |-  ( ph  ->  B  =  C )
42, 3syl5eq 2435 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-cleq 2374
This theorem is referenced by:  3eqtr3g  2446  csbeq1a  3357  ssdifeq0  3826  pofun  4730  opabbi2dv  5065  fresin  5662  fresaunres2  5665  f1imacnv  5740  foimacnv  5741  funfv  5841  dffv2  5847  fsn2  5973  funiunfvf  6062  fcof1oinvd  6097  riotaxfrd  6188  f1opw2  6427  fnexALT  6665  fparlem3  6801  fparlem4  6802  mpt2curryd  6916  seqomlem1  7033  seqomlem4  7036  oasuc  7092  oesuclem  7093  omsuc  7094  onasuc  7096  onmsuc  7097  eqerlem  7261  pmresg  7365  fopwdom  7544  sbthlem8  7553  sbthlem9  7554  fodomr  7587  domss2  7595  mapen  7600  enp1i  7670  xpfi  7706  fiint  7712  f1opwfi  7739  mapfien  7782  marypha1lem  7808  unxpwdom  7930  cantnfval2  8001  cantnfval2OLD  8031  mapfienOLD  8051  cnfcom2lemOLD  8066  infxpenlem  8304  cdainf  8485  isf34lem3  8668  isf34lem5  8671  axdc4lem  8748  ttukeylem6  8807  rankcf  9066  tskuni  9072  gruima  9091  dmrecnq  9257  ltexnq  9264  reclem3pr  9338  pn0sr  9389  mulgt0sr  9393  recdiv  10167  max0sub  11316  rexmul  11384  xmulmnf1  11389  xmulm1  11394  prunioo  11570  fseq1p1m1  11674  fzshftral  11688  seqp1i  12026  seqf1olem2  12050  seqfeq4  12059  binom3  12189  expmulnbnd  12200  discr  12205  bcn2  12299  hashun2  12354  hashun3  12355  hashdif  12380  hashgt12el  12385  hashgt12el2  12386  hashfacen  12407  wrdeqs1cat  12611  swrdccat3a  12630  s2prop  12773  s4prop  12774  cnrecnv  13000  rddif  13175  amgm2  13204  rlimres  13383  lo1res  13384  iseraltlem2  13507  iseralt  13509  fsumss  13549  fsumcl2lem  13555  isumclim3  13576  fsumcnv  13590  telfsumo  13618  fsumiun  13637  arisum2  13674  geoisum1c  13691  fprodss  13757  fprodser  13758  fprodcl2lem  13759  fprodsplit  13772  fprodn0  13785  fprodcnv  13789  iprodclim3  13795  sinhval  13891  cos01bnd  13923  ruclem6  13970  sqr2irrlem  13983  sadadd2lem2  14102  eucalgval  14213  pcid  14398  prmreclem4  14439  4sqlem15  14479  4sqlem16  14480  ramcl  14549  strfv2d  14668  setsid  14677  imasvscafn  14944  xpsc0  14967  xpsc1  14968  xpsff1o  14975  xpsaddlem  14982  xpsvsca  14986  xpsle  14988  mreexexlem2d  15052  mreexexlem4d  15054  sscres  15229  xpcid  15575  evlfcllem  15607  hofcl  15645  isacs5lem  15916  frmdup3lem  16151  cayleylem2  16555  f1omvdco2  16590  symggen  16612  psgnunilem1  16635  pgp0  16733  sylow3lem2  16765  lsmdisjr  16819  lsmdisj2r  16820  subgdisj2  16827  efgval  16852  frgpuplem  16907  frgpup2  16911  gsumval3OLD  17025  gsumval3  17028  gsumzres  17031  gsumzresOLD  17035  gsum2d2lem  17115  dprdf1  17193  dmdprdsplit2lem  17207  dmdprdsplit2  17208  ablfaclem3  17251  prdsmgp  17372  unitgrp  17429  crng2idl  18000  psrass1lem  18142  evl1var  18485  pf1mpf  18501  pf1ind  18504  gsumfsum  18597  chrid  18657  znleval  18684  ocv1  18801  frlmip  18898  ellspd  18922  mamuvs2  18993  madurid  19231  baspartn  19540  mretopd  19679  ordtcld1  19784  ordtcld2  19785  leordtvallem1  19797  leordtvallem2  19798  paste  19881  imacmp  19983  cmpsub  19986  uncon  20015  1stckgen  20140  ptbasfi  20167  txcld  20189  ptclsg  20201  txdis1cn  20221  ptrescn  20225  hausdiag  20231  txkgen  20238  xkoptsub  20240  xkococnlem  20245  cnmpt21  20257  cnmpt22  20260  tgqtop  20298  qtoprest  20303  kqdisj  20318  hmeores  20357  hmphindis  20383  pt1hmeo  20392  ptuncnv  20393  ptunhmeo  20394  xpstopnlem1  20395  xkohmeo  20401  alexsublem  20629  ptcmplem2  20638  tmdcn2  20673  cldsubg  20694  qustgplem  20704  tsmsresOLD  20730  tsmsres  20731  ustbas2  20813  ressuss  20851  metreslem  20950  xpsdsval  20969  prdsxmslem2  21117  txmetcnp  21135  tngngp  21253  remetdval  21379  cnheibor  21540  evth2  21545  pcoass  21609  iscmet3  21817  rrxip  21907  minveclem2  21926  cmmbl  22030  nulmbl2  22032  volinun  22041  voliunlem1  22045  volsup  22051  ovolioo  22063  uniiccdif  22072  uniioombllem2  22077  uniioombllem3  22079  uniioombllem4  22080  uniioombllem5  22081  ismbf3d  22146  itg2uba  22235  itg2i1fseq  22247  itgsplitioo  22329  limcflf  22370  cnplimc  22376  limcun  22384  dvfval  22386  dvres  22400  dvres3a  22403  dvnp1  22413  dvn1  22414  dvexp3  22464  dvsincos  22467  mvth  22478  c1lip2  22484  dvfsumlem2  22513  itgsubstlem  22534  itgsubst  22535  deg1valOLD  22582  coeeq2  22724  dgreq0  22747  dgrcolem2  22756  vieta1  22793  ulm2  22865  radcnv0  22896  abelthlem2  22912  tanarg  23091  advlogexp  23123  efopn  23126  logtayl  23128  cxpcn3  23209  ang180lem3  23261  quad2  23286  mcubic  23294  binom4  23297  dquart  23300  quart1lem  23302  quart1  23303  quartlem1  23304  asinlem3a  23317  efiatan  23359  tanatan  23366  atanbndlem  23372  dvatan  23382  ftalem3  23465  ftalem5  23467  basellem3  23473  mumullem2  23571  musum  23584  chtublem  23603  perfectlem2  23622  bposlem6  23681  bposlem9  23684  1lgs  23729  lgs1  23730  lgseisenlem1  23741  lgseisenlem2  23742  lgseisenlem3  23743  lgsquadlem2  23747  lgsquad2lem2  23751  2sqblem  23769  rpvmasum2  23814  log2sumbnd  23846  opphllem3  24241  vdgrun  25022  vdgrfiun  25023  numclwwlkovf2num  25206  nvpi  25686  nvop  25697  phop  25850  minvecolem2  25908  hi01  26130  pjchi  26467  chjidm  26555  mayete3i  26763  ho0val  26785  lnop0  27001  adjbdlnb  27119  pjin2i  27228  mdslmd3i  27367  mdexchi  27370  imadifxp  27591  fcoinver  27593  fimacnvinrn  27615  padct  27695  fcobijfs  27699  ffsrn  27702  iocinif  27745  difioo  27746  gsummpt2co  27924  ofldchr  27958  fvproj  27989  indf1ofs  28174  esumpad2  28204  hasheuni  28233  esumcvg2  28235  sigapildsys  28307  measxun2  28337  measunl  28343  measinblem  28347  carsgclctunlem1  28444  carsgclctunlem3  28447  sibfof  28465  sitgclg  28467  eulerpartlemgf  28501  probdif  28542  cndprobval  28555  ballotlemic  28628  signsvtn0  28710  signstres  28715  subfacp1lem1  28812  subfacp1lem3  28815  subfacp1lem5  28817  cvmscld  28907  cvmlift2lem9a  28937  cvmlift2lem9  28945  risefac1  29321  fallfac1  29322  nofulllem5  29631  bpolyval  29964  bpoly3  29973  bpoly4  29974  fsumcube  29975  ptrest  30213  voliunnfl  30223  volsupnfl  30224  mbfresfi  30226  itg2addnclem2  30233  itg2addnclem3  30234  ftc1anclem5  30260  dvacos  30270  areacirclem5  30277  cocnv  30382  istotbnd3  30433  ssbnd  30450  diophin  30871  monotuz  31042  monotoddzzfi  31043  oddcomabszz  31045  fnwe2val  31161  lnmlmic  31200  fiuneneq  31322  cytpval  31337  radcnvrat  31363  nzprmdif  31392  binomcxplemnotnn0  31429  ioccncflimc  31854  icocncflimc  31858  stoweidlem50  31998  fourierdlem89  32144  fourierdlem90  32145  fourierdlem91  32146  fourierdlem107  32162  perfectALTVlem2  32544  logb2aval  33503  aacllem  33550  bnj1415  34441  fsumshftdOLD  35096  osumcllem9N  36101  4atexlemex2  36208  cdleme20j  36457  cdlemg47  36875  diaintclN  37198  dibintclN  37307  dihintcl  37484  lclkrlem2e  37651  lclkrlem2p  37662  lcfrlem31  37713
  Copyright terms: Public domain W3C validator