Theorem eqtr3i 2200

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

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtr3i  2206  3eqtr3ri  2207  unundi  3298  unundir  3299  inindi  3354  inindir  3355  difun1  3397  difabs  3401  notab  3407  dfrab2  3412  dif0  3495  difdifdirss  3509  tpidm13  3694  intmin2  3872  univ  4478  iunxpconst  4688  dmres  4930  opabresid  4962  rnresi  4987  cnvcnv  5083  rnresv  5090  cnvsn0  5099  cnvsn  5113  resdmres  5122  coi2  5147  coires1  5148  dfdm2  5165  isarep2  5305  ssimaex  5580  fnreseql  5629  fmptpr  5711  idref  5760  mpompt  5970  caov31  6067  xpexgALT  6137  cnvoprab  6238  frec0g  6401  unfiin  6928  xpfi  6932  endjusym  7098  halfnqq  7412  caucvgprlemm  7670  caucvgprprlemmu  7697  caucvgsr  7804  mvlladdi  8178  8th4div3  9141  nneoor  9358  nummac  9431  numadd  9433  numaddc  9434  nummul1c  9435  decbin0  9526  infrenegsupex  9597  iseqvalcbv  10460  m1expcl2  10545  facnn  10710  fac0  10711  4bc3eq4  10756  fihasheq0  10776  resqrexlemcalc1  11026  sqrt1  11058  sqrt4  11059  sqrt9  11060  infxrnegsupex  11274  isumss2  11404  geo2sum2  11526  geoihalfsum  11533  sin0  11740  efival  11743  ef01bndlem  11767  cos2bnd  11771  sin4lt0  11777  flodddiv4  11942  2prm  12130  znnen  12402  ennnfonelemhf1o  12417  setsslid  12516  ressressg  12537  metreslem  14020  retopbas  14163  sinhalfpilem  14352  sincos6thpi  14403  sincos3rdpi  14404  lgsdir2lem3  14571  lgseisenlem1  14590  lgseisenlem2  14591  2lgsoddprmlem2  14594