Theorem syl5reqr 2188

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

Hypotheses

Ref	Expression
syl5reqr.1	|- B = A
syl5reqr.2	|- ( ph -> B = C )

Assertion

Ref	Expression
syl5reqr	|- ( ph -> C = A )

Proof of Theorem syl5reqr

Step	Hyp	Ref	Expression
1		syl5reqr.1	. . 3 |- B = A
2	1	eqcomi 2144	. 2 |- A = B
3		syl5reqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5req 2186	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  bm2.5ii  4420  resdmdfsn  4870  f0dom0  5324  f1o00  5410  fmpt  5578  fmptsn  5617  resfunexg  5649  mapsn  6592  sbthlemi4  6856  sbthlemi6  6858  pm54.43  7063  prarloclem5  7332  recexprlem1ssl  7465  recexprlem1ssu  7466  iooval2  9728  hashsng  10576  zfz1isolem1  10615  resqrexlemover  10814  isumclim3  11224  algrp1  11763  tangtx  12967  coskpi  12977  subctctexmid  13369