Theorem syl5reqr 1522

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

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  bm2.5ii 3019  coi2 3511  fnima 3604  foima 3676  f1imacnv 3705  f1o00 3714  oaabs 4252  mapsn 4345  sbthlem4 4450  sbthlem6 4452  pm54.43 4572  rankxplim3 4714  rankxpsuc 4715  prlem934a 5137  discrlem3 6658  fsump1 7006  isummulc1 7212  geoser 7234  metxp 7834  ipval3 8359  siii 8513  cm2jt 9563  pjssm 9626  hmopidmchlem 10078  hmopidmpj 10080  pjcmmul1 10129  mddmd 10236  mdexch 10262  cvexchlem 10295  dmdbr6at 10350  ghomfo 10391

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