Theorem syl5eqr 2184

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

Hypotheses

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

Assertion

Ref	Expression
syl5eqr	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem syl5eqr

Step	Hyp	Ref	Expression
1		syl5eqr.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2141	. 2 ⊢ 𝐴 = 𝐵
3		syl5eqr.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5eq 2182	1 ⊢ (𝜑 → 𝐴 = 𝐶)

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 2119

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

This theorem is referenced by:  3eqtr3g  2193  csbeq1a  3007  ssdifeq0  3440  pofun  4229  opabbi2dv  4683  funimaexg  5202  fresin  5296  f1imacnv  5377  foimacnv  5378  fsn2  5587  fmptpr  5605  funiunfvdm  5657  funiunfvdmf  5658  fcof1o  5683  f1opw2  5969  fnexALT  6004  eqerlem  6453  pmresg  6563  mapsn  6577  fopwdom  6723  mapen  6733  fiintim  6810  xpfi  6811  sbthlemi8  6845  sbthlemi9  6846  ctssdccl  6989  exmidfodomrlemim  7050  mul02  8142  recdivap  8471  fzpreddisj  9844  fzshftral  9881  qbtwnrelemcalc  10026  frec2uzrdg  10175  frecuzrdgrcl  10176  frecuzrdgsuc  10180  frecuzrdgrclt  10181  frecuzrdgg  10182  binom3  10402  bcn2  10503  hashfz1  10522  hashunlem  10543  hashfacen  10572  cnrecnv  10675  resqrexlemnm  10783  amgm2  10883  2zsupmax  10990  xrmaxltsup  11020  xrmaxadd  11023  xrbdtri  11038  fisumss  11154  fsumcnv  11199  telfsumo  11228  fsumiun  11239  arisum2  11261  ege2le3  11366  efgt1p  11391  cos01bnd  11454  dfgcd3  11687  eucalgval  11724  sqrt2irrlem  11828  setsslid  11998  baspartn  12206  txdis1cn  12436  cnmpt21  12449  cnmpt22  12452  hmeores  12473  metreslem  12538  remetdval  12697  dvfvalap  12808  nninfsellemqall  13200