Theorem eqtr3i 2228

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  3eqtr3i  2234  3eqtr3ri  2235  unundi  3334  unundir  3335  inindi  3390  inindir  3391  difun1  3433  difabs  3437  notab  3443  dfrab2  3448  dif0  3531  difdifdirss  3545  tpidm13  3733  intmin2  3911  univ  4523  iunxpconst  4735  dmres  4980  rnresi  5039  cnvcnv  5135  rnresv  5142  cnvsn0  5151  cnvsn  5165  resdmres  5174  coi2  5199  coires1  5200  dfdm2  5217  isarep2  5361  ssimaex  5640  fnreseql  5690  fmptpr  5776  idref  5825  mpompt  6037  caov31  6136  xpexgALT  6218  cnvoprab  6320  frec0g  6483  unfiin  7023  xpfi  7029  endjusym  7198  halfnqq  7523  caucvgprlemm  7781  caucvgprprlemmu  7808  caucvgsr  7915  mvlladdi  8290  8th4div3  9256  nneoor  9475  nummac  9548  numadd  9550  numaddc  9551  nummul1c  9552  decbin0  9643  infrenegsupex  9715  xnn0nnen  10582  iseqvalcbv  10604  m1expcl2  10706  facnn  10872  fac0  10873  4bc3eq4  10918  fihasheq0  10938  resqrexlemcalc1  11325  sqrt1  11357  sqrt4  11358  sqrt9  11359  infxrnegsupex  11574  isumss2  11704  geo2sum2  11826  geoihalfsum  11833  sin0  12040  efival  12043  ef01bndlem  12067  cos2bnd  12071  sin4lt0  12078  flodddiv4  12247  2prm  12449  dec5dvds  12735  modxai  12739  mod2xi  12740  gcdi  12743  numexp2x  12748  decsplit  12752  znnen  12769  ennnfonelemhf1o  12784  setsslid  12883  ressressg  12907  metreslem  14852  retopbas  14995  cnfldms  15008  sinhalfpilem  15263  sincos6thpi  15314  sincos3rdpi  15315  lgsdir2lem3  15507  lgseisenlem1  15547  lgseisenlem2  15548  lgsquadlem1  15554  lgsquadlem2  15555  2lgsoddprmlem2  15583