Theorem syl6eqr 1525

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 1479	. 2 |- B = C
4	1, 3	syl6eq 1523	1 |- (ph -> A = C)

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  3eqtr4g 1531  rabbirdv 2221  opprc3 2797  relop 3275  dfimafn2 3762  rdglim2a 3950  ffnoprval 4014  fnoprval 4017  fnrnoprval 4036  fooprval 4037  oprvalex 4041  curry1 4098  elrnoprabg 4124  oa0r 4173  om1r 4177  oaabs 4252  xpmapenlem3 4498  xpmapenlem5 4500  phplem1 4508  abfii4OLD 4564  rankuni 4698  zorn2lem1 4788  halfpq 5082  prlem934a 5137  prlem936 5155  mulcmpblnrlem 5182  recexsrlem 5212  nneo 6197  seq1val 6312  cjexpt 6817  bcpasc 6969  serzfsum 7004  fsum3 7024  fsum4 7025  iserzshft2 7107  iserzabslem 7178  isumclimtf 7195  geosum 7241  geoisum1c 7245  fsum0diag2 7259  efnn0valt 7373  efivalt 7447  sinbndt 7465  cosbndt 7466  subbasOLD 7644  subtop 7646  cldval 7666  ntrfval 7667  clsfval 7668  ntrval 7676  clsval 7677  neifval 7714  neival 7717  lpfval 7742  lpval 7743  cnfval 7756  cnpfval 7757  ishaus 7783  metxpdval 7829  blfval 7835  blf 7844  opnfval 7857  dscmet 7918  lmfval 7925  caufval 7926  iscms 7946  metcn4i 7972  bopcnlem2 7982  grpidval 8058  grpinvfval 8066  grpdivfval 8081  isabl 8101  subgrnss 8119  addinv 8128  isring 8141  ringi 8142  vci 8167  isvclem 8196  nvop2 8227  nvvop 8228  isnvlem 8229  nvi 8233  imsval 8316  ipfval 8352  sspval 8382  isssp 8383  lnoval 8413  nmofval 8425  bloval 8441  0ofval 8447  ajfval 8469  hmoval 8470  isphg 8476  phop 8477  ipasslem11 8500  siii 8513  isbn 8524  pjthlem7 9225  hstle1t 10153  stm1add 10172  stm1add3 10174  mdslmd1lem1 10252  mdexch 10262  atord 10311  dmdbr5at 10349  cdj3lem1 10361  elghomlem1 10382  ghomgrpilem2 10386  ficli 10472  ficliOLD 10473  homeofval 10516  infi 10578  infiOLD 10579  rcfpfillem4 10591  rcfpfillem4OLD 10592  sfvlimOLD 10606  ist1 10614  isalg 10653  isded 10669  dedi 10670  dedalg 10676  iscat 10687  cati 10688  catded 10697  ishoma 10715  ismona 10737  isepia 10747  isfuna 10754

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain