Theorem syl5req 1520

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

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

Proof of Theorem syl5req

Step	Hyp	Ref	Expression
1		syl5req.1	. . 3 |- (ph -> A = B)
2		syl5req.2	. . 3 |- C = A
3	1, 2	syl5eq 1519	. 2 |- (ph -> C = B)
4	3	eqcomd 1480	1 |- (ph -> B = C)

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  syl5reqr 1522  opeqsn 2802  onfr 2986  relop 3275  funopg 3547  funcnvres 3568  xpmapenlem4 4499  unblem2 4541  pwfilemOLD 4570  kmlem2 4766  kmlem11 4775  kmlem12 4776  1idsr 5207  recextlem1 5682  quoremz 6251  intfrac 6253  intfracOLD 6254  seq0p1 6551  fsumrev 7029  efaddlem5 7342  lmsslem 7952  lmss 7953  vc2 8174  nvge0 8302  nmo0 8451  blocnilem 8464  minveclem27 8571  bcsALT 9046  pjch 9265  shjshsel 9416  spanpr 9503  pjinvar 10119  mdslmd1lem2 10253

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