Theorem eqtr3i 2254

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

Syntax hints:   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtr3i  2260  3eqtr3ri  2261  unundi  3368  unundir  3369  inindi  3424  inindir  3425  difun1  3467  difabs  3471  notab  3477  dfrab2  3482  dif0  3565  difdifdirss  3579  tpidm13  3771  intmin2  3954  univ  4573  iunxpconst  4786  dmres  5034  rnresi  5093  cnvcnv  5189  rnresv  5196  cnvsn0  5205  cnvsn  5219  resdmres  5228  coi2  5253  coires1  5254  dfdm2  5271  isarep2  5417  ssimaex  5707  fnreseql  5757  fmptpr  5846  idref  5897  mpompt  6113  caov31  6212  xpexgALT  6295  cnvoprab  6399  frec0g  6563  unfiin  7118  xpfi  7124  endjusym  7295  halfnqq  7630  caucvgprlemm  7888  caucvgprprlemmu  7915  caucvgsr  8022  mvlladdi  8397  8th4div3  9363  nneoor  9582  nummac  9655  numadd  9657  numaddc  9658  nummul1c  9659  decbin0  9750  infrenegsupex  9828  xnn0nnen  10700  iseqvalcbv  10722  m1expcl2  10824  facnn  10990  fac0  10991  4bc3eq4  11036  fihasheq0  11056  resqrexlemcalc1  11579  sqrt1  11611  sqrt4  11612  sqrt9  11613  infxrnegsupex  11828  isumss2  11959  geo2sum2  12081  geoihalfsum  12088  sin0  12295  efival  12298  ef01bndlem  12322  cos2bnd  12326  sin4lt0  12333  flodddiv4  12502  2prm  12704  dec5dvds  12990  modxai  12994  mod2xi  12995  gcdi  12998  numexp2x  13003  decsplit  13007  znnen  13024  ennnfonelemhf1o  13039  setsslid  13138  ressressg  13163  metreslem  15110  retopbas  15253  cnfldms  15266  sinhalfpilem  15521  sincos6thpi  15572  sincos3rdpi  15573  lgsdir2lem3  15765  lgseisenlem1  15805  lgseisenlem2  15806  lgsquadlem1  15812  lgsquadlem2  15813  2lgsoddprmlem2  15841