Theorem syl5reqr 1943

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

Syntax hints:   -> wi 3   = wceq 1298

This theorem is referenced by:  bm2.5ii 3887  coi2 4414  fnimaOLD 4531  foima 4622  f1imacnv 4656  f1o00 4668  oaabs 5309  mapsn 5404  sbthlem4 5513  sbthlem6 5515  pm54.43 5662  rankxplim3 5825  rankxpsuc 5826  prlem934a 6289  discrlem3 7908  fsump1i 8266  isummulc1 8473  geoseri 8496  metxp 9111  ipval3 9698  siii 9854  coskpi 10064  dif1enOLD 10173  cm2j 11196  pjssmii 11261  opsqrlem1 11711  hmopidmchlem 11722  hmopidmpji 11724  pjcmmul1i 11774  mddmd2 11881  mdexchi 11907  cvexchlem 11940  dmdbr6ati 11995  ghomfo 13634  mulgcdlem7 13762  nepss 13820  domcnvpre 14574  fprodp1i 14674  conttnf 14944  connsub 15443  isufil2 15565  ufileu 15573  pcoval2 16075  erreft2 16261  glbcon 17028  pmodl42 17312  2polss 17327

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain