Theorem syl6eqr 2403

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl6eqr.1	⊢ (φ → A = B)
syl6eqr.2	⊢ C = B

Assertion

Ref	Expression
syl6eqr	⊢ (φ → A = C)

Proof of Theorem syl6eqr

Step	Hyp	Ref	Expression
1		syl6eqr.1	. 2 ⊢ (φ → A = B)
2		syl6eqr.2	. . 3 ⊢ C = B
3	2	eqcomi 2357	. 2 ⊢ B = C
4	1, 3	syl6eq 2401	1 ⊢ (φ → A = C)

Syntax hints:   → wi 4   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  3eqtr4g  2410  iinrab2  4030  setswith  4322  pw1equn  4332  uniabio  4350  iotanul  4355  nnsucelrlem3  4427  ltfintr  4460  lefinlteq  4464  sfinltfin  4536  1cvsfin  4543  tncveqnc1fin  4545  phialllem1  4617  phialllem2  4618  dfimafn2  5368  fnasrn  5418  ffnov  5588  fnov  5592  fnrnov  5606  foov  5607  funimassov  5610  ovelimab  5611  fce  6189  ce0  6191  el2c  6192  nc0le1  6217  nclenn  6250  ncslesuc  6268  nchoicelem9  6298