Theorem eqtr3i 2261

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

Syntax hints:   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  3eqtr3i  2267  3eqtr3ri  2268  unundi  3390  unundir  3391  inindi  3448  inindir  3449  difun1  3491  difabs  3495  notab  3503  dfrab2  3508  dif0  3594  difdifdirss  3609  tpidm13  3807  intmin2  3991  univ  4617  iunxpconst  4830  dmres  5079  rnresi  5139  cnvcnv  5235  rnresv  5242  cnvsn0  5251  cnvsn  5265  resdmres  5274  coi2  5299  coires1  5300  dfdm2  5317  isarep2  5463  ssimaex  5758  fnreseql  5810  fmptpr  5898  idref  5952  mpompt  6170  caov31  6269  xpexgALT  6356  cnvoprab  6460  frec0g  6658  unfiin  7223  xpfi  7229  endjusym  7426  halfnqq  7767  caucvgprlemm  8025  caucvgprprlemmu  8052  caucvgsr  8159  mvlladdi  8534  8th4div3  9503  nneoor  9727  nummac  9800  numadd  9802  numaddc  9803  nummul1c  9804  decbin0  9895  infrenegsupex  9973  xnn0nnen  10852  iseqvalcbv  10874  m1expcl2  10976  facnn  11143  fac0  11144  4bc3eq4  11190  fihasheq0  11210  resqrexlemcalc1  11758  sqrt1  11790  sqrt4  11791  sqrt9  11792  infxrnegsupex  12007  isumss2  12138  geo2sum2  12260  geoihalfsum  12267  sin0  12474  efival  12477  ef01bndlem  12501  cos2bnd  12505  sin4lt0  12512  flodddiv4  12681  2prm  12883  dec5dvds  13169  modxai  13173  mod2xi  13174  gcdi  13177  numexp2x  13182  decsplit  13186  ballotfilem2  13206  znnen  13267  ennnfonelemhf1o  13282  setsslid  13381  ressressg  13406  metreslem  15404  retopbas  15547  cnfldms  15560  sinhalfpilem  15815  sincos6thpi  15866  sincos3rdpi  15867  lgsdir2lem3  16063  lgseisenlem1  16103  lgseisenlem2  16104  lgsquadlem1  16110  lgsquadlem2  16111  2lgsoddprmlem2  16139