Theorem eqtr3id 2204

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

Hypotheses

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

Assertion

Ref	Expression
eqtr3id	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr3id

Step	Hyp	Ref	Expression
1		eqtr3id.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2161	. 2 ⊢ 𝐴 = 𝐵
3		eqtr3id.2	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	2, 3	syl5eq 2202	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1335

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

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

This theorem is referenced by:  3eqtr3g  2213  csbeq1a  3040  ssdifeq0  3476  pofun  4272  opabbi2dv  4734  funimaexg  5253  fresin  5347  f1imacnv  5430  foimacnv  5431  fsn2  5640  fmptpr  5658  funiunfvdm  5710  funiunfvdmf  5711  fcof1o  5736  f1opw2  6023  fnexALT  6058  eqerlem  6508  pmresg  6618  mapsn  6632  fopwdom  6778  mapen  6788  fiintim  6870  xpfi  6871  sbthlemi8  6905  sbthlemi9  6906  ctssdccl  7049  exmidfodomrlemim  7130  mul02  8256  recdivap  8585  fzpreddisj  9966  fzshftral  10003  qbtwnrelemcalc  10148  frec2uzrdg  10301  frecuzrdgrcl  10302  frecuzrdgsuc  10306  frecuzrdgrclt  10307  frecuzrdgg  10308  binom3  10528  bcn2  10631  hashfz1  10650  hashunlem  10671  hashfacen  10700  cnrecnv  10803  resqrexlemnm  10911  amgm2  11011  2zsupmax  11118  xrmaxltsup  11148  xrmaxadd  11151  xrbdtri  11166  fisumss  11282  fsumcnv  11327  telfsumo  11356  fsumiun  11367  arisum2  11389  fprodssdc  11480  fprodsplitdc  11486  fprodsplit  11487  fprodcnv  11515  ege2le3  11561  efgt1p  11586  cos01bnd  11648  dfgcd3  11885  eucalgval  11922  sqrt2irrlem  12026  setsslid  12211  baspartn  12419  txdis1cn  12649  cnmpt21  12662  cnmpt22  12665  hmeores  12686  metreslem  12751  remetdval  12910  dvfvalap  13021  binom4  13267  nninfsellemqall  13558