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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  3eqtr3i  2260  3eqtr3ri  2261  unundi  3370  unundir  3371  inindi  3426  inindir  3427  difun1  3469  difabs  3473  notab  3479  dfrab2  3484  dif0  3567  difdifdirss  3581  tpidm13  3775  intmin2  3959  univ  4579  iunxpconst  4792  dmres  5040  rnresi  5100  cnvcnv  5196  rnresv  5203  cnvsn0  5212  cnvsn  5226  resdmres  5235  coi2  5260  coires1  5261  dfdm2  5278  isarep2  5424  ssimaex  5716  fnreseql  5766  fmptpr  5854  idref  5907  mpompt  6123  caov31  6222  xpexgALT  6304  cnvoprab  6408  frec0g  6606  unfiin  7161  xpfi  7167  endjusym  7338  halfnqq  7673  caucvgprlemm  7931  caucvgprprlemmu  7958  caucvgsr  8065  mvlladdi  8439  8th4div3  9405  nneoor  9626  nummac  9699  numadd  9701  numaddc  9702  nummul1c  9703  decbin0  9794  infrenegsupex  9872  xnn0nnen  10745  iseqvalcbv  10767  m1expcl2  10869  facnn  11035  fac0  11036  4bc3eq4  11081  fihasheq0  11101  resqrexlemcalc1  11637  sqrt1  11669  sqrt4  11670  sqrt9  11671  infxrnegsupex  11886  isumss2  12017  geo2sum2  12139  geoihalfsum  12146  sin0  12353  efival  12356  ef01bndlem  12380  cos2bnd  12384  sin4lt0  12391  flodddiv4  12560  2prm  12762  dec5dvds  13048  modxai  13052  mod2xi  13053  gcdi  13056  numexp2x  13061  decsplit  13065  znnen  13082  ennnfonelemhf1o  13097  setsslid  13196  ressressg  13221  metreslem  15174  retopbas  15317  cnfldms  15330  sinhalfpilem  15585  sincos6thpi  15636  sincos3rdpi  15637  lgsdir2lem3  15832  lgseisenlem1  15872  lgseisenlem2  15873  lgsquadlem1  15879  lgsquadlem2  15880  2lgsoddprmlem2  15908