Theorem eqtr3i 2219

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr3i  2225  3eqtr3ri  2226  unundi  3325  unundir  3326  inindi  3381  inindir  3382  difun1  3424  difabs  3428  notab  3434  dfrab2  3439  dif0  3522  difdifdirss  3536  tpidm13  3723  intmin2  3901  univ  4512  iunxpconst  4724  dmres  4968  rnresi  5027  cnvcnv  5123  rnresv  5130  cnvsn0  5139  cnvsn  5153  resdmres  5162  coi2  5187  coires1  5188  dfdm2  5205  isarep2  5346  ssimaex  5625  fnreseql  5675  fmptpr  5757  idref  5806  mpompt  6018  caov31  6117  xpexgALT  6199  cnvoprab  6301  frec0g  6464  unfiin  6996  xpfi  7002  endjusym  7171  halfnqq  7494  caucvgprlemm  7752  caucvgprprlemmu  7779  caucvgsr  7886  mvlladdi  8261  8th4div3  9227  nneoor  9445  nummac  9518  numadd  9520  numaddc  9521  nummul1c  9522  decbin0  9613  infrenegsupex  9685  xnn0nnen  10546  iseqvalcbv  10568  m1expcl2  10670  facnn  10836  fac0  10837  4bc3eq4  10882  fihasheq0  10902  resqrexlemcalc1  11196  sqrt1  11228  sqrt4  11229  sqrt9  11230  infxrnegsupex  11445  isumss2  11575  geo2sum2  11697  geoihalfsum  11704  sin0  11911  efival  11914  ef01bndlem  11938  cos2bnd  11942  sin4lt0  11949  flodddiv4  12118  2prm  12320  dec5dvds  12606  modxai  12610  mod2xi  12611  gcdi  12614  numexp2x  12619  decsplit  12623  znnen  12640  ennnfonelemhf1o  12655  setsslid  12754  ressressg  12778  metreslem  14700  retopbas  14843  cnfldms  14856  sinhalfpilem  15111  sincos6thpi  15162  sincos3rdpi  15163  lgsdir2lem3  15355  lgseisenlem1  15395  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  2lgsoddprmlem2  15431