Theorem eqtr3i 2261

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 2242	. 2 |- B = A
3		eqtr3i.2	. 2 |- A = C
4	2, 3	eqtri 2259	1 |- B = C

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr3i  2267  3eqtr3ri  2268  unundi  3390  unundir  3391  inindi  3448  inindir  3449  difun1  3491  difabs  3495  notab  3503  dfrab2  3508  dif0  3596  difdifdirss  3612  tpidm13  3811  intmin2  3996  univ  4624  iunxpconst  4837  dmres  5086  rnresi  5147  cnvcnv  5243  rnresv  5250  cnvsn0  5259  cnvsn  5273  resdmres  5282  coi2  5307  coires1  5308  dfdm2  5325  isarep2  5471  ssimaex  5767  fnreseql  5822  fmptpr  5910  idref  5965  mpompt  6183  caov31  6282  xpexgALT  6370  cnvoprab  6474  frec0g  6672  unfiin  7237  xpfi  7243  endjusym  7442  halfnqq  7783  caucvgprlemm  8041  caucvgprprlemmu  8068  caucvgsr  8175  mvlladdi  8551  8th4div3  9535  nneoor  9759  nummac  9837  numadd  9839  numaddc  9840  nummul1c  9841  decbin0  9932  infrenegsupex  10010  fz00m1  10468  xnn0nnen  10895  iseqvalcbv  10917  m1expcl2  11019  facnn  11187  fac0  11188  4bc3eq4  11234  fihasheq0  11254  resqrexlemcalc1  11802  sqrt1  11834  sqrt4  11835  sqrt9  11836  infxrnegsupex  12054  isumss2  12185  geo2sum2  12307  geoihalfsum  12314  sin0  12521  efival  12524  ef01bndlem  12548  cos2bnd  12552  sin4lt0  12559  flodddiv4  12728  2prm  12930  dec5dvds  13220  modxai  13224  mod2xi  13225  mod2xnegi  13227  gcdi  13229  numexp2x  13234  decsplit  13238  ballotfilem2  13286  znnen  13347  ennnfonelemhf1o  13362  setsslid  13461  ressressg  13488  metreslem  15606  retopbas  15749  cnfldms  15762  sinhalfpilem  16018  sincos6thpi  16069  sincos3rdpi  16070  log2tlbndlog2  16220  log2ublem2  16222  log2ublog2  16224  cht2  16276  ppiqub  16293  bposlem6  16316  bposlem8  16318  bposlem9  16319  lgsdir2lem3  16354  lgseisenlem1  16394  lgseisenlem2  16395  lgsquadlem1  16401  lgsquadlem2  16402  2lgsoddprmlem2  16430