Theorem syl6reqr 1529

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

Ref	Expression
syl6reqr	|- (ph -> C = A)

Proof of Theorem syl6reqr

Step	Hyp	Ref	Expression
1		syl6reqr.1	. 2 |- (ph -> A = B)
2		syl6reqr.2	. . 3 |- C = B
3	2	eqcomi 1482	. 2 |- B = C
4	1, 3	syl6req 1527	1 |- (ph -> C = A)

Syntax hints:   -> wi 3   = wceq 958

This theorem is referenced by:  csbabg 2046  iftrue 2370  iffalse 2371  iin0 2745  funimacnv 3577  zfrep6 3620  dfimafn 3767  fniinfv 3772  fniunfv 3871  isoini 3906  sbthlem4 4456  sbthlem5 4457  sbthlem6 4458  mapunen 4508  aceq3 4743  cardval 4836  alephsuc2 4892  zeot 6201  iooint 6373  dfseq0 6564  climrecl 7110  oprcn 7974  opr1cn 7975  opr2cn 7976  bopcnlem3 7980  siii 8509  nlelch 9989  difeqri2 10438

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

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

Copyright terms: Public domain