Theorem eqtr3i 2255

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  3eqtr3i  2261  3eqtr3ri  2262  unundi  3379  unundir  3380  inindi  3437  inindir  3438  difun1  3480  difabs  3484  notab  3490  dfrab2  3495  dif0  3578  difdifdirss  3593  tpidm13  3790  intmin2  3974  univ  4596  iunxpconst  4809  dmres  5058  rnresi  5118  cnvcnv  5214  rnresv  5221  cnvsn0  5230  cnvsn  5244  resdmres  5253  coi2  5278  coires1  5279  dfdm2  5296  isarep2  5442  ssimaex  5737  fnreseql  5787  fmptpr  5875  idref  5928  mpompt  6144  caov31  6243  xpexgALT  6325  cnvoprab  6429  frec0g  6627  unfiin  7185  xpfi  7191  endjusym  7386  halfnqq  7724  caucvgprlemm  7982  caucvgprprlemmu  8009  caucvgsr  8116  mvlladdi  8490  8th4div3  9456  nneoor  9679  nummac  9752  numadd  9754  numaddc  9755  nummul1c  9756  decbin0  9847  infrenegsupex  9925  xnn0nnen  10798  iseqvalcbv  10820  m1expcl2  10922  facnn  11088  fac0  11089  4bc3eq4  11134  fihasheq0  11154  resqrexlemcalc1  11695  sqrt1  11727  sqrt4  11728  sqrt9  11729  infxrnegsupex  11944  isumss2  12075  geo2sum2  12197  geoihalfsum  12204  sin0  12411  efival  12414  ef01bndlem  12438  cos2bnd  12442  sin4lt0  12449  flodddiv4  12618  2prm  12820  dec5dvds  13106  modxai  13110  mod2xi  13111  gcdi  13114  numexp2x  13119  decsplit  13123  znnen  13141  ennnfonelemhf1o  13156  setsslid  13255  ressressg  13280  metreslem  15237  retopbas  15380  cnfldms  15393  sinhalfpilem  15648  sincos6thpi  15699  sincos3rdpi  15700  lgsdir2lem3  15895  lgseisenlem1  15935  lgseisenlem2  15936  lgsquadlem1  15942  lgsquadlem2  15943  2lgsoddprmlem2  15971