Theorem eqtr3i 2252

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr3i  2258  3eqtr3ri  2259  unundi  3366  unundir  3367  inindi  3422  inindir  3423  difun1  3465  difabs  3469  notab  3475  dfrab2  3480  dif0  3563  difdifdirss  3577  tpidm13  3769  intmin2  3952  univ  4571  iunxpconst  4784  dmres  5032  rnresi  5091  cnvcnv  5187  rnresv  5194  cnvsn0  5203  cnvsn  5217  resdmres  5226  coi2  5251  coires1  5252  dfdm2  5269  isarep2  5414  ssimaex  5703  fnreseql  5753  fmptpr  5841  idref  5892  mpompt  6108  caov31  6207  xpexgALT  6290  cnvoprab  6394  frec0g  6558  unfiin  7111  xpfi  7117  endjusym  7286  halfnqq  7620  caucvgprlemm  7878  caucvgprprlemmu  7905  caucvgsr  8012  mvlladdi  8387  8th4div3  9353  nneoor  9572  nummac  9645  numadd  9647  numaddc  9648  nummul1c  9649  decbin0  9740  infrenegsupex  9818  xnn0nnen  10689  iseqvalcbv  10711  m1expcl2  10813  facnn  10979  fac0  10980  4bc3eq4  11025  fihasheq0  11045  resqrexlemcalc1  11565  sqrt1  11597  sqrt4  11598  sqrt9  11599  infxrnegsupex  11814  isumss2  11944  geo2sum2  12066  geoihalfsum  12073  sin0  12280  efival  12283  ef01bndlem  12307  cos2bnd  12311  sin4lt0  12318  flodddiv4  12487  2prm  12689  dec5dvds  12975  modxai  12979  mod2xi  12980  gcdi  12983  numexp2x  12988  decsplit  12992  znnen  13009  ennnfonelemhf1o  13024  setsslid  13123  ressressg  13148  metreslem  15094  retopbas  15237  cnfldms  15250  sinhalfpilem  15505  sincos6thpi  15556  sincos3rdpi  15557  lgsdir2lem3  15749  lgseisenlem1  15789  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  2lgsoddprmlem2  15825