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  5845  idref  5896  mpompt  6112  caov31  6211  xpexgALT  6294  cnvoprab  6398  frec0g  6562  unfiin  7117  xpfi  7123  endjusym  7294  halfnqq  7629  caucvgprlemm  7887  caucvgprprlemmu  7914  caucvgsr  8021  mvlladdi  8396  8th4div3  9362  nneoor  9581  nummac  9654  numadd  9656  numaddc  9657  nummul1c  9658  decbin0  9749  infrenegsupex  9827  xnn0nnen  10698  iseqvalcbv  10720  m1expcl2  10822  facnn  10988  fac0  10989  4bc3eq4  11034  fihasheq0  11054  resqrexlemcalc1  11574  sqrt1  11606  sqrt4  11607  sqrt9  11608  infxrnegsupex  11823  isumss2  11953  geo2sum2  12075  geoihalfsum  12082  sin0  12289  efival  12292  ef01bndlem  12316  cos2bnd  12320  sin4lt0  12327  flodddiv4  12496  2prm  12698  dec5dvds  12984  modxai  12988  mod2xi  12989  gcdi  12992  numexp2x  12997  decsplit  13001  znnen  13018  ennnfonelemhf1o  13033  setsslid  13132  ressressg  13157  metreslem  15103  retopbas  15246  cnfldms  15259  sinhalfpilem  15514  sincos6thpi  15565  sincos3rdpi  15566  lgsdir2lem3  15758  lgseisenlem1  15798  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  2lgsoddprmlem2  15834