Theorem eqtr3i 2193

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

Syntax hints:   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  3eqtr3i  2199  3eqtr3ri  2200  unundi  3288  unundir  3289  inindi  3344  inindir  3345  difun1  3387  difabs  3391  notab  3397  dfrab2  3402  dif0  3485  difdifdirss  3499  tpidm13  3683  intmin2  3857  univ  4461  iunxpconst  4671  dmres  4912  opabresid  4944  rnresi  4968  cnvcnv  5063  rnresv  5070  cnvsn0  5079  cnvsn  5093  resdmres  5102  coi2  5127  coires1  5128  dfdm2  5145  isarep2  5285  ssimaex  5557  fnreseql  5606  fmptpr  5688  idref  5736  mpompt  5945  caov31  6042  xpexgALT  6112  cnvoprab  6213  frec0g  6376  unfiin  6903  xpfi  6907  endjusym  7073  halfnqq  7372  caucvgprlemm  7630  caucvgprprlemmu  7657  caucvgsr  7764  mvlladdi  8137  8th4div3  9097  nneoor  9314  nummac  9387  numadd  9389  numaddc  9390  nummul1c  9391  decbin0  9482  infrenegsupex  9553  iseqvalcbv  10413  m1expcl2  10498  facnn  10661  fac0  10662  4bc3eq4  10707  fihasheq0  10728  resqrexlemcalc1  10978  sqrt1  11010  sqrt4  11011  sqrt9  11012  infxrnegsupex  11226  isumss2  11356  geo2sum2  11478  geoihalfsum  11485  sin0  11692  efival  11695  ef01bndlem  11719  cos2bnd  11723  sin4lt0  11729  flodddiv4  11893  2prm  12081  znnen  12353  ennnfonelemhf1o  12368  setsslid  12466  metreslem  13174  retopbas  13317  sinhalfpilem  13506  sincos6thpi  13557  sincos3rdpi  13558  lgsdir2lem3  13725