Theorem syl5eqr 2522

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

Syntax hints:   -> wi 4   = wceq 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459

This theorem is referenced by:  3eqtr3g  2531  csbeq1a  3444  ssdifeq0  3909  pofun  4816  opabbi2dv  5150  fresin  5752  fresaunres2  5755  f1imacnv  5830  foimacnv  5831  funfv  5932  dffv2  5938  fsn2  6059  fmptpr  6084  funiunfvf  6147  fcof1oinvd  6182  riotaxfrd  6274  f1opw2  6510  fnexALT  6747  fparlem3  6882  fparlem4  6883  mpt2curryd  6995  seqomlem1  7112  seqomlem4  7115  oasuc  7171  oesuclem  7172  omsuc  7173  onasuc  7175  onmsuc  7176  eqerlem  7340  pmresg  7443  fopwdom  7622  sbthlem8  7631  sbthlem9  7632  fodomr  7665  domss2  7673  mapen  7678  enp1i  7751  xpfi  7787  fiint  7793  f1opwfi  7820  mapfien  7863  marypha1lem  7889  unxpwdom  8011  cantnfval2  8084  cantnfval2OLD  8114  mapfienOLD  8134  cnfcom2lemOLD  8149  infxpenlem  8387  cdainf  8568  isf34lem3  8751  isf34lem5  8754  axdc4lem  8831  ttukeylem6  8890  rankcf  9151  tskuni  9157  gruima  9176  dmrecnq  9342  ltexnq  9349  reclem3pr  9423  pn0sr  9474  mulgt0sr  9478  recdiv  10246  max0sub  11391  rexmul  11459  xmulmnf1  11464  xmulm1  11469  prunioo  11645  fseq1p1m1  11748  fzshftral  11761  seqp1i  12086  seqf1olem2  12110  seqfeq4  12119  binom3  12249  expmulnbnd  12260  discr  12265  bcn2  12359  hashun2  12413  hashun3  12414  hashdif  12435  hashgt12el  12440  hashgt12el2  12441  hashfacen  12463  wrdeqs1cat  12657  swrdccat3a  12676  s2prop  12819  s4prop  12820  cnrecnv  12955  rddif  13129  amgm2  13158  rlimres  13337  lo1res  13338  iseraltlem2  13461  iseralt  13463  fsumss  13503  fsumcl2lem  13509  isumclim3  13530  fsumcnv  13544  telfsumo  13572  fsumiun  13591  arisum2  13628  geoisum1c  13645  sinhval  13743  cos01bnd  13775  ruclem6  13822  sqr2irrlem  13835  sadadd2lem2  13952  eucalgval  14063  pcid  14248  prmreclem4  14289  4sqlem15  14329  4sqlem16  14330  ramcl  14399  strfv2d  14515  setsid  14524  imasvscafn  14785  xpsc0  14808  xpsc1  14809  xpsff1o  14816  xpsaddlem  14823  xpsvsca  14827  xpsle  14829  mreexexlem2d  14893  mreexexlem4d  14895  sscres  15046  xpcid  15309  evlfcllem  15341  hofcl  15379  isacs5lem  15649  frmdup3  15854  cayleylem2  16230  f1omvdco2  16266  symggen  16288  psgnunilem1  16311  pgp0  16409  sylow3lem2  16441  lsmdisjr  16495  lsmdisj2r  16496  subgdisj2  16503  efgval  16528  frgpuplem  16583  frgpup2  16587  gsumval3OLD  16696  gsumval3  16699  gsumzres  16702  gsumzresOLD  16706  gsum2d2lem  16789  dprdf1  16867  dmdprdsplit2lem  16881  dmdprdsplit2  16882  ablfaclem3  16925  prdsmgp  17040  unitgrp  17097  crng2idl  17666  psrass1lem  17797  evl1var  18140  pf1mpf  18156  pf1ind  18159  gsumfsum  18249  chrid  18328  znleval  18357  ocv1  18474  frlmip  18573  ellspd  18600  ellspdOLD  18601  mamuvs2  18672  madurid  18910  baspartn  19219  mretopd  19356  ordtcld1  19461  ordtcld2  19462  leordtvallem1  19474  leordtvallem2  19475  paste  19558  imacmp  19660  cmpsub  19663  uncon  19693  1stckgen  19787  ptbasfi  19814  txcld  19836  ptclsg  19848  txdis1cn  19868  ptrescn  19872  hausdiag  19878  txkgen  19885  xkoptsub  19887  xkococnlem  19892  cnmpt21  19904  cnmpt22  19907  tgqtop  19945  qtoprest  19950  kqdisj  19965  hmeores  20004  hmphindis  20030  pt1hmeo  20039  ptuncnv  20040  ptunhmeo  20041  xpstopnlem1  20042  xkohmeo  20048  alexsublem  20276  ptcmplem2  20285  tmdcn2  20320  cldsubg  20341  divstgplem  20351  tsmsresOLD  20377  tsmsres  20378  ustbas2  20460  ressuss  20498  metreslem  20597  xpsdsval  20616  prdsxmslem2  20764  txmetcnp  20782  tngngp  20900  remetdval  21026  cnheibor  21187  evth2  21192  pcoass  21256  iscmet3  21464  rrxip  21554  minveclem2  21573  cmmbl  21677  nulmbl2  21679  volinun  21688  voliunlem1  21692  volsup  21698  ovolioo  21710  uniiccdif  21719  uniioombllem2  21724  uniioombllem3  21726  uniioombllem4  21727  uniioombllem5  21728  ismbf3d  21793  itg2uba  21882  itg2i1fseq  21894  itgsplitioo  21976  limcflf  22017  cnplimc  22023  limcun  22031  dvfval  22033  dvres  22047  dvres3a  22050  dvnp1  22060  dvn1  22061  dvexp3  22111  dvsincos  22114  mvth  22125  c1lip2  22131  dvfsumlem2  22160  itgsubstlem  22181  itgsubst  22182  deg1valOLD  22229  coeeq2  22371  dgreq0  22393  dgrcolem2  22402  vieta1  22439  ulm2  22511  radcnv0  22542  abelthlem2  22558  tanarg  22729  advlogexp  22761  efopn  22764  logtayl  22766  cxpcn3  22847  ang180lem3  22868  quad2  22895  mcubic  22903  binom4  22906  dquart  22909  quart1lem  22911  quart1  22912  quartlem1  22913  asinlem3a  22926  efiatan  22968  tanatan  22975  atanbndlem  22981  dvatan  22991  ftalem3  23073  ftalem5  23075  basellem3  23081  mumullem2  23179  musum  23192  chtublem  23211  perfectlem2  23230  bposlem6  23289  bposlem9  23292  1lgs  23337  lgs1  23338  lgseisenlem1  23349  lgseisenlem2  23350  lgseisenlem3  23351  lgsquadlem2  23355  lgsquad2lem2  23359  2sqblem  23377  rpvmasum2  23422  log2sumbnd  23454  vdgrun  24574  vdgrfiun  24575  numclwwlkovf2num  24759  nvpi  25242  nvop  25253  phop  25406  minvecolem2  25464  hi01  25686  pjchi  26023  chjidm  26111  mayete3i  26319  mayete3iOLD  26320  ho0val  26342  lnop0  26558  adjbdlnb  26676  pjin2i  26785  mdslmd3i  26924  mdexchi  26927  imadifxp  27128  fcoinver  27130  fimacnvinrn  27145  fcobijfs  27218  ffsrn  27221  iocinif  27257  difioo  27258  gsummpt2co  27431  ofldchr  27464  fvproj  27495  logb2aval  27646  indf1ofs  27676  hasheuni  27728  esumcvg2  27730  measxun2  27818  measunl  27824  measinblem  27828  sibfof  27919  sitgclg  27921  eulerpartlems  27936  eulerpartlemgf  27955  probdif  27996  cndprobval  28009  ballotlemic  28082  signsvtn0  28164  signstres  28169  subfacp1lem1  28260  subfacp1lem3  28263  subfacp1lem5  28265  cvmscld  28355  cvmlift2lem9a  28385  cvmlift2lem9  28393  relexpadd  28533  fprodss  28654  fprodser  28655  fprodcl2lem  28656  fprodsplit  28669  fprodn0  28683  fprodcnv  28687  iprodclim3  28693  risefac1  28729  fallfac1  28730  nofulllem5  29040  bpolyval  29385  bpoly3  29394  bpoly4  29395  fsumcube  29396  ptrest  29623  voliunnfl  29633  volsupnfl  29634  mbfresfi  29636  itg2addnclem2  29642  itg2addnclem3  29643  ftc1anclem5  29669  dvacos  29679  areacirclem5  29686  cocnv  29817  istotbnd3  29868  ssbnd  29885  diophin  30308  monotuz  30479  monotoddzzfi  30480  oddcomabszz  30482  fnwe2val  30599  lnmlmic  30638  fiuneneq  30759  cytpval  30774  nzprmdif  30824  stoweidlem50  31350  fourierdlem81  31488  bnj1415  33173  fsumshftdOLD  33755  osumcllem9N  34760  4atexlemex2  34867  cdleme20j  35114  cdlemg47  35532  diaintclN  35855  dibintclN  35964  dihintcl  36141  lclkrlem2e  36308  lclkrlem2p  36319  lcfrlem31  36370