Theorem syl6reqr 2139

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

Hypotheses

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

Assertion

Ref	Expression
syl6reqr	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem syl6reqr

Step	Hyp	Ref	Expression
1		syl6reqr.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6reqr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2092	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6req 2137	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1289

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081

This theorem is referenced by:  iftrue  3398  iffalse  3401  difprsn1  3576  dmmptg  4928  relcoi1  4962  funimacnv  5090  dffv3g  5301  dfimafn  5353  fvco2  5373  isoini  5597  oprabco  5982  unfiexmid  6628  undifdc  6634  sbthlemi4  6669  sbthlemi5  6670  sbthlemi6  6671  supval2ti  6690  exmidfodomrlemim  6827  eqneg  8199  zeo  8851  fseq1p1m1  9508  iseqval  9871  iseqvalt  9873  seq3val  9874  hashfzo  10230  hashxp  10234  fsumconst  10848  modfsummod  10852  telfsumo  10860  mulgcd  11283  ialgrp1  11306  ialgcvg  11308  phiprmpw  11476  strslfv3  11539