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  7496  caucvgprlemm  7754  caucvgprprlemmu  7781  caucvgsr  7888  mvlladdi  8263  8th4div3  9229  nneoor  9447  nummac  9520  numadd  9522  numaddc  9523  nummul1c  9524  decbin0  9615  infrenegsupex  9687  xnn0nnen  10548  iseqvalcbv  10570  m1expcl2  10672  facnn  10838  fac0  10839  4bc3eq4  10884  fihasheq0  10904  resqrexlemcalc1  11198  sqrt1  11230  sqrt4  11231  sqrt9  11232  infxrnegsupex  11447  isumss2  11577  geo2sum2  11699  geoihalfsum  11706  sin0  11913  efival  11916  ef01bndlem  11940  cos2bnd  11944  sin4lt0  11951  flodddiv4  12120  2prm  12322  dec5dvds  12608  modxai  12612  mod2xi  12613  gcdi  12616  numexp2x  12621  decsplit  12625  znnen  12642  ennnfonelemhf1o  12657  setsslid  12756  ressressg  12780  metreslem  14724  retopbas  14867  cnfldms  14880  sinhalfpilem  15135  sincos6thpi  15186  sincos3rdpi  15187  lgsdir2lem3  15379  lgseisenlem1  15419  lgseisenlem2  15420  lgsquadlem1  15426  lgsquadlem2  15427  2lgsoddprmlem2  15455