Theorem syl5eqr 2489

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

Step	Hyp	Ref	Expression
1		syl5eqr.1	. . 3 |- B = A
2	1	eqcomi 2447	. 2 |- A = B
3		syl5eqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5eq 2487	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436

This theorem is referenced by:  3eqtr3g  2498  csbeq1a  3309  ssdifeq0  3773  pofun  4669  opabbi2dv  5001  fresin  5592  fresaunres2  5595  f1imacnv  5669  foimacnv  5670  funfv  5770  dffv2  5776  fsn2  5895  fmptpr  5915  funiunfvf  5978  fcof1o  6009  riotaxfrd  6095  f1opw2  6325  fnexALT  6555  fparlem3  6686  fparlem4  6687  mpt2curryd  6800  seqomlem1  6917  seqomlem4  6920  oasuc  6976  oesuclem  6977  omsuc  6978  onasuc  6980  onmsuc  6981  eqerlem  7145  pmresg  7252  fopwdom  7431  sbthlem8  7440  sbthlem9  7441  fodomr  7474  domss2  7482  mapen  7487  enp1i  7559  xpfi  7595  fiint  7600  f1opwfi  7627  mapfien  7669  marypha1lem  7695  unxpwdom  7816  cantnfval2  7889  cantnfval2OLD  7919  mapfienOLD  7939  cnfcom2lemOLD  7954  infxpenlem  8192  cdainf  8373  isf34lem3  8556  isf34lem5  8559  axdc4lem  8636  ttukeylem6  8695  rankcf  8956  tskuni  8962  gruima  8981  dmrecnq  9149  ltexnq  9156  reclem3pr  9230  pn0sr  9280  mulgt0sr  9284  recdiv  10049  max0sub  11178  rexmul  11246  xmulmnf1  11251  xmulm1  11256  prunioo  11426  fseq1p1m1  11546  fzshftral  11559  seqp1i  11834  seqf1olem2  11858  seqfeq4  11867  binom3  11997  expmulnbnd  12008  discr  12013  bcn2  12107  hashun2  12158  hashun3  12159  hashdif  12180  hashgt12el  12185  hashgt12el2  12186  hashfacen  12219  wrdeqs1cat  12381  swrdccat3a  12397  s2prop  12536  s4prop  12537  cnrecnv  12666  rddif  12840  amgm2  12869  rlimres  13048  lo1res  13049  iseraltlem2  13172  iseralt  13174  fsumss  13214  fsumcl2lem  13220  isumclim3  13238  fsumcnv  13252  fsumtscopo  13277  fsumiun  13296  arisum2  13335  geoisum1c  13352  sinhval  13450  cos01bnd  13482  ruclem6  13529  sqr2irrlem  13542  sadadd2lem2  13658  eucalgval  13769  pcid  13951  prmreclem4  13992  4sqlem15  14032  4sqlem16  14033  ramcl  14102  strfv2d  14218  setsid  14227  imasvscafn  14487  xpsc0  14510  xpsc1  14511  xpsff1o  14518  xpsaddlem  14525  xpsvsca  14529  xpsle  14531  mreexexlem2d  14595  mreexexlem4d  14597  sscres  14748  xpcid  15011  evlfcllem  15043  hofcl  15081  isacs5lem  15351  frmdup3  15556  cayleylem2  15930  f1omvdco2  15966  symggen  15988  psgnunilem1  16011  pgp0  16107  sylow3lem2  16139  lsmdisjr  16193  lsmdisj2r  16194  subgdisj2  16201  efgval  16226  frgpuplem  16281  frgpup2  16285  gsumval3OLD  16394  gsumval3  16397  gsumzres  16400  gsumzresOLD  16404  gsum2d2lem  16477  dprdf1  16542  dmdprdsplit2lem  16556  dmdprdsplit2  16557  ablfaclem3  16600  prdsmgp  16714  unitgrp  16771  crng2idl  17333  psrass1lem  17459  evl1var  17782  pf1mpf  17798  pf1ind  17801  gsumfsum  17891  chrid  17970  znleval  17999  ocv1  18116  frlmip  18215  ellspd  18242  ellspdOLD  18243  mamuvs2  18322  madurid  18462  baspartn  18571  mretopd  18708  ordtcld1  18813  ordtcld2  18814  leordtvallem1  18826  leordtvallem2  18827  paste  18910  imacmp  19012  cmpsub  19015  uncon  19045  1stckgen  19139  ptbasfi  19166  txcld  19188  ptclsg  19200  txdis1cn  19220  ptrescn  19224  hausdiag  19230  txkgen  19237  xkoptsub  19239  xkococnlem  19244  cnmpt21  19256  cnmpt22  19259  tgqtop  19297  qtoprest  19302  kqdisj  19317  hmeores  19356  hmphindis  19382  pt1hmeo  19391  ptuncnv  19392  ptunhmeo  19393  xpstopnlem1  19394  xkohmeo  19400  alexsublem  19628  ptcmplem2  19637  tmdcn2  19672  cldsubg  19693  divstgplem  19703  tsmsresOLD  19729  tsmsres  19730  ustbas2  19812  ressuss  19850  metreslem  19949  xpsdsval  19968  prdsxmslem2  20116  txmetcnp  20134  tngngp  20252  remetdval  20378  cnheibor  20539  evth2  20544  pcoass  20608  iscmet3  20816  rrxip  20906  minveclem2  20925  cmmbl  21028  nulmbl2  21030  volinun  21039  voliunlem1  21043  volsup  21049  ovolioo  21061  uniiccdif  21070  uniioombllem2  21075  uniioombllem3  21077  uniioombllem4  21078  uniioombllem5  21079  ismbf3d  21144  itg2uba  21233  itg2i1fseq  21245  itgsplitioo  21327  limcflf  21368  cnplimc  21374  limcun  21382  dvfval  21384  dvres  21398  dvres3a  21401  dvnp1  21411  dvn1  21412  dvexp3  21462  dvsincos  21465  mvth  21476  c1lip2  21482  dvfsumlem2  21511  itgsubstlem  21532  itgsubst  21533  deg1valOLD  21580  coeeq2  21722  dgreq0  21744  dgrcolem2  21753  vieta1  21790  ulm2  21862  radcnv0  21893  abelthlem2  21909  tanarg  22080  advlogexp  22112  efopn  22115  logtayl  22117  cxpcn3  22198  ang180lem3  22219  quad2  22246  mcubic  22254  binom4  22257  dquart  22260  quart1lem  22262  quart1  22263  quartlem1  22264  asinlem3a  22277  efiatan  22319  tanatan  22326  atanbndlem  22332  dvatan  22342  ftalem3  22424  ftalem5  22426  basellem3  22432  mumullem2  22530  musum  22543  chtublem  22562  perfectlem2  22581  bposlem6  22640  bposlem9  22643  1lgs  22688  lgs1  22689  lgseisenlem1  22700  lgseisenlem2  22701  lgseisenlem3  22702  lgsquadlem2  22706  lgsquad2lem2  22710  2sqblem  22728  rpvmasum2  22773  log2sumbnd  22805  vdgrun  23583  vdgrfiun  23584  nvpi  24066  nvop  24077  phop  24230  minvecolem2  24288  hi01  24510  pjchi  24847  chjidm  24935  mayete3i  25143  mayete3iOLD  25144  ho0val  25166  lnop0  25382  adjbdlnb  25500  pjin2i  25609  mdslmd3i  25748  mdexchi  25751  imadifxp  25951  fimacnvinrn  25964  fcobijfs  26038  ffsrn  26041  iocinif  26083  difioo  26084  gsummpt2co  26261  ofldchr  26294  logb2aval  26464  indf1ofs  26494  hasheuni  26546  esumcvg2  26548  measxun2  26636  measunl  26642  measinblem  26646  sibfof  26738  sitgclg  26740  eulerpartlems  26755  eulerpartlemgf  26774  probdif  26815  cndprobval  26828  ballotlemic  26901  signstres  26988  subfacp1lem1  27079  subfacp1lem3  27082  subfacp1lem5  27084  cvmscld  27174  cvmlift2lem9a  27204  cvmlift2lem9  27212  relexpadd  27352  fprodss  27473  fprodser  27474  fprodcl2lem  27475  fprodsplit  27488  fprodn0  27502  fprodcnv  27506  iprodclim3  27512  risefac1  27548  fallfac1  27549  nofulllem5  27859  bpolyval  28204  bpoly3  28213  bpoly4  28214  fsumcube  28215  ptrest  28437  voliunnfl  28447  volsupnfl  28448  mbfresfi  28450  itg2addnclem2  28456  itg2addnclem3  28457  ftc1anclem5  28483  dvacos  28493  areacirclem5  28500  cocnv  28631  istotbnd3  28682  ssbnd  28699  diophin  29123  monotuz  29294  monotoddzzfi  29295  oddcomabszz  29297  fnwe2val  29414  lnmlmic  29453  fiuneneq  29574  cytpval  29589  stoweidlem50  29857  numclwwlkovf2num  30690  bnj1415  32041  fsumshftdOLD  32615  osumcllem9N  33620  4atexlemex2  33727  cdleme20j  33974  cdlemg47  34392  diaintclN  34715  dibintclN  34824  dihintcl  35001  lclkrlem2e  35168  lclkrlem2p  35179  lcfrlem31  35230