Theorem eqtr3i 2219

Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)

Hypotheses

Ref	Expression
eqtr3i.1	⊢ 𝐴 = 𝐵
eqtr3i.2	⊢ 𝐴 = 𝐶

Assertion

Ref	Expression
eqtr3i	⊢ 𝐵 = 𝐶

Proof of Theorem eqtr3i

Step	Hyp	Ref	Expression
1		eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2200	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2217	1 ⊢ 𝐵 = 𝐶

Syntax hints:   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189

This theorem is referenced by:  3eqtr3i  2225  3eqtr3ri  2226  unundi  3324  unundir  3325  inindi  3380  inindir  3381  difun1  3423  difabs  3427  notab  3433  dfrab2  3438  dif0  3521  difdifdirss  3535  tpidm13  3722  intmin2  3900  univ  4511  iunxpconst  4723  dmres  4967  rnresi  5026  cnvcnv  5122  rnresv  5129  cnvsn0  5138  cnvsn  5152  resdmres  5161  coi2  5186  coires1  5187  dfdm2  5204  isarep2  5345  ssimaex  5622  fnreseql  5672  fmptpr  5754  idref  5803  mpompt  6014  caov31  6113  xpexgALT  6190  cnvoprab  6292  frec0g  6455  unfiin  6987  xpfi  6993  endjusym  7162  halfnqq  7477  caucvgprlemm  7735  caucvgprprlemmu  7762  caucvgsr  7869  mvlladdi  8244  8th4div3  9210  nneoor  9428  nummac  9501  numadd  9503  numaddc  9504  nummul1c  9505  decbin0  9596  infrenegsupex  9668  xnn0nnen  10529  iseqvalcbv  10551  m1expcl2  10653  facnn  10819  fac0  10820  4bc3eq4  10865  fihasheq0  10885  resqrexlemcalc1  11179  sqrt1  11211  sqrt4  11212  sqrt9  11213  infxrnegsupex  11428  isumss2  11558  geo2sum2  11680  geoihalfsum  11687  sin0  11894  efival  11897  ef01bndlem  11921  cos2bnd  11925  sin4lt0  11932  flodddiv4  12101  2prm  12295  dec5dvds  12581  modxai  12585  mod2xi  12586  gcdi  12589  numexp2x  12594  decsplit  12598  znnen  12615  ennnfonelemhf1o  12630  setsslid  12729  ressressg  12753  metreslem  14616  retopbas  14759  cnfldms  14772  sinhalfpilem  15027  sincos6thpi  15078  sincos3rdpi  15079  lgsdir2lem3  15271  lgseisenlem1  15311  lgseisenlem2  15312  lgsquadlem1  15318  lgsquadlem2  15319  2lgsoddprmlem2  15347