Theorem syl5eqr 2471

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

Syntax hints:   -> wi 4   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-cleq 2416

This theorem is referenced by:  3eqtr3g  2480  csbeq1a  3342  ssdifeq0  3818  pofun  4728  opabbi2dv  4941  fresin  5707  fresaunres2  5710  f1imacnv  5785  foimacnv  5786  funfv  5887  dffv2  5893  fsn2  6016  funiunfvf  6108  fcof1oinvd  6145  riotaxfrd  6236  f1opw2  6475  fnexALT  6712  fparlem3  6848  fparlem4  6849  mpt2curryd  6966  seqomlem1  7117  seqomlem4  7120  oasuc  7176  oesuclem  7177  omsuc  7178  onasuc  7180  onmsuc  7181  eqerlem  7345  pmresg  7449  fopwdom  7628  sbthlem8  7637  sbthlem9  7638  fodomr  7671  domss2  7679  mapen  7684  enp1i  7754  xpfi  7790  fiint  7796  f1opwfi  7826  mapfien  7869  marypha1lem  7895  unxpwdom  8052  cantnfval2  8121  infxpenlem  8391  cdainf  8568  isf34lem3  8751  isf34lem5  8754  axdc4lem  8831  ttukeylem6  8890  rankcf  9148  tskuni  9154  gruima  9173  dmrecnq  9339  ltexnq  9346  reclem3pr  9420  pn0sr  9471  mulgt0sr  9475  recdiv  10259  max0sub  11435  rexmul  11503  xmulmnf1  11508  xmulm1  11513  prunioo  11707  fseq1p1m1  11814  fzshftral  11828  seqp1i  12174  seqf1olem2  12198  seqfeq4  12207  binom3  12338  expmulnbnd  12349  discr  12354  bcn2  12449  hashun2  12507  hashun3  12508  hashdif  12533  hashgt12el  12538  hashgt12el2  12539  hashfacen  12560  wrdeqs1cat  12772  swrdccat3a  12791  s2prop  12938  s4prop  12939  cnrecnv  13167  rddif  13342  amgm2  13371  rlimres  13560  lo1res  13561  iseraltlem2  13687  iseralt  13689  fsumss  13729  fsumcl2lem  13735  isumclim3  13758  fsumcnv  13772  telfsumo  13800  fsumiun  13819  arisum2  13857  geoisum1c  13874  fprodss  13940  fprodser  13941  fprodcl2lem  13942  fprodsplit  13958  fprodn0  13971  fprodcnv  13975  iprodclim3  13991  risefac1  14024  fallfac1  14025  bpolyval  14040  bpoly3  14049  bpoly4  14050  fsumcube  14051  sinhval  14146  cos01bnd  14178  ruclem6  14225  sqr2irrlem  14238  sadadd2lem2  14362  eucalgval  14479  pcid  14760  prmreclem4  14801  4sqlem15OLD  14841  4sqlem16OLD  14842  4sqlem15  14847  4sqlem16  14848  ramcl  14925  strfv2d  15093  setsid  15102  imasvscafn  15381  xpsc0  15404  xpsc1  15405  xpsff1o  15412  xpsaddlem  15419  xpsvsca  15423  xpsle  15425  mreexexlem2d  15489  mreexexlem4d  15491  sscres  15666  xpcid  16012  evlfcllem  16044  hofcl  16082  isacs5lem  16353  frmdup3lem  16588  cayleylem2  16992  f1omvdco2  17027  symggen  17049  psgnunilem1  17072  pgp0  17186  sylow3lem2  17218  lsmdisjr  17272  lsmdisj2r  17273  subgdisj2  17280  efgval  17305  frgpuplem  17360  frgpup2  17364  gsumval3  17479  gsumzres  17481  gsum2d2lem  17543  dprdf1  17604  dmdprdsplit2lem  17616  dmdprdsplit2  17617  ablfaclem3  17658  prdsmgp  17776  unitgrp  17833  crng2idl  18401  psrass1lem  18539  evl1var  18862  pf1mpf  18878  pf1ind  18881  gsumfsum  18972  chrid  19035  znleval  19062  ocv1  19179  frlmip  19273  ellspd  19297  mamuvs2  19368  madurid  19606  baspartn  19906  mretopd  20045  ordtcld1  20150  ordtcld2  20151  leordtvallem1  20163  leordtvallem2  20164  paste  20247  imacmp  20349  cmpsub  20352  uncon  20381  1stckgen  20506  ptbasfi  20533  txcld  20555  ptclsg  20567  txdis1cn  20587  ptrescn  20591  hausdiag  20597  txkgen  20604  xkoptsub  20606  xkococnlem  20611  cnmpt21  20623  cnmpt22  20626  tgqtop  20664  qtoprest  20669  kqdisj  20684  hmeores  20723  hmphindis  20749  pt1hmeo  20758  ptuncnv  20759  ptunhmeo  20760  xpstopnlem1  20761  xkohmeo  20767  alexsublem  20996  ptcmplem2  21005  tmdcn2  21041  cldsubg  21062  qustgplem  21072  tsmsres  21095  ustbas2  21177  ressuss  21215  metreslem  21314  xpsdsval  21333  prdsxmslem2  21481  txmetcnp  21499  tngngp  21599  remetdval  21744  cnheibor  21920  evth2  21925  pcoass  21992  iscmet3  22200  rrxip  22286  minveclem2  22305  minveclem2OLD  22317  cmmbl  22425  nulmbl2  22427  volinun  22436  voliunlem1  22440  volsup  22446  ovolioo  22458  uniiccdif  22472  uniioombllem2  22477  uniioombllem2OLD  22478  uniioombllem3  22480  uniioombllem4  22481  uniioombllem5  22482  ismbf3d  22547  itg2uba  22638  itg2i1fseq  22650  itgsplitioo  22732  limcflf  22773  cnplimc  22779  limcun  22787  dvfval  22789  dvres  22803  dvres3a  22806  dvnp1  22816  dvn1  22817  dvexp3  22867  dvsincos  22870  mvth  22881  c1lip2  22887  dvfsumlem2  22916  itgsubstlem  22937  itgsubst  22938  coeeq2  23133  dgreq0  23156  dgrcolem2  23165  vieta1  23202  ulm2  23277  radcnv0  23308  abelthlem2  23324  tanarg  23505  advlogexp  23537  efopn  23540  logtayl  23542  cxpcn3  23625  ang180lem3  23677  quad2  23702  mcubic  23710  binom4  23713  dquart  23716  quart1lem  23718  quart1  23719  quartlem1  23720  asinlem3a  23733  efiatan  23775  tanatan  23782  atanbndlem  23788  dvatan  23798  ftalem3  23936  ftalem5  23938  ftalem5OLD  23940  basellem3  23946  mumullem2  24044  musum  24057  chtublem  24076  perfectlem2  24095  bposlem6  24154  bposlem9  24157  1lgs  24202  lgs1  24203  lgseisenlem1  24214  lgseisenlem2  24215  lgseisenlem3  24216  lgsquadlem2  24220  lgsquad2lem2  24224  2sqblem  24242  rpvmasum2  24287  log2sumbnd  24319  opphllem3  24728  vdgrun  25566  vdgrfiun  25567  numclwwlkovf2num  25750  nvpi  26232  nvop  26243  phop  26396  minvecolem2  26454  minvecolem2OLD  26464  hi01  26686  pjchi  27022  chjidm  27110  mayete3i  27318  ho0val  27340  lnop0  27556  adjbdlnb  27674  pjin2i  27783  mdslmd3i  27922  mdexchi  27925  imadifxp  28153  fcoinver  28155  fimacnvinrn  28176  padct  28252  fcobijfs  28256  ffsrn  28259  iocinif  28308  difioo  28309  gsummpt2co  28489  ofldchr  28524  symgfcoeu  28555  pmtrprfv2  28558  smatlem  28570  fvproj  28606  indf1ofs  28794  esumpad2  28824  hasheuni  28853  esumcvg2  28855  sigapildsys  28931  measxun2  28979  measunl  28985  measinblem  28989  carsgclctunlem1  29096  carsgclctunlem3  29099  sibfof  29120  sitgclg  29122  eulerpartlemgf  29159  probdif  29200  cndprobval  29213  ballotlemic  29286  ballotlemicOLD  29324  signsvtn0  29406  signstres  29411  bnj1415  29794  subfacp1lem1  29849  subfacp1lem3  29852  subfacp1lem5  29854  cvmscld  29943  cvmlift2lem9a  29973  cvmlift2lem9  29981  nofulllem5  30539  fwddifnp1  30876  csbpredg  31634  finxpreclem5  31694  ptrest  31846  poimirlem2  31849  poimirlem3  31850  poimirlem6  31853  poimirlem7  31854  poimirlem9  31856  poimirlem11  31858  poimirlem12  31859  poimirlem16  31863  poimirlem17  31864  poimirlem19  31866  poimirlem20  31867  poimirlem24  31871  poimirlem25  31872  poimirlem27  31874  poimirlem28  31875  poimirlem29  31876  poimirlem31  31878  voliunnfl  31891  volsupnfl  31892  mbfresfi  31894  itg2addnclem2  31901  itg2addnclem3  31902  ftc1anclem5  31928  dvacos  31936  areacirclem5  31943  cocnv  31959  istotbnd3  32010  ssbnd  32027  fsumshftdOLD  32436  osumcllem9N  33441  4atexlemex2  33548  cdleme20j  33797  cdlemg47  34215  diaintclN  34538  dibintclN  34647  dihintcl  34824  lclkrlem2e  34991  lclkrlem2p  35002  lcfrlem31  35053  diophin  35527  monotuz  35702  monotoddzzfi  35703  oddcomabszz  35705  fnwe2val  35820  lnmlmic  35859  fiuneneq  35984  cytpval  35999  radcnvrat  36576  nzprmdif  36581  binomcxplemnotnn0  36618  ioccncflimc  37646  icocncflimc  37650  stoweidlem50  37794  fourierdlem89  37942  fourierdlem90  37943  fourierdlem91  37944  fourierdlem107  37960  perfectALTVlem2  38657  logb2aval  40086  aacllem  40133