Theorem syl5reqr 2187

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 2143	. 2 |- A = B
3		syl5reqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5req 2185	1 |- ( ph -> C = A )

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 2121

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

This theorem is referenced by:  bm2.5ii  4412  resdmdfsn  4862  f0dom0  5316  f1o00  5402  fmpt  5570  fmptsn  5609  resfunexg  5641  mapsn  6584  sbthlemi4  6848  sbthlemi6  6850  pm54.43  7046  prarloclem5  7308  recexprlem1ssl  7441  recexprlem1ssu  7442  iooval2  9698  hashsng  10544  zfz1isolem1  10583  resqrexlemover  10782  isumclim3  11192  algrp1  11727  tangtx  12919  coskpi  12929  subctctexmid  13196