Theorem syl6eqr 1522

Description: An equality transitivity deduction.

Hypotheses

Ref	Expression
syl6eqr.1	|- (ph -> A = B)
syl6eqr.2	|- C = B

Assertion

Ref	Expression
syl6eqr	|- (ph -> A = C)

Proof of Theorem syl6eqr

Step	Hyp	Ref	Expression
1		syl6eqr.1	. 2 |- (ph -> A = B)
2		syl6eqr.2	. . 3 |- C = B
3	2	eqcomi 1476	. 2 |- B = C
4	1, 3	syl6eq 1520	1 |- (ph -> A = C)

Syntax hints:   -> wi 3   = wceq 954

This theorem is referenced by:  3eqtr4g 1528  rabbirdv 2217  opprc3 2792  relop 3270  dfimafn2 3753  rdglim2a 3941  ffnoprval 4005  fnoprval 4008  fnrnoprval 4027  fooprval 4028  oprvalex 4032  curry1 4088  elrnoprabg 4114  oa0r 4163  om1r 4167  oaabs 4242  xpmapenlem3 4484  xpmapenlem5 4486  phplem1 4494  abfii4 4544  rankuni 4678  zorn2lem1 4768  halfpq 5062  prlem934a 5117  prlem936 5135  mulcmpblnrlem 5162  recexsrlem 5192  nneo 6152  seq1val 6257  cjexpt 6760  bcpasc 6915  serzfsum 6950  fsum3 6970  fsum4 6971  iserzshft2 7052  iserzabslem 7122  isumclimtf 7139  geosum 7184  geoisum1c 7188  fsum0diag2 7202  efnn0valt 7323  efivalt 7397  sinbndt 7415  cosbndt 7416  subbas 7594  subtop 7596  cldval 7616  ntrfval 7617  clsfval 7618  ntrval 7626  clsval 7627  neifval 7664  neival 7667  lpfval 7692  lpval 7693  cnfval 7706  cnpfval 7707  ishaus 7733  metxpdval 7781  blfval 7787  blf 7796  opnfval 7809  dscmet 7870  lmfval 7877  caufval 7878  iscms 7897  metcn4i 7922  bopcnlem2 7932  grpidval 8008  grpinvfval 8016  grpdivfval 8031  isabl 8052  subgrnss 8071  addinv 8080  isring 8093  ringi 8094  vci 8119  isvclem 8148  nvop2 8179  nvvop 8180  isnvlem 8181  nvi 8185  imsval 8267  ipfval 8299  sspval 8329  isssp 8330  lnoval 8360  nmofval 8370  bloval 8386  0ofval 8392  ajfval 8413  hmoval 8414  isphg 8420  phop 8421  ipasslem11 8444  siii 8457  isbn 8468  pjthlem7 9163  hstle1t 10091  stm1add 10110  stm1add3 10112  mdslmd1lem1 10189  mdexch 10199  atord 10248  dmdbr5at 10284  cdj3lem1 10295  elghomlem1 10316  ghomgrpilem2 10320  ficli 10404  homeofval 10439  infi 10484  ist1 10494  isalg 10533  isded 10549  dedi 10550  dedalg 10556  iscat 10567  cati 10568  catded 10577  ishoma 10595  ismona 10615  isfuna 10628

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467

Copyright terms: Public domain