Theorem syl5eqr 2487

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

Syntax hints:   -> wi 4   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434

This theorem is referenced by:  3eqtr3g  2496  csbeq1a  3294  ssdifeq0  3758  pofun  4653  opabbi2dv  4985  fresin  5577  fresaunres2  5580  f1imacnv  5654  foimacnv  5655  funfv  5755  dffv2  5761  fsn2  5880  fmptpr  5900  funiunfvf  5963  fcof1o  5994  riotaxfrd  6081  f1opw2  6312  fnexALT  6542  fparlem3  6673  fparlem4  6674  seqomlem1  6901  seqomlem4  6904  oasuc  6960  oesuclem  6961  omsuc  6962  onasuc  6964  onmsuc  6965  eqerlem  7129  pmresg  7236  fopwdom  7415  sbthlem8  7424  sbthlem9  7425  fodomr  7458  domss2  7466  mapen  7471  enp1i  7543  xpfi  7579  fiint  7584  f1opwfi  7611  mapfien  7653  marypha1lem  7679  unxpwdom  7800  cantnfval2  7873  cantnfval2OLD  7903  mapfienOLD  7923  cnfcom2lemOLD  7938  infxpenlem  8176  cdainf  8357  isf34lem3  8540  isf34lem5  8543  axdc4lem  8620  ttukeylem6  8679  rankcf  8940  tskuni  8946  gruima  8965  dmrecnq  9133  ltexnq  9140  reclem3pr  9214  pn0sr  9264  mulgt0sr  9268  recdiv  10033  max0sub  11162  rexmul  11230  xmulmnf1  11235  xmulm1  11240  prunioo  11410  fseq1p1m1  11530  fzshftral  11543  seqp1i  11818  seqf1olem2  11842  seqfeq4  11851  binom3  11981  expmulnbnd  11992  discr  11997  bcn2  12091  hashun2  12142  hashun3  12143  hashdif  12164  hashgt12el  12169  hashgt12el2  12170  hashfacen  12203  wrdeqs1cat  12365  swrdccat3a  12381  s2prop  12520  s4prop  12521  cnrecnv  12650  rddif  12824  amgm2  12853  rlimres  13032  lo1res  13033  iseraltlem2  13156  iseralt  13158  fsumss  13198  fsumcl2lem  13204  isumclim3  13222  fsumcnv  13236  fsumtscopo  13261  fsumiun  13280  arisum2  13319  geoisum1c  13336  sinhval  13434  cos01bnd  13466  ruclem6  13513  sqr2irrlem  13526  sadadd2lem2  13642  eucalgval  13753  pcid  13935  prmreclem4  13976  4sqlem15  14016  4sqlem16  14017  ramcl  14086  strfv2d  14202  setsid  14211  imasvscafn  14471  xpsc0  14494  xpsc1  14495  xpsff1o  14502  xpsaddlem  14509  xpsvsca  14513  xpsle  14515  mreexexlem2d  14579  mreexexlem4d  14581  sscres  14732  xpcid  14995  evlfcllem  15027  hofcl  15065  isacs5lem  15335  frmdup3  15537  cayleylem2  15911  f1omvdco2  15947  symggen  15969  psgnunilem1  15992  pgp0  16088  sylow3lem2  16120  lsmdisjr  16174  lsmdisj2r  16175  subgdisj2  16182  efgval  16207  frgpuplem  16262  frgpup2  16266  gsumval3OLD  16375  gsumval3  16378  gsumzres  16381  gsumzresOLD  16385  gsum2d2lem  16455  dprdf1  16520  dmdprdsplit2lem  16534  dmdprdsplit2  16535  ablfaclem3  16578  prdsmgp  16692  unitgrp  16749  crng2idl  17299  psrass1lem  17425  evl1var  17739  pf1mpf  17755  pf1ind  17758  gsumfsum  17838  chrid  17917  znleval  17946  ocv1  18063  frlmip  18162  ellspd  18189  ellspdOLD  18190  mamuvs2  18269  madurid  18409  baspartn  18518  mretopd  18655  ordtcld1  18760  ordtcld2  18761  leordtvallem1  18773  leordtvallem2  18774  paste  18857  imacmp  18959  cmpsub  18962  uncon  18992  1stckgen  19086  ptbasfi  19113  txcld  19135  ptclsg  19147  txdis1cn  19167  ptrescn  19171  hausdiag  19177  txkgen  19184  xkoptsub  19186  xkococnlem  19191  cnmpt21  19203  cnmpt22  19206  tgqtop  19244  qtoprest  19249  kqdisj  19264  hmeores  19303  hmphindis  19329  pt1hmeo  19338  ptuncnv  19339  ptunhmeo  19340  xpstopnlem1  19341  xkohmeo  19347  alexsublem  19575  ptcmplem2  19584  tmdcn2  19619  cldsubg  19640  divstgplem  19650  tsmsresOLD  19676  tsmsres  19677  ustbas2  19759  ressuss  19797  metreslem  19896  xpsdsval  19915  prdsxmslem2  20063  txmetcnp  20081  tngngp  20199  remetdval  20325  cnheibor  20486  evth2  20491  pcoass  20555  iscmet3  20763  rrxip  20853  minveclem2  20872  cmmbl  20975  nulmbl2  20977  volinun  20986  voliunlem1  20990  volsup  20996  ovolioo  21008  uniiccdif  21017  uniioombllem2  21022  uniioombllem3  21024  uniioombllem4  21025  uniioombllem5  21026  ismbf3d  21091  itg2uba  21180  itg2i1fseq  21192  itgsplitioo  21274  limcflf  21315  cnplimc  21321  limcun  21329  dvfval  21331  dvres  21345  dvres3a  21348  dvnp1  21358  dvn1  21359  dvexp3  21409  dvsincos  21412  mvth  21423  c1lip2  21429  dvfsumlem2  21458  itgsubstlem  21479  itgsubst  21480  deg1valOLD  21527  coeeq2  21669  dgreq0  21691  dgrcolem2  21700  vieta1  21737  ulm2  21809  radcnv0  21840  abelthlem2  21856  tanarg  22027  advlogexp  22059  efopn  22062  logtayl  22064  cxpcn3  22145  ang180lem3  22166  quad2  22193  mcubic  22201  binom4  22204  dquart  22207  quart1lem  22209  quart1  22210  quartlem1  22211  asinlem3a  22224  efiatan  22266  tanatan  22273  atanbndlem  22279  dvatan  22289  ftalem3  22371  ftalem5  22373  basellem3  22379  mumullem2  22477  musum  22490  chtublem  22509  perfectlem2  22528  bposlem6  22587  bposlem9  22590  1lgs  22635  lgs1  22636  lgseisenlem1  22647  lgseisenlem2  22648  lgseisenlem3  22649  lgsquadlem2  22653  lgsquad2lem2  22657  2sqblem  22675  rpvmasum2  22720  log2sumbnd  22752  vdgrun  23506  vdgrfiun  23507  nvpi  23989  nvop  24000  phop  24153  minvecolem2  24211  hi01  24433  pjchi  24770  chjidm  24858  mayete3i  25066  mayete3iOLD  25067  ho0val  25089  lnop0  25305  adjbdlnb  25423  pjin2i  25532  mdslmd3i  25671  mdexchi  25674  imadifxp  25874  fimacnvinrn  25887  fcobijfs  25961  ffsrn  25964  iocinif  26004  difioo  26005  gsummpt2co  26184  ofldchr  26217  logb2aval  26388  indf1ofs  26418  hasheuni  26470  esumcvg2  26472  measxun2  26560  measunl  26566  measinblem  26570  sibfof  26656  sitgclg  26658  eulerpartlems  26673  eulerpartlemgf  26692  probdif  26733  cndprobval  26746  ballotlemic  26819  signstres  26906  subfacp1lem1  26997  subfacp1lem3  27000  subfacp1lem5  27002  cvmscld  27092  cvmlift2lem9a  27122  cvmlift2lem9  27130  relexpadd  27269  fprodss  27390  fprodser  27391  fprodcl2lem  27392  fprodsplit  27405  fprodn0  27419  fprodcnv  27423  iprodclim3  27429  risefac1  27465  fallfac1  27466  nofulllem5  27776  bpolyval  28121  bpoly3  28130  bpoly4  28131  fsumcube  28132  ptrest  28350  voliunnfl  28360  volsupnfl  28361  mbfresfi  28363  itg2addnclem2  28369  itg2addnclem3  28370  ftc1anclem5  28396  dvacos  28406  areacirclem5  28413  cocnv  28544  istotbnd3  28595  ssbnd  28612  diophin  29036  monotuz  29207  monotoddzzfi  29208  oddcomabszz  29210  fnwe2val  29327  lnmlmic  29366  fiuneneq  29487  cytpval  29502  stoweidlem50  29770  numclwwlkovf2num  30603  bnj1415  31863  osumcllem9N  33330  4atexlemex2  33437  cdleme20j  33684  cdlemg47  34102  diaintclN  34425  dibintclN  34534  dihintcl  34711  lclkrlem2e  34878  lclkrlem2p  34889  lcfrlem31  34940