Theorem syl5reqr 1519

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

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

Proof of Theorem syl5reqr

Step	Hyp	Ref	Expression
1		syl5reqr.1	. 2 |- (ph -> A = B)
2		syl5reqr.2	. . 3 |- A = C
3	2	eqcomi 1476	. 2 |- C = A
4	1, 3	syl5req 1517	1 |- (ph -> B = C)

Syntax hints:   -> wi 3   = wceq 954

This theorem is referenced by:  bm2.5ii 3014  coi2 3503  fnima 3596  foima 3667  f1imacnv 3696  f1o00 3705  oaabs 4242  mapsn 4335  sbthlem4 4436  sbthlem6 4438  pm54.43 4552  rankxplim3 4694  rankxpsuc 4695  prlem934a 5117  discrlem3 6596  fsump1 6952  isummulc1 7155  geoser 7177  metxp 7786  ipval3 8306  siii 8457  cm2jt 9503  pjssm 9566  hmopidmchlem 10016  hmopidmpj 10018  pjcmmul1 10067  mddmd 10173  mdexch 10199  cvexchlem 10232  dmdbr6at 10285  ghomfo 10325

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