Theorem eqtr3i 2230

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 2211	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2228	1 ⊢ 𝐵 = 𝐶

Syntax hints:   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  3eqtr3i  2236  3eqtr3ri  2237  unundi  3342  unundir  3343  inindi  3398  inindir  3399  difun1  3441  difabs  3445  notab  3451  dfrab2  3456  dif0  3539  difdifdirss  3553  tpidm13  3743  intmin2  3925  univ  4541  iunxpconst  4753  dmres  4999  rnresi  5058  cnvcnv  5154  rnresv  5161  cnvsn0  5170  cnvsn  5184  resdmres  5193  coi2  5218  coires1  5219  dfdm2  5236  isarep2  5380  ssimaex  5663  fnreseql  5713  fmptpr  5799  idref  5848  mpompt  6060  caov31  6159  xpexgALT  6241  cnvoprab  6343  frec0g  6506  unfiin  7049  xpfi  7055  endjusym  7224  halfnqq  7558  caucvgprlemm  7816  caucvgprprlemmu  7843  caucvgsr  7950  mvlladdi  8325  8th4div3  9291  nneoor  9510  nummac  9583  numadd  9585  numaddc  9586  nummul1c  9587  decbin0  9678  infrenegsupex  9750  xnn0nnen  10619  iseqvalcbv  10641  m1expcl2  10743  facnn  10909  fac0  10910  4bc3eq4  10955  fihasheq0  10975  resqrexlemcalc1  11440  sqrt1  11472  sqrt4  11473  sqrt9  11474  infxrnegsupex  11689  isumss2  11819  geo2sum2  11941  geoihalfsum  11948  sin0  12155  efival  12158  ef01bndlem  12182  cos2bnd  12186  sin4lt0  12193  flodddiv4  12362  2prm  12564  dec5dvds  12850  modxai  12854  mod2xi  12855  gcdi  12858  numexp2x  12863  decsplit  12867  znnen  12884  ennnfonelemhf1o  12899  setsslid  12998  ressressg  13022  metreslem  14967  retopbas  15110  cnfldms  15123  sinhalfpilem  15378  sincos6thpi  15429  sincos3rdpi  15430  lgsdir2lem3  15622  lgseisenlem1  15662  lgseisenlem2  15663  lgsquadlem1  15669  lgsquadlem2  15670  2lgsoddprmlem2  15698