Theorem syl5reqr 1565

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

Syntax hints:   -> wi 3   = wceq 992

This theorem is referenced by:  bm2.5ii 3163  coi2 3615  fnima 3710  foima 3784  f1imacnv 3813  f1o00 3825  oaabs 4392  mapsn 4486  sbthlem4 4595  sbthlem6 4597  pm54.43 4715  rankxplim3 4860  rankxpsuc 4861  prlem934a 5291  discrlem3 6859  fsump1i 7209  isummulc1 7416  geoseri 7439  metxp 8044  ipval3 8613  siii 8769  coskpi 8982  cm2j 9839  pjssmii 9904  hmopidmchlem 10358  hmopidmpji 10360  pjcmmul1i 10410  mddmd2 10517  mdexchi 10543  cvexchlem 10576  dmdbr6ati 10632  ghomfo 10676  connsub 11502  isufil2 11650  ufileu 11658  dif1en 11833

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-cleq 1511

Copyright terms: Public domain