Theorem syl5eqr 2128

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem syl5eqr

Step	Hyp	Ref	Expression
1		syl5eqr.1	. . 3 |- B = A
2	1	eqcomi 2086	. 2 |- A = B
3		syl5eqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5eq 2126	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1285

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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064

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

This theorem is referenced by:  3eqtr3g  2137  csbeq1a  2917  ssdifeq0  3332  pofun  4075  opabbi2dv  4513  funimaexg  5014  fresin  5099  f1imacnv  5174  foimacnv  5175  fsn2  5369  fmptpr  5387  funiunfvdm  5434  funiunfvdmf  5435  fcof1o  5460  f1opw2  5737  fnexALT  5771  eqerlem  6203  fopwdom  6380  mul02  7558  recdivap  7873  fzpreddisj  9164  fzshftral  9201  qbtwnrelemcalc  9342  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  binom3  9687  bcn2  9788  sizefz1  9807  sizeunlem  9828  cnrecnv  9935  resqrexlemnm  10042  amgm2  10142  dfgcd3  10543  eucalgval  10580  sqrt2irrlem  10684