Theorem eqtr3i 2160

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

Syntax hints:   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130

This theorem is referenced by:  3eqtr3i  2166  3eqtr3ri  2167  unundi  3232  unundir  3233  inindi  3288  inindir  3289  difun1  3331  difabs  3335  notab  3341  dfrab2  3346  dif0  3428  difdifdirss  3442  tpidm13  3618  intmin2  3792  univ  4392  iunxpconst  4594  dmres  4835  opabresid  4867  rnresi  4891  cnvcnv  4986  rnresv  4993  cnvsn0  5002  cnvsn  5016  resdmres  5025  coi2  5050  coires1  5051  dfdm2  5068  isarep2  5205  ssimaex  5475  fnreseql  5523  fmptpr  5605  idref  5651  mpompt  5856  caov31  5953  xpexgALT  6024  cnvoprab  6124  frec0g  6287  unfiin  6807  xpfi  6811  endjusym  6974  halfnqq  7211  caucvgprlemm  7469  caucvgprprlemmu  7496  caucvgsr  7603  mvlladdi  7973  8th4div3  8932  nneoor  9146  nummac  9219  numadd  9221  numaddc  9222  nummul1c  9223  decbin0  9314  infrenegsupex  9382  iseqvalcbv  10223  m1expcl2  10308  facnn  10466  fac0  10467  4bc3eq4  10512  fihasheq0  10533  resqrexlemcalc1  10779  sqrt1  10811  sqrt4  10812  sqrt9  10813  infxrnegsupex  11025  isumss2  11155  geo2sum2  11277  geoihalfsum  11284  sin0  11425  efival  11428  ef01bndlem  11452  cos2bnd  11456  sin4lt0  11462  flodddiv4  11620  2prm  11797  znnen  11900  ennnfonelemhf1o  11915  setsslid  11998  metreslem  12538  retopbas  12681  sinhalfpilem  12861  sincos6thpi  12912  sincos3rdpi  12913