Theorem syl6eqr 2090

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

Hypotheses

Ref	Expression
syl6eqr.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6eqr.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
syl6eqr	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem syl6eqr

Step	Hyp	Ref	Expression
1		syl6eqr.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6eqr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2044	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6eq 2088	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  3eqtr4g  2097  rabxmdc  3249  relop  4486  csbcnvg  4519  dfiun3g  4589  dfiin3g  4590  resima2  4644  relcnvfld  4851  uniabio  4877  fntpg  4955  dffn5im  5219  dfimafn2  5223  fncnvima2  5288  fmptcof  5331  fcoconst  5334  fnasrng  5343  ffnov  5605  fnovim  5609  fnrnov  5646  foov  5647  funimassov  5650  ovelimab  5651  ofc12  5731  caofinvl  5733  dftpos3  5877  tfr0  5937  rdgisucinc  5972  oasuc  6044  ecinxp  6181  phplem1  6315  indpi  6440  nqnq0pi  6536  nq0m0r  6554  addnqpr1  6660  recexgt0sr  6858  recidpipr  6932  recidpirq  6934  axrnegex  6953  nntopi  6968  cnref1o  8582  fztp  8940  fseq1m1p1  8957  frecuzrdgrrn  9194  frecuzrdgsuc  9201  mulexpzap  9295  expaddzap  9299  cjexp  9493  rexuz3  9588  climconst  9811