Theorem syl5eqr 2086

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 2044	. 2 |- A = B
3		syl5eqr.2	. 2 |- ( ph -> B = C )
4	2, 3	syl5eq 2084	1 |- ( ph -> A = C )

Syntax hints:   -> wi 4   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  3eqtr3g  2095  csbeq1a  2860  ssdifeq0  3305  pofun  4049  opabbi2dv  4485  funimaexg  4983  fresin  5068  f1imacnv  5143  foimacnv  5144  fsn2  5337  fmptpr  5355  funiunfvdm  5402  funiunfvdmf  5403  fcof1o  5429  f1opw2  5706  fnexALT  5740  eqerlem  6137  fopwdom  6310  mul02  7384  recdivap  7694  fzpreddisj  8933  fzshftral  8970  qbtwnrelemcalc  9110  frec2uzrdg  9195  binom3  9366  cnrecnv  9510  resqrexlemnm  9616  amgm2  9714  sqr2irrlem  9877