Theorem syl5eqr 2484

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 2442	. 2 |- A = B
3		syl5eqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5eq 2482	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 1665  ax-4 1678  ax-ext 2407

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

This theorem is referenced by:  3eqtr3g  2493  csbeq1a  3410  ssdifeq0  3884  pofun  4791  opabbi2dv  5004  fresin  5769  fresaunres2  5772  f1imacnv  5847  foimacnv  5848  funfv  5948  dffv2  5954  fsn2  6077  funiunfvf  6169  fcof1oinvd  6206  riotaxfrd  6297  f1opw2  6536  fnexALT  6773  fparlem3  6909  fparlem4  6910  mpt2curryd  7024  seqomlem1  7175  seqomlem4  7178  oasuc  7234  oesuclem  7235  omsuc  7236  onasuc  7238  onmsuc  7239  eqerlem  7403  pmresg  7507  fopwdom  7686  sbthlem8  7695  sbthlem9  7696  fodomr  7729  domss2  7737  mapen  7742  enp1i  7812  xpfi  7848  fiint  7854  f1opwfi  7884  mapfien  7927  marypha1lem  7953  unxpwdom  8104  cantnfval2  8173  infxpenlem  8443  cdainf  8620  isf34lem3  8803  isf34lem5  8806  axdc4lem  8883  ttukeylem6  8942  rankcf  9201  tskuni  9207  gruima  9226  dmrecnq  9392  ltexnq  9399  reclem3pr  9473  pn0sr  9524  mulgt0sr  9528  recdiv  10312  max0sub  11489  rexmul  11557  xmulmnf1  11562  xmulm1  11567  prunioo  11759  fseq1p1m1  11866  fzshftral  11880  seqp1i  12226  seqf1olem2  12250  seqfeq4  12259  binom3  12390  expmulnbnd  12401  discr  12406  bcn2  12501  hashun2  12559  hashun3  12560  hashdif  12585  hashgt12el  12590  hashgt12el2  12591  hashfacen  12612  wrdeqs1cat  12816  swrdccat3a  12835  s2prop  12978  s4prop  12979  cnrecnv  13207  rddif  13382  amgm2  13411  rlimres  13600  lo1res  13601  iseraltlem2  13727  iseralt  13729  fsumss  13769  fsumcl2lem  13775  isumclim3  13798  fsumcnv  13812  telfsumo  13840  fsumiun  13859  arisum2  13897  geoisum1c  13914  fprodss  13980  fprodser  13981  fprodcl2lem  13982  fprodsplit  13998  fprodn0  14011  fprodcnv  14015  iprodclim3  14031  risefac1  14064  fallfac1  14065  bpolyval  14080  bpoly3  14089  bpoly4  14090  fsumcube  14091  sinhval  14186  cos01bnd  14218  ruclem6  14265  sqr2irrlem  14278  sadadd2lem2  14398  eucalgval  14512  pcid  14776  prmreclem4  14817  4sqlem15OLD  14857  4sqlem16OLD  14858  4sqlem15  14863  4sqlem16  14864  ramcl  14941  strfv2d  15109  setsid  15118  imasvscafn  15385  xpsc0  15408  xpsc1  15409  xpsff1o  15416  xpsaddlem  15423  xpsvsca  15427  xpsle  15429  mreexexlem2d  15493  mreexexlem4d  15495  sscres  15670  xpcid  16016  evlfcllem  16048  hofcl  16086  isacs5lem  16357  frmdup3lem  16592  cayleylem2  16996  f1omvdco2  17031  symggen  17053  psgnunilem1  17076  pgp0  17174  sylow3lem2  17206  lsmdisjr  17260  lsmdisj2r  17261  subgdisj2  17268  efgval  17293  frgpuplem  17348  frgpup2  17352  gsumval3  17467  gsumzres  17469  gsum2d2lem  17531  dprdf1  17592  dmdprdsplit2lem  17604  dmdprdsplit2  17605  ablfaclem3  17646  prdsmgp  17764  unitgrp  17821  crng2idl  18389  psrass1lem  18527  evl1var  18850  pf1mpf  18866  pf1ind  18869  gsumfsum  18960  chrid  19020  znleval  19047  ocv1  19164  frlmip  19258  ellspd  19282  mamuvs2  19353  madurid  19591  baspartn  19891  mretopd  20030  ordtcld1  20135  ordtcld2  20136  leordtvallem1  20148  leordtvallem2  20149  paste  20232  imacmp  20334  cmpsub  20337  uncon  20366  1stckgen  20491  ptbasfi  20518  txcld  20540  ptclsg  20552  txdis1cn  20572  ptrescn  20576  hausdiag  20582  txkgen  20589  xkoptsub  20591  xkococnlem  20596  cnmpt21  20608  cnmpt22  20611  tgqtop  20649  qtoprest  20654  kqdisj  20669  hmeores  20708  hmphindis  20734  pt1hmeo  20743  ptuncnv  20744  ptunhmeo  20745  xpstopnlem1  20746  xkohmeo  20752  alexsublem  20981  ptcmplem2  20990  tmdcn2  21026  cldsubg  21047  qustgplem  21057  tsmsres  21080  ustbas2  21162  ressuss  21200  metreslem  21299  xpsdsval  21318  prdsxmslem2  21466  txmetcnp  21484  tngngp  21584  remetdval  21709  cnheibor  21870  evth2  21875  pcoass  21939  iscmet3  22147  rrxip  22233  minveclem2  22252  cmmbl  22356  nulmbl2  22358  volinun  22367  voliunlem1  22371  volsup  22377  ovolioo  22389  uniiccdif  22403  uniioombllem2  22408  uniioombllem2OLD  22409  uniioombllem3  22411  uniioombllem4  22412  uniioombllem5  22413  ismbf3d  22478  itg2uba  22569  itg2i1fseq  22581  itgsplitioo  22663  limcflf  22704  cnplimc  22710  limcun  22718  dvfval  22720  dvres  22734  dvres3a  22737  dvnp1  22747  dvn1  22748  dvexp3  22798  dvsincos  22801  mvth  22812  c1lip2  22818  dvfsumlem2  22847  itgsubstlem  22868  itgsubst  22869  coeeq2  23055  dgreq0  23078  dgrcolem2  23087  vieta1  23124  ulm2  23196  radcnv0  23227  abelthlem2  23243  tanarg  23424  advlogexp  23456  efopn  23459  logtayl  23461  cxpcn3  23544  ang180lem3  23596  quad2  23621  mcubic  23629  binom4  23632  dquart  23635  quart1lem  23637  quart1  23638  quartlem1  23639  asinlem3a  23652  efiatan  23694  tanatan  23701  atanbndlem  23707  dvatan  23717  ftalem3  23855  ftalem5  23857  basellem3  23863  mumullem2  23961  musum  23974  chtublem  23993  perfectlem2  24012  bposlem6  24071  bposlem9  24074  1lgs  24119  lgs1  24120  lgseisenlem1  24131  lgseisenlem2  24132  lgseisenlem3  24133  lgsquadlem2  24137  lgsquad2lem2  24141  2sqblem  24159  rpvmasum2  24204  log2sumbnd  24236  opphllem3  24639  vdgrun  25465  vdgrfiun  25466  numclwwlkovf2num  25649  nvpi  26131  nvop  26142  phop  26295  minvecolem2  26353  hi01  26575  pjchi  26911  chjidm  26999  mayete3i  27207  ho0val  27229  lnop0  27445  adjbdlnb  27563  pjin2i  27672  mdslmd3i  27811  mdexchi  27814  imadifxp  28042  fcoinver  28044  fimacnvinrn  28066  padct  28141  fcobijfs  28145  ffsrn  28148  iocinif  28190  difioo  28191  gsummpt2co  28372  ofldchr  28407  symgfcoeu  28438  pmtrprfv2  28441  smatlem  28453  fvproj  28489  indf1ofs  28677  esumpad2  28707  hasheuni  28736  esumcvg2  28738  sigapildsys  28814  measxun2  28862  measunl  28868  measinblem  28872  carsgclctunlem1  28969  carsgclctunlem3  28972  sibfof  28992  sitgclg  28994  eulerpartlemgf  29029  probdif  29070  cndprobval  29083  ballotlemic  29156  signsvtn0  29238  signstres  29243  bnj1415  29626  subfacp1lem1  29681  subfacp1lem3  29684  subfacp1lem5  29686  cvmscld  29775  cvmlift2lem9a  29805  cvmlift2lem9  29813  nofulllem5  30371  fwddifnp1  30708  ptrest  31633  poimirlem2  31636  poimirlem3  31637  poimirlem6  31640  poimirlem7  31641  poimirlem9  31643  poimirlem11  31645  poimirlem12  31646  poimirlem16  31650  poimirlem17  31651  poimirlem19  31653  poimirlem20  31654  poimirlem24  31658  poimirlem25  31659  poimirlem27  31661  poimirlem28  31662  poimirlem29  31663  poimirlem31  31665  voliunnfl  31678  volsupnfl  31679  mbfresfi  31681  itg2addnclem2  31688  itg2addnclem3  31689  ftc1anclem5  31715  dvacos  31723  areacirclem5  31730  cocnv  31746  istotbnd3  31797  ssbnd  31814  fsumshftdOLD  32223  osumcllem9N  33228  4atexlemex2  33335  cdleme20j  33584  cdlemg47  34002  diaintclN  34325  dibintclN  34434  dihintcl  34611  lclkrlem2e  34778  lclkrlem2p  34789  lcfrlem31  34840  diophin  35314  monotuz  35485  monotoddzzfi  35486  oddcomabszz  35488  fnwe2val  35603  lnmlmic  35642  fiuneneq  35760  cytpval  35775  radcnvrat  36290  nzprmdif  36295  binomcxplemnotnn0  36332  ioccncflimc  37325  icocncflimc  37329  stoweidlem50  37470  fourierdlem89  37617  fourierdlem90  37618  fourierdlem91  37619  fourierdlem107  37635  perfectALTVlem2  38224  logb2aval  39244  aacllem  39291