Theorem syl5reqr 2185

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 2141	. 2 ⊢ 𝐴 = 𝐵
3		syl5reqr.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5req 2183	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

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

This theorem is referenced by:  bm2.5ii  4407  resdmdfsn  4857  f0dom0  5311  f1o00  5395  fmpt  5563  fmptsn  5602  resfunexg  5634  mapsn  6577  sbthlemi4  6841  sbthlemi6  6843  pm54.43  7039  prarloclem5  7301  recexprlem1ssl  7434  recexprlem1ssu  7435  iooval2  9691  hashsng  10537  zfz1isolem1  10576  resqrexlemover  10775  isumclim3  11185  algrp1  11716  tangtx  12908  coskpi  12918  subctctexmid  13185