Theorem eqtr3i 2180

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

Syntax hints:   = wceq 1335

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

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

This theorem is referenced by:  3eqtr3i  2186  3eqtr3ri  2187  unundi  3268  unundir  3269  inindi  3324  inindir  3325  difun1  3367  difabs  3371  notab  3377  dfrab2  3382  dif0  3464  difdifdirss  3478  tpidm13  3659  intmin2  3833  univ  4434  iunxpconst  4643  dmres  4884  opabresid  4916  rnresi  4940  cnvcnv  5035  rnresv  5042  cnvsn0  5051  cnvsn  5065  resdmres  5074  coi2  5099  coires1  5100  dfdm2  5117  isarep2  5254  ssimaex  5526  fnreseql  5574  fmptpr  5656  idref  5702  mpompt  5907  caov31  6004  xpexgALT  6075  cnvoprab  6175  frec0g  6338  unfiin  6863  xpfi  6867  endjusym  7030  halfnqq  7313  caucvgprlemm  7571  caucvgprprlemmu  7598  caucvgsr  7705  mvlladdi  8076  8th4div3  9035  nneoor  9249  nummac  9322  numadd  9324  numaddc  9325  nummul1c  9326  decbin0  9417  infrenegsupex  9488  iseqvalcbv  10338  m1expcl2  10423  facnn  10583  fac0  10584  4bc3eq4  10629  fihasheq0  10650  resqrexlemcalc1  10896  sqrt1  10928  sqrt4  10929  sqrt9  10930  infxrnegsupex  11142  isumss2  11272  geo2sum2  11394  geoihalfsum  11401  sin0  11608  efival  11611  ef01bndlem  11635  cos2bnd  11639  sin4lt0  11645  flodddiv4  11806  2prm  11984  znnen  12099  ennnfonelemhf1o  12114  setsslid  12200  metreslem  12740  retopbas  12883  sinhalfpilem  13072  sincos6thpi  13123  sincos3rdpi  13124