Theorem syl5eqr 2509

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

Syntax hints:   -> wi 4   = wceq 1454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-cleq 2454

This theorem is referenced by:  3eqtr3g  2518  csbeq1a  3383  ssdifeq0  3861  pofun  4789  opabbi2dv  5002  funcnvpr  5657  funcnvtp  5658  funcnvqp  5659  fresin  5774  fresaunres2  5777  f1imacnv  5852  foimacnv  5853  funfv  5954  dffv2  5960  fsn2  6085  funiunfvf  6178  fcof1oinvd  6215  riotaxfrd  6306  f1opw2  6548  fnexALT  6785  fparlem3  6924  fparlem4  6925  mpt2curryd  7041  seqomlem1  7192  seqomlem4  7195  oasuc  7251  oesuclem  7252  omsuc  7253  onasuc  7255  onmsuc  7256  eqerlem  7420  pmresg  7524  fopwdom  7705  sbthlem8  7714  sbthlem9  7715  fodomr  7748  domss2  7756  mapen  7761  enp1i  7831  xpfi  7867  fiint  7873  f1opwfi  7903  mapfien  7946  marypha1lem  7972  unxpwdom  8129  cantnfval2  8199  infxpenlem  8469  cdainf  8647  isf34lem3  8830  isf34lem5  8833  axdc4lem  8910  ttukeylem6  8969  rankcf  9227  tskuni  9233  gruima  9252  dmrecnq  9418  ltexnq  9425  reclem3pr  9499  pn0sr  9550  mulgt0sr  9554  recdiv  10340  max0sub  11517  rexmul  11585  xmulmnf1  11590  xmulm1  11595  prunioo  11789  fseq1p1m1  11896  fzshftral  11910  seqp1i  12260  seqf1olem2  12284  seqfeq4  12293  binom3  12424  expmulnbnd  12435  discr  12440  bcn2  12535  hashun2  12593  hashun3  12594  hashdif  12621  hashgt12el  12627  hashgt12el2  12628  hashfacen  12649  wrdeqs1cat  12867  swrdccat3a  12886  s2prop  13037  s4prop  13040  cnrecnv  13276  rddif  13451  amgm2  13480  rlimres  13670  lo1res  13671  iseraltlem2  13797  iseralt  13799  fsumss  13839  fsumcl2lem  13845  isumclim3  13868  fsumcnv  13882  telfsumo  13910  fsumiun  13929  arisum2  13967  geoisum1c  13984  fprodss  14050  fprodser  14051  fprodcl2lem  14052  fprodsplit  14068  fprodn0  14081  fprodcnv  14085  iprodclim3  14101  risefac1  14134  fallfac1  14135  bpolyval  14150  bpoly3  14159  bpoly4  14160  fsumcube  14161  sinhval  14256  cos01bnd  14288  ruclem6  14335  sqr2irrlem  14348  sadadd2lem2  14472  eucalgval  14589  pcid  14870  prmreclem4  14911  4sqlem15OLD  14951  4sqlem16OLD  14952  4sqlem15  14957  4sqlem16  14958  ramcl  15035  strfv2d  15203  setsid  15212  imasvscafn  15491  xpsc0  15514  xpsc1  15515  xpsff1o  15522  xpsaddlem  15529  xpsvsca  15533  xpsle  15535  mreexexlem2d  15599  mreexexlem4d  15601  sscres  15776  xpcid  16122  evlfcllem  16154  hofcl  16192  isacs5lem  16463  frmdup3lem  16698  cayleylem2  17102  f1omvdco2  17137  symggen  17159  psgnunilem1  17182  pgp0  17296  sylow3lem2  17328  lsmdisjr  17382  lsmdisj2r  17383  subgdisj2  17390  efgval  17415  frgpuplem  17470  frgpup2  17474  gsumval3  17589  gsumzres  17591  gsum2d2lem  17653  dprdf1  17714  dmdprdsplit2lem  17726  dmdprdsplit2  17727  ablfaclem3  17768  prdsmgp  17886  unitgrp  17943  crng2idl  18511  psrass1lem  18649  evl1var  18972  pf1mpf  18988  pf1ind  18991  gsumfsum  19082  chrid  19146  znleval  19173  ocv1  19290  frlmip  19384  ellspd  19408  mamuvs2  19479  madurid  19717  baspartn  20017  mretopd  20156  ordtcld1  20261  ordtcld2  20262  leordtvallem1  20274  leordtvallem2  20275  paste  20358  imacmp  20460  cmpsub  20463  uncon  20492  1stckgen  20617  ptbasfi  20644  txcld  20666  ptclsg  20678  txdis1cn  20698  ptrescn  20702  hausdiag  20708  txkgen  20715  xkoptsub  20717  xkococnlem  20722  cnmpt21  20734  cnmpt22  20737  tgqtop  20775  qtoprest  20780  kqdisj  20795  hmeores  20834  hmphindis  20860  pt1hmeo  20869  ptuncnv  20870  ptunhmeo  20871  xpstopnlem1  20872  xkohmeo  20878  alexsublem  21107  ptcmplem2  21116  tmdcn2  21152  cldsubg  21173  qustgplem  21183  tsmsres  21206  ustbas2  21288  ressuss  21326  metreslem  21425  xpsdsval  21444  prdsxmslem2  21592  txmetcnp  21610  tngngp  21710  remetdval  21855  cnheibor  22031  evth2  22036  pcoass  22103  iscmet3  22311  rrxip  22397  minveclem2  22416  minveclem2OLD  22428  cmmbl  22536  nulmbl2  22538  volinun  22547  voliunlem1  22551  volsup  22557  ovolioo  22569  uniiccdif  22583  uniioombllem2  22588  uniioombllem2OLD  22589  uniioombllem3  22591  uniioombllem4  22592  uniioombllem5  22593  ismbf3d  22658  itg2uba  22749  itg2i1fseq  22761  itgsplitioo  22843  limcflf  22884  cnplimc  22890  limcun  22898  dvfval  22900  dvres  22914  dvres3a  22917  dvnp1  22927  dvn1  22928  dvexp3  22978  dvsincos  22981  mvth  22992  c1lip2  22998  dvfsumlem2  23027  itgsubstlem  23048  itgsubst  23049  coeeq2  23244  dgreq0  23267  dgrcolem2  23276  vieta1  23313  ulm2  23388  radcnv0  23419  abelthlem2  23435  tanarg  23616  advlogexp  23648  efopn  23651  logtayl  23653  cxpcn3  23736  ang180lem3  23788  quad2  23813  mcubic  23821  binom4  23824  dquart  23827  quart1lem  23829  quart1  23830  quartlem1  23831  asinlem3a  23844  efiatan  23886  tanatan  23893  atanbndlem  23899  dvatan  23909  ftalem3  24047  ftalem5  24049  ftalem5OLD  24051  basellem3  24057  mumullem2  24155  musum  24168  chtublem  24187  perfectlem2  24206  bposlem6  24265  bposlem9  24268  1lgs  24313  lgs1  24314  lgseisenlem1  24325  lgseisenlem2  24326  lgseisenlem3  24327  lgsquadlem2  24331  lgsquad2lem2  24335  2sqblem  24353  rpvmasum2  24398  log2sumbnd  24430  opphllem3  24839  vdgrun  25677  vdgrfiun  25678  numclwwlkovf2num  25861  nvpi  26343  nvop  26354  phop  26507  minvecolem2  26565  minvecolem2OLD  26575  hi01  26797  pjchi  27133  chjidm  27221  mayete3i  27429  ho0val  27451  lnop0  27667  adjbdlnb  27785  pjin2i  27894  mdslmd3i  28033  mdexchi  28036  imadifxp  28260  fcoinver  28262  fimacnvinrn  28283  padct  28355  fcobijfs  28359  ffsrn  28362  iocinif  28411  difioo  28412  gsummpt2co  28591  ofldchr  28625  symgfcoeu  28656  pmtrprfv2  28659  smatlem  28671  fvproj  28707  indf1ofs  28895  esumpad2  28925  hasheuni  28954  esumcvg2  28956  sigapildsys  29032  measxun2  29080  measunl  29086  measinblem  29090  carsgclctunlem1  29197  carsgclctunlem3  29200  sibfof  29221  sitgclg  29223  eulerpartlemgf  29260  probdif  29301  cndprobval  29314  ballotlemic  29387  ballotlemicOLD  29425  signsvtn0  29507  signstres  29512  bnj1415  29895  subfacp1lem1  29950  subfacp1lem3  29953  subfacp1lem5  29955  cvmscld  30044  cvmlift2lem9a  30074  cvmlift2lem9  30082  nofulllem5  30643  fwddifnp1  30980  csbpredg  31771  finxpreclem5  31831  ptrest  31983  poimirlem2  31986  poimirlem3  31987  poimirlem6  31990  poimirlem7  31991  poimirlem9  31993  poimirlem11  31995  poimirlem12  31996  poimirlem16  32000  poimirlem17  32001  poimirlem19  32003  poimirlem20  32004  poimirlem24  32008  poimirlem25  32009  poimirlem27  32011  poimirlem28  32012  poimirlem29  32013  poimirlem31  32015  voliunnfl  32028  volsupnfl  32029  mbfresfi  32031  itg2addnclem2  32038  itg2addnclem3  32039  ftc1anclem5  32065  dvacos  32073  areacirclem5  32080  cocnv  32096  istotbnd3  32147  ssbnd  32164  fsumshftdOLD  32568  osumcllem9N  33573  4atexlemex2  33680  cdleme20j  33929  cdlemg47  34347  diaintclN  34670  dibintclN  34779  dihintcl  34956  lclkrlem2e  35123  lclkrlem2p  35134  lcfrlem31  35185  diophin  35659  monotuz  35833  monotoddzzfi  35834  oddcomabszz  35836  fnwe2val  35951  lnmlmic  35990  fiuneneq  36115  cytpval  36130  radcnvrat  36706  nzprmdif  36711  binomcxplemnotnn0  36748  ioccncflimc  37800  icocncflimc  37804  stoweidlem50  37948  fourierdlem89  38096  fourierdlem90  38097  fourierdlem91  38098  fourierdlem107  38114  perfectALTVlem2  38881  vtxduhgrun  39587  logb2aval  40765  aacllem  40812