Theorem syl5eqr 1513

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

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  3eqtr3g 1522  csbeq1a 1996  uneqin 2246  reuunixfr 2896  fnex 3593  f1ocnv 3686  f1imacnv 3690  funfv 3755  fsn2 3821  funiunfv 3851  funiunfvf 3855  2ndconst 4081  sbcopeq1a 4095  csbopeq1a 4096  dfoprab4 4100  oasuc 4147  omsuc 4149  oesuc 4150  pw2en 4426  sbthlem8 4434  sbthlem9 4435  fodomr 4463  fiint 4534  inf3lem7 4591  fodom 4770  prlem934a 5109  reclem3pr 5130  pn0sr 5182  mulgt0sr 5186  supsrlem2 5198  addge0 5573  addgegt0 5574  add20 5576  mulge0 5581  recdivt 5746  prodgt0 5775  shftidt 6292  fzshftralt 6454  sqrcl 6630  sqrge0 6632  rimul 6675  rereb 6715  bcpasc 6907  fsumserz2 6941  fsump1 6944  fsumshft 6969  iserzabslem 7114  isumval2t 7130  isumclim4t 7136  isumshft 7139  isumshft2 7140  geoisum1c 7180  ivthlem8 7223  ivthlem8OLD 7232  eirrlem5 7334  cos01bndlem3 7413  acdc3lem 7428  acdclem 7436  cnconst 7719  remetdval 7847  nvpi 8233  nvop 8244  phop 8408  ubthlem6 8465  hi01t 8883  pjch 9180  chjidmt 9358  mayete3 9590  ho0valt 9593  lnop0t 9806  pjin2 10031  mdslmd3 10167  mdexch 10170  f2imacnv 10370  filintf 10443  ishomb 10560  isfuna 10592

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

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

Copyright terms: Public domain