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  3948  univ  4566  iunxpconst  4778  dmres  5025  rnresi  5084  cnvcnv  5180  rnresv  5187  cnvsn0  5196  cnvsn  5210  resdmres  5219  coi2  5244  coires1  5245  dfdm2  5262  isarep2  5407  ssimaex  5694  fnreseql  5744  fmptpr  5830  idref  5879  mpompt  6095  caov31  6194  xpexgALT  6276  cnvoprab  6378  frec0g  6541  unfiin  7084  xpfi  7090  endjusym  7259  halfnqq  7593  caucvgprlemm  7851  caucvgprprlemmu  7878  caucvgsr  7985  mvlladdi  8360  8th4div3  9326  nneoor  9545  nummac  9618  numadd  9620  numaddc  9621  nummul1c  9622  decbin0  9713  infrenegsupex  9785  xnn0nnen  10654  iseqvalcbv  10676  m1expcl2  10778  facnn  10944  fac0  10945  4bc3eq4  10990  fihasheq0  11010  resqrexlemcalc1  11520  sqrt1  11552  sqrt4  11553  sqrt9  11554  infxrnegsupex  11769  isumss2  11899  geo2sum2  12021  geoihalfsum  12028  sin0  12235  efival  12238  ef01bndlem  12262  cos2bnd  12266  sin4lt0  12273  flodddiv4  12442  2prm  12644  dec5dvds  12930  modxai  12934  mod2xi  12935  gcdi  12938  numexp2x  12943  decsplit  12947  znnen  12964  ennnfonelemhf1o  12979  setsslid  13078  ressressg  13103  metreslem  15048  retopbas  15191  cnfldms  15204  sinhalfpilem  15459  sincos6thpi  15510  sincos3rdpi  15511  lgsdir2lem3  15703  lgseisenlem1  15743  lgseisenlem2  15744  lgsquadlem1  15750  lgsquadlem2  15751  2lgsoddprmlem2  15779