Theorem syl6req 1527

Description: An equality transitivity deduction.

Hypotheses

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

Assertion

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

Proof of Theorem syl6req

Step	Hyp	Ref	Expression
1		syl6req.1	. . 3 |- (ph -> A = B)
2		syl6req.2	. . 3 |- B = C
3	1, 2	syl6eq 1526	. 2 |- (ph -> A = C)
4	3	eqcomd 1483	1 |- (ph -> C = A)

Syntax hints:   -> wi 3   = wceq 958

This theorem is referenced by:  syl6reqr 1529  reucl 2891  elxp4 3459  elxp5 3460  fvex 3738  dfopab2 4119  dfoprab3 4120  oev2 4168  odi 4216  nneob 4261  fundmen 4434  xpsnen 4441  xpcomen 4445  xpassen 4447  infeq5 4630  ine0 5446  msqge0 5626  recexpt 6596  bcpasc 6969  ser1const 7171  efcvgfsum 7315  alephsuc3 7587  ismet 7795  metssba 7806  bcthlem10 8005  grprndm 8051  vafval 8218  smfval 8220  0vfval 8221  imsba 8317  minveclem38 8578  efif1lem5 8729  hvmul0t 8888  dfchj3 9320  cmcmlem 9529  cmbr3 9538  nmcoplb 9953  nmbdfnlb 9973  nmcfnlb 9982  cnlnadjlem5 9999  nmopcoadj 10029  pjin2 10116  hst1ht 10149  ghomfo 10386  domval 10626  codval 10627  idval 10628  cmpval 10629

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