Theorem syl5eqr 2450

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 2408	. 2 |- A = B
3		syl5eqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5eq 2448	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1649

This theorem is referenced by:  3eqtr3g  2459  csbeq1a  3219  ssdifeq0  3670  pofun  4479  opabbi2dv  4981  fresin  5571  fresaunres2  5574  f1imacnv  5650  foimacnv  5651  funfv  5749  dffv2  5755  fsn2  5867  fnexALT  5921  funiunfvf  5955  fcof1o  5985  f1opw2  6257  fparlem3  6407  fparlem4  6408  riotaxfrd  6540  seqomlem1  6666  seqomlem4  6669  oasuc  6727  oesuclem  6728  omsuc  6729  onasuc  6731  onmsuc  6732  eqerlem  6896  pmresg  7000  fopwdom  7175  sbthlem8  7183  sbthlem9  7184  fodomr  7217  domss2  7225  mapen  7230  enp1i  7302  xpfi  7337  fiint  7342  f1opwfi  7368  marypha1lem  7396  unxpwdom  7513  cantnfval2  7580  mapfien  7609  cnfcom2lem  7614  infxpenlem  7851  cdainf  8028  isf34lem3  8211  isf34lem5  8214  axdc4lem  8291  ttukeylem6  8350  rankcf  8608  tskuni  8614  gruima  8633  dmrecnq  8801  ltexnq  8808  reclem3pr  8882  pn0sr  8932  mulgt0sr  8936  recdiv  9676  max0sub  10738  rexmul  10806  xmulmnf1  10811  xmulm1  10816  prunioo  10981  fseq1p1m1  11077  fzshftral  11089  seqp1i  11294  seqf1olem2  11318  seqfeq4  11327  binom3  11455  expmulnbnd  11466  discr  11471  bcn2  11565  hashun2  11612  hashun3  11613  hashdif  11633  hashgt12el  11637  hashgt12el2  11638  hashfacen  11658  wrdeqs1cat  11744  s2prop  11816  s4prop  11817  cnrecnv  11925  rddif  12099  amgm2  12128  rlimres  12307  lo1res  12308  iseraltlem2  12431  iseralt  12433  fsumss  12474  fsumcl2lem  12480  isumclim3  12498  fsumcnv  12512  fsumtscopo  12536  fsumiun  12555  arisum2  12595  geoisum1c  12612  sinhval  12710  cos01bnd  12742  ruclem6  12789  sqr2irrlem  12802  sadadd2lem2  12917  eucalgval  13028  pcid  13201  prmreclem4  13242  4sqlem15  13282  4sqlem16  13283  ramcl  13352  strfv2d  13454  setsid  13463  imasvscafn  13717  xpsc0  13740  xpsc1  13741  xpsff1o  13748  xpsaddlem  13755  xpsvsca  13759  xpsle  13761  mreexexlem2d  13825  mreexexlem4d  13827  sscres  13978  xpcid  14241  evlfcllem  14273  hofcl  14311  isacs5lem  14550  frmdup3  14766  cayleylem2  15066  pgp0  15185  sylow3lem2  15217  lsmdisjr  15271  lsmdisj2r  15272  subgdisj2  15279  efgval  15304  frgpuplem  15359  frgpup2  15363  gsumval3  15469  gsumzres  15472  gsum2d2lem  15502  dprdf1  15546  dmdprdsplit2lem  15558  dmdprdsplit2  15559  ablfaclem3  15600  prdsmgp  15671  unitgrp  15727  crng2idl  16265  psrass1lem  16397  gsumfsum  16721  zrhval  16744  zlmval  16752  chrid  16763  znleval  16790  ocv1  16861  baspartn  16974  mretopd  17111  ordtcld1  17215  ordtcld2  17216  leordtvallem1  17228  leordtvallem2  17229  paste  17312  imacmp  17414  cmpsub  17417  uncon  17445  1stckgen  17539  ptbasfi  17566  txcld  17588  ptclsg  17600  txdis1cn  17620  ptrescn  17624  hausdiag  17630  txkgen  17637  xkoptsub  17639  xkococnlem  17644  cnmpt21  17656  cnmpt22  17659  tgqtop  17697  qtoprest  17702  kqdisj  17717  hmeores  17756  hmphindis  17782  pt1hmeo  17791  ptuncnv  17792  ptunhmeo  17793  xpstopnlem1  17794  xkohmeo  17800  alexsublem  18028  ptcmplem2  18037  tmdcn2  18072  cldsubg  18093  divstgplem  18103  tsmsres  18126  ustbas2  18208  ressuss  18246  metreslem  18345  xpsdsval  18364  prdsxmslem2  18512  txmetcnp  18530  tngngp  18648  remetdval  18773  cnheibor  18933  evth2  18938  pcoass  19002  iscmet3  19199  minveclem2  19280  cmmbl  19382  nulmbl2  19384  volinun  19393  voliunlem1  19397  volsup  19403  ovolioo  19415  uniiccdif  19423  uniioombllem2  19428  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  ismbf3d  19499  itg2uba  19588  itg2i1fseq  19600  itgsplitioo  19682  limcflf  19721  cnplimc  19727  limcun  19735  dvfval  19737  dvres  19751  dvres3a  19754  dvnp1  19764  dvn1  19765  dvexp3  19815  dvsincos  19818  mvth  19829  c1lip2  19835  dvfsumlem2  19864  itgsubstlem  19885  itgsubst  19886  evl1var  19905  pf1mpf  19925  pf1ind  19928  deg1val  19972  coeeq2  20114  dgreq0  20136  dgrcolem2  20145  vieta1  20182  ulm2  20254  radcnv0  20285  abelthlem2  20301  tanarg  20467  advlogexp  20499  efopn  20502  logtayl  20504  cxpcn3  20585  ang180lem3  20606  quad2  20632  mcubic  20640  binom4  20643  dquart  20646  quart1lem  20648  quart1  20649  quartlem1  20650  asinlem3a  20663  efiatan  20705  tanatan  20712  atanbndlem  20718  dvatan  20728  ftalem3  20810  ftalem5  20812  basellem3  20818  mumullem2  20916  musum  20929  chtublem  20948  perfectlem2  20967  bposlem6  21026  bposlem9  21029  1lgs  21074  lgs1  21075  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgsquadlem2  21092  lgsquad2lem2  21096  2sqblem  21114  rpvmasum2  21159  log2sumbnd  21191  vdgrun  21625  vdgrfiun  21626  nvpi  22108  nvop  22119  phop  22272  minvecolem2  22330  hi01  22551  pjchi  22887  chjidm  22975  mayete3i  23183  mayete3iOLD  23184  ho0val  23206  lnop0  23422  adjbdlnb  23540  pjin2i  23649  mdslmd3i  23788  mdexchi  23791  imadifxp  23991  fimacnvinrn  24000  fmptpr  24015  iocinif  24097  difioo  24098  ofldchr  24197  logb2aval  24344  indf1ofs  24376  hasheuni  24428  esumcvg2  24430  measxun2  24517  measunl  24523  measinblem  24527  sibfof  24607  sitgclg  24609  probdif  24631  cndprobval  24644  ballotlemic  24717  subfacp1lem1  24818  subfacp1lem3  24821  subfacp1lem5  24823  cvmscld  24913  cvmlift2lem9a  24943  cvmlift2lem9  24951  relexpadd  25091  fprodss  25227  fprodser  25228  fprodcl2lem  25229  fprodsplit  25242  fprodn0  25256  fprodcnv  25260  iprodclim3  25266  risefac1  25299  fallfac1  25300  nofulllem5  25574  bpolyval  25999  bpoly3  26008  bpoly4  26009  fsumcube  26010  voliunnfl  26149  volsupnfl  26150  mbfresfi  26152  itg2addnclem2  26156  itg2addnclem3  26157  dvreacos  26180  areacirclem6  26186  cocnv  26317  istotbnd3  26370  ssbnd  26387  diophin  26721  monotuz  26894  monotoddzzfi  26895  oddcomabszz  26897  fnwe2val  27014  lnmlmic  27054  ellspd  27122  f1omvdco2  27259  symggen  27279  psgnunilem1  27284  mamuvs2  27332  fiuneneq  27381  cytpval  27396  stoweidlem50  27666  swrdccat3a  28030  bnj1415  29113  osumcllem9N  30446  4atexlemex2  30553  cdleme20j  30800  cdlemg47  31218  diaintclN  31541  dibintclN  31650  dihintcl  31827  lclkrlem2e  31994  lclkrlem2p  32005  lcfrlem31  32056

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 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397