Theorem eqtr3i 2200

Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)

Hypotheses

Ref	Expression
eqtr3i.1	|- A = B
eqtr3i.2	|- A = C

Assertion

Ref	Expression
eqtr3i	|- B = C

Proof of Theorem eqtr3i

Step	Hyp	Ref	Expression
1		eqtr3i.1	. . 3 |- A = B
2	1	eqcomi 2181	. 2 |- B = A
3		eqtr3i.2	. 2 |- A = C
4	2, 3	eqtri 2198	1 |- B = C

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  5579  fnreseql  5628  fmptpr  5710  idref  5759  mpompt  5969  caov31  6066  xpexgALT  6136  cnvoprab  6237  frec0g  6400  unfiin  6927  xpfi  6931  endjusym  7097  halfnqq  7411  caucvgprlemm  7669  caucvgprprlemmu  7696  caucvgsr  7803  mvlladdi  8177  8th4div3  9140  nneoor  9357  nummac  9430  numadd  9432  numaddc  9433  nummul1c  9434  decbin0  9525  infrenegsupex  9596  iseqvalcbv  10459  m1expcl2  10544  facnn  10709  fac0  10710  4bc3eq4  10755  fihasheq0  10775  resqrexlemcalc1  11025  sqrt1  11057  sqrt4  11058  sqrt9  11059  infxrnegsupex  11273  isumss2  11403  geo2sum2  11525  geoihalfsum  11532  sin0  11739  efival  11742  ef01bndlem  11766  cos2bnd  11770  sin4lt0  11776  flodddiv4  11941  2prm  12129  znnen  12401  ennnfonelemhf1o  12416  setsslid  12515  ressressg  12536  metreslem  13919  retopbas  14062  sinhalfpilem  14251  sincos6thpi  14302  sincos3rdpi  14303  lgsdir2lem3  14470  lgseisenlem1  14489  lgseisenlem2  14490  2lgsoddprmlem2  14493