Theorem eqtr3i 2252

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr3i  2258  3eqtr3ri  2259  unundi  3365  unundir  3366  inindi  3421  inindir  3422  difun1  3464  difabs  3468  notab  3474  dfrab2  3479  dif0  3562  difdifdirss  3576  tpidm13  3766  intmin2  3949  univ  4567  iunxpconst  4779  dmres  5026  rnresi  5085  cnvcnv  5181  rnresv  5188  cnvsn0  5197  cnvsn  5211  resdmres  5220  coi2  5245  coires1  5246  dfdm2  5263  isarep2  5408  ssimaex  5697  fnreseql  5747  fmptpr  5835  idref  5886  mpompt  6102  caov31  6201  xpexgALT  6284  cnvoprab  6386  frec0g  6549  unfiin  7099  xpfi  7105  endjusym  7274  halfnqq  7608  caucvgprlemm  7866  caucvgprprlemmu  7893  caucvgsr  8000  mvlladdi  8375  8th4div3  9341  nneoor  9560  nummac  9633  numadd  9635  numaddc  9636  nummul1c  9637  decbin0  9728  infrenegsupex  9801  xnn0nnen  10671  iseqvalcbv  10693  m1expcl2  10795  facnn  10961  fac0  10962  4bc3eq4  11007  fihasheq0  11027  resqrexlemcalc1  11540  sqrt1  11572  sqrt4  11573  sqrt9  11574  infxrnegsupex  11789  isumss2  11919  geo2sum2  12041  geoihalfsum  12048  sin0  12255  efival  12258  ef01bndlem  12282  cos2bnd  12286  sin4lt0  12293  flodddiv4  12462  2prm  12664  dec5dvds  12950  modxai  12954  mod2xi  12955  gcdi  12958  numexp2x  12963  decsplit  12967  znnen  12984  ennnfonelemhf1o  12999  setsslid  13098  ressressg  13123  metreslem  15069  retopbas  15212  cnfldms  15225  sinhalfpilem  15480  sincos6thpi  15531  sincos3rdpi  15532  lgsdir2lem3  15724  lgseisenlem1  15764  lgseisenlem2  15765  lgsquadlem1  15771  lgsquadlem2  15772  2lgsoddprmlem2  15800