Theorem syl5reqr 2136

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

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

Assertion

Ref	Expression
syl5reqr	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem syl5reqr

Step	Hyp	Ref	Expression
1		syl5reqr.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2093	. 2 ⊢ 𝐴 = 𝐵
3		syl5reqr.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5req 2134	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1290

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-4 1446  ax-17 1465  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-cleq 2082

This theorem is referenced by:  bm2.5ii  4326  resdmdfsn  4768  f0dom0  5217  f1o00  5301  fmpt  5463  fmptsn  5500  resfunexg  5532  mapsn  6461  sbthlemi4  6723  sbthlemi6  6725  pm54.43  6872  prarloclem5  7113  recexprlem1ssl  7246  recexprlem1ssu  7247  iooval2  9387  hashsng  10260  zfz1isolem1  10299  resqrexlemover  10497  isumclim3  10871  algrp1  11360