Theorem syl5eqr 2187

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 2144	. 2 ⊢ 𝐴 = 𝐵
3		syl5eqr.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5eq 2185	1 ⊢ (𝜑 → 𝐴 = 𝐶)

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:  3eqtr3g  2196  csbeq1a  3016  ssdifeq0  3450  pofun  4242  opabbi2dv  4696  funimaexg  5215  fresin  5309  f1imacnv  5392  foimacnv  5393  fsn2  5602  fmptpr  5620  funiunfvdm  5672  funiunfvdmf  5673  fcof1o  5698  f1opw2  5984  fnexALT  6019  eqerlem  6468  pmresg  6578  mapsn  6592  fopwdom  6738  mapen  6748  fiintim  6825  xpfi  6826  sbthlemi8  6860  sbthlemi9  6861  ctssdccl  7004  exmidfodomrlemim  7074  mul02  8173  recdivap  8502  fzpreddisj  9882  fzshftral  9919  qbtwnrelemcalc  10064  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  binom3  10440  bcn2  10542  hashfz1  10561  hashunlem  10582  hashfacen  10611  cnrecnv  10714  resqrexlemnm  10822  amgm2  10922  2zsupmax  11029  xrmaxltsup  11059  xrmaxadd  11062  xrbdtri  11077  fisumss  11193  fsumcnv  11238  telfsumo  11267  fsumiun  11278  arisum2  11300  ege2le3  11414  efgt1p  11439  cos01bnd  11501  dfgcd3  11734  eucalgval  11771  sqrt2irrlem  11875  setsslid  12048  baspartn  12256  txdis1cn  12486  cnmpt21  12499  cnmpt22  12502  hmeores  12523  metreslem  12588  remetdval  12747  dvfvalap  12858  nninfsellemqall  13386