Theorem syl6reqr 1526

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

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  csbabg 2043  iftrue 2366  iffalse 2367  iin0 2740  funimacnv 3571  zfrep6 3614  dfimafn 3761  fniinfv 3766  fniunfv 3865  isoini 3900  sbthlem4 4450  sbthlem5 4451  sbthlem6 4452  mapunen 4502  aceq3 4733  cardval 4826  alephsuc2 4881  zeot 6199  iooint 6372  dfseq0 6563  climrecl 7110  oprcn 7977  opr1cn 7978  opr2cn 7979  bopcnlem3 7983  siii 8513  nlelch 9994  difeqri2 10443

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