Theorem eqtr3i 2261

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr3i  2267  3eqtr3ri  2268  unundi  3390  unundir  3391  inindi  3448  inindir  3449  difun1  3491  difabs  3495  notab  3503  dfrab2  3508  dif0  3596  difdifdirss  3612  tpidm13  3811  intmin2  3996  univ  4624  iunxpconst  4837  dmres  5086  rnresi  5147  cnvcnv  5243  rnresv  5250  cnvsn0  5259  cnvsn  5273  resdmres  5282  coi2  5307  coires1  5308  dfdm2  5325  isarep2  5471  ssimaex  5767  fnreseql  5822  fmptpr  5910  idref  5965  mpompt  6183  caov31  6282  xpexgALT  6370  cnvoprab  6474  frec0g  6673  unfiin  7239  xpfi  7245  endjusym  7442  halfnqq  7783  caucvgprlemm  8041  caucvgprprlemmu  8068  caucvgsr  8175  mvlladdi  8551  8th4div3  9535  nneoor  9758  nummac  9836  numadd  9838  numaddc  9839  nummul1c  9840  decbin0  9931  infrenegsupex  10009  fz00m1  10467  xnn0nnen  10894  iseqvalcbv  10916  m1expcl2  11018  facnn  11186  fac0  11187  4bc3eq4  11233  fihasheq0  11253  resqrexlemcalc1  11801  sqrt1  11833  sqrt4  11834  sqrt9  11835  infxrnegsupex  12053  isumss2  12184  geo2sum2  12306  geoihalfsum  12313  sin0  12520  efival  12523  ef01bndlem  12547  cos2bnd  12551  sin4lt0  12558  flodddiv4  12727  2prm  12929  dec5dvds  13219  modxai  13223  mod2xi  13224  mod2xnegi  13226  gcdi  13228  numexp2x  13233  decsplit  13237  ballotfilem2  13285  znnen  13346  ennnfonelemhf1o  13361  setsslid  13460  ressressg  13487  metreslem  15623  retopbas  15766  cnfldms  15779  sinhalfpilem  16035  sincos6thpi  16086  sincos3rdpi  16087  log2tlbndlog2  16237  log2ublem2  16239  log2ublog2  16241  cht2  16293  ppiqub  16310  bposlem6  16333  bposlem8  16335  bposlem9  16336  lgsdir2lem3  16371  lgseisenlem1  16411  lgseisenlem2  16412  lgsquadlem1  16418  lgsquadlem2  16419  2lgsoddprmlem2  16447