Theorem syl5eqr 2498

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

Syntax hints:   -> wi 4   = wceq 1383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

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

This theorem is referenced by:  3eqtr3g  2507  csbeq1a  3429  ssdifeq0  3896  pofun  4806  opabbi2dv  5142  fresin  5744  fresaunres2  5747  f1imacnv  5822  foimacnv  5823  funfv  5925  dffv2  5931  fsn2  6056  funiunfvf  6146  fcof1oinvd  6181  riotaxfrd  6273  f1opw2  6513  fnexALT  6751  fparlem3  6887  fparlem4  6888  mpt2curryd  7000  seqomlem1  7117  seqomlem4  7120  oasuc  7176  oesuclem  7177  omsuc  7178  onasuc  7180  onmsuc  7181  eqerlem  7345  pmresg  7448  fopwdom  7627  sbthlem8  7636  sbthlem9  7637  fodomr  7670  domss2  7678  mapen  7683  enp1i  7757  xpfi  7793  fiint  7799  f1opwfi  7826  mapfien  7869  marypha1lem  7895  unxpwdom  8018  cantnfval2  8091  cantnfval2OLD  8121  mapfienOLD  8141  cnfcom2lemOLD  8156  infxpenlem  8394  cdainf  8575  isf34lem3  8758  isf34lem5  8761  axdc4lem  8838  ttukeylem6  8897  rankcf  9158  tskuni  9164  gruima  9183  dmrecnq  9349  ltexnq  9356  reclem3pr  9430  pn0sr  9481  mulgt0sr  9485  recdiv  10257  max0sub  11406  rexmul  11474  xmulmnf1  11479  xmulm1  11484  prunioo  11660  fseq1p1m1  11763  fzshftral  11777  seqp1i  12105  seqf1olem2  12129  seqfeq4  12138  binom3  12269  expmulnbnd  12280  discr  12285  bcn2  12379  hashun2  12433  hashun3  12434  hashdif  12458  hashgt12el  12463  hashgt12el2  12464  hashfacen  12485  wrdeqs1cat  12682  swrdccat3a  12701  s2prop  12844  s4prop  12845  cnrecnv  12980  rddif  13155  amgm2  13184  rlimres  13363  lo1res  13364  iseraltlem2  13487  iseralt  13489  fsumss  13529  fsumcl2lem  13535  isumclim3  13556  fsumcnv  13570  telfsumo  13598  fsumiun  13617  arisum2  13654  geoisum1c  13671  fprodss  13737  fprodser  13738  fprodcl2lem  13739  fprodsplit  13752  fprodn0  13765  fprodcnv  13769  iprodclim3  13775  sinhval  13871  cos01bnd  13903  ruclem6  13950  sqr2irrlem  13963  sadadd2lem2  14082  eucalgval  14193  pcid  14378  prmreclem4  14419  4sqlem15  14459  4sqlem16  14460  ramcl  14529  strfv2d  14646  setsid  14655  imasvscafn  14916  xpsc0  14939  xpsc1  14940  xpsff1o  14947  xpsaddlem  14954  xpsvsca  14958  xpsle  14960  mreexexlem2d  15024  mreexexlem4d  15026  sscres  15174  xpcid  15437  evlfcllem  15469  hofcl  15507  isacs5lem  15778  frmdup3lem  16013  cayleylem2  16417  f1omvdco2  16452  symggen  16474  psgnunilem1  16497  pgp0  16595  sylow3lem2  16627  lsmdisjr  16681  lsmdisj2r  16682  subgdisj2  16689  efgval  16714  frgpuplem  16769  frgpup2  16773  gsumval3OLD  16887  gsumval3  16890  gsumzres  16893  gsumzresOLD  16897  gsum2d2lem  16980  dprdf1  17059  dmdprdsplit2lem  17073  dmdprdsplit2  17074  ablfaclem3  17117  prdsmgp  17238  unitgrp  17295  crng2idl  17866  psrass1lem  18008  evl1var  18351  pf1mpf  18367  pf1ind  18370  gsumfsum  18463  chrid  18542  znleval  18571  ocv1  18688  frlmip  18787  ellspd  18814  ellspdOLD  18815  mamuvs2  18886  madurid  19124  baspartn  19433  mretopd  19571  ordtcld1  19676  ordtcld2  19677  leordtvallem1  19689  leordtvallem2  19690  paste  19773  imacmp  19875  cmpsub  19878  uncon  19908  1stckgen  20033  ptbasfi  20060  txcld  20082  ptclsg  20094  txdis1cn  20114  ptrescn  20118  hausdiag  20124  txkgen  20131  xkoptsub  20133  xkococnlem  20138  cnmpt21  20150  cnmpt22  20153  tgqtop  20191  qtoprest  20196  kqdisj  20211  hmeores  20250  hmphindis  20276  pt1hmeo  20285  ptuncnv  20286  ptunhmeo  20287  xpstopnlem1  20288  xkohmeo  20294  alexsublem  20522  ptcmplem2  20531  tmdcn2  20566  cldsubg  20587  qustgplem  20597  tsmsresOLD  20623  tsmsres  20624  ustbas2  20706  ressuss  20744  metreslem  20843  xpsdsval  20862  prdsxmslem2  21010  txmetcnp  21028  tngngp  21146  remetdval  21272  cnheibor  21433  evth2  21438  pcoass  21502  iscmet3  21710  rrxip  21800  minveclem2  21819  cmmbl  21923  nulmbl2  21925  volinun  21934  voliunlem1  21938  volsup  21944  ovolioo  21956  uniiccdif  21965  uniioombllem2  21970  uniioombllem3  21972  uniioombllem4  21973  uniioombllem5  21974  ismbf3d  22039  itg2uba  22128  itg2i1fseq  22140  itgsplitioo  22222  limcflf  22263  cnplimc  22269  limcun  22277  dvfval  22279  dvres  22293  dvres3a  22296  dvnp1  22306  dvn1  22307  dvexp3  22357  dvsincos  22360  mvth  22371  c1lip2  22377  dvfsumlem2  22406  itgsubstlem  22427  itgsubst  22428  deg1valOLD  22475  coeeq2  22617  dgreq0  22640  dgrcolem2  22649  vieta1  22686  ulm2  22758  radcnv0  22789  abelthlem2  22805  tanarg  22982  advlogexp  23014  efopn  23017  logtayl  23019  cxpcn3  23100  ang180lem3  23121  quad2  23148  mcubic  23156  binom4  23159  dquart  23162  quart1lem  23164  quart1  23165  quartlem1  23166  asinlem3a  23179  efiatan  23221  tanatan  23228  atanbndlem  23234  dvatan  23244  ftalem3  23326  ftalem5  23328  basellem3  23334  mumullem2  23432  musum  23445  chtublem  23464  perfectlem2  23483  bposlem6  23542  bposlem9  23545  1lgs  23590  lgs1  23591  lgseisenlem1  23602  lgseisenlem2  23603  lgseisenlem3  23604  lgsquadlem2  23608  lgsquad2lem2  23612  2sqblem  23630  rpvmasum2  23675  log2sumbnd  23707  opphllem3  24099  vdgrun  24879  vdgrfiun  24880  numclwwlkovf2num  25063  nvpi  25547  nvop  25558  phop  25711  minvecolem2  25769  hi01  25991  pjchi  26328  chjidm  26416  mayete3i  26624  mayete3iOLD  26625  ho0val  26647  lnop0  26863  adjbdlnb  26981  pjin2i  27090  mdslmd3i  27229  mdexchi  27232  imadifxp  27436  fcoinver  27438  fimacnvinrn  27453  fcobijfs  27527  ffsrn  27530  iocinif  27570  difioo  27571  gsummpt2co  27749  ofldchr  27782  fvproj  27813  logb2aval  27987  indf1ofs  28017  hasheuni  28069  esumcvg2  28071  measxun2  28159  measunl  28165  measinblem  28169  sibfof  28260  sitgclg  28262  eulerpartlemgf  28296  probdif  28337  cndprobval  28350  ballotlemic  28423  signsvtn0  28505  signstres  28510  subfacp1lem1  28601  subfacp1lem3  28604  subfacp1lem5  28606  cvmscld  28696  cvmlift2lem9a  28726  cvmlift2lem9  28734  relexpadd  29039  risefac1  29131  fallfac1  29132  nofulllem5  29442  bpolyval  29787  bpoly3  29796  bpoly4  29797  fsumcube  29798  ptrest  30024  voliunnfl  30034  volsupnfl  30035  mbfresfi  30037  itg2addnclem2  30043  itg2addnclem3  30044  ftc1anclem5  30070  dvacos  30080  areacirclem5  30087  cocnv  30192  istotbnd3  30243  ssbnd  30260  diophin  30682  monotuz  30853  monotoddzzfi  30854  oddcomabszz  30856  fnwe2val  30971  lnmlmic  31010  fiuneneq  31130  cytpval  31145  radcnvrat  31171  nzprmdif  31200  ioccncflimc  31642  icocncflimc  31646  stoweidlem50  31786  fourierdlem89  31932  fourierdlem90  31933  fourierdlem91  31934  fourierdlem107  31950  bnj1415  33962  fsumshftdOLD  34558  osumcllem9N  35563  4atexlemex2  35670  cdleme20j  35919  cdlemg47  36337  diaintclN  36660  dibintclN  36769  dihintcl  36946  lclkrlem2e  37113  lclkrlem2p  37124  lcfrlem31  37175