Theorem syl5eqr 1521

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

Ref	Expression
syl5eqr	|- (ph -> C = B)

Proof of Theorem syl5eqr

Step	Hyp	Ref	Expression
1		syl5eqr.1	. 2 |- (ph -> A = B)
2		syl5eqr.2	. . 3 |- A = C
3	2	eqcomi 1479	. 2 |- C = A
4	1, 3	syl5eq 1519	1 |- (ph -> C = B)

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  3eqtr3g 1530  csbeq1a 2006  uneqin 2256  reuunixfr 2906  fnex 3607  f1ocnv 3701  f1imacnv 3705  funfv 3770  fsn2 3836  funiunfv 3866  funiunfvf 3870  2ndconst 4097  sbcopeq1a 4111  csbopeq1a 4112  dfoprab4 4116  oasuc 4163  omsuc 4165  oesuc 4166  pw2en 4446  sbthlem8 4454  sbthlem9 4455  fodomr 4483  fiint 4559  fiintOLD 4560  inf3lem7 4619  fodom 4798  prlem934a 5137  reclem3pr 5158  pn0sr 5210  mulgt0sr 5214  supsrlem2 5226  addge0 5599  addgegt0 5600  add20 5602  mulge0 5607  recdivt 5790  prodgt0 5819  shftidt 6355  fzshftralt 6522  sqrcl 6700  sqrge0 6702  rimul 6744  bcpasc 6969  fsumserz2 7003  fsump1 7006  fsumshft 7031  iserzabslem 7178  isumval2t 7194  isumclim4t 7201  isumshft 7204  isumshft2 7205  geoisum1c 7245  ivthlem8 7288  eirrlem5 7393  cos01bndlem3 7471  acdc3lem 7486  acdclem 7494  cnconst 7780  remetdval 7908  nvpi 8294  nvop 8305  phop 8477  ubthlem6 8534  hi01t 8962  pjch 9265  chjidmt 9443  mayete3 9673  ho0valt 9676  lnop0t 9890  pjin2 10121  mdslmd3 10259  mdexch 10262  f2imacnv 10475  filintf 10569  rcfpfillem6 10595  rcfpfillem6OLD 10596  ishomb 10716  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