Theorem eqtr3i 2228

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  3eqtr3i  2234  3eqtr3ri  2235  unundi  3334  unundir  3335  inindi  3390  inindir  3391  difun1  3433  difabs  3437  notab  3443  dfrab2  3448  dif0  3531  difdifdirss  3545  tpidm13  3733  intmin2  3911  univ  4524  iunxpconst  4736  dmres  4981  rnresi  5040  cnvcnv  5136  rnresv  5143  cnvsn0  5152  cnvsn  5166  resdmres  5175  coi2  5200  coires1  5201  dfdm2  5218  isarep2  5362  ssimaex  5642  fnreseql  5692  fmptpr  5778  idref  5827  mpompt  6039  caov31  6138  xpexgALT  6220  cnvoprab  6322  frec0g  6485  unfiin  7025  xpfi  7031  endjusym  7200  halfnqq  7525  caucvgprlemm  7783  caucvgprprlemmu  7810  caucvgsr  7917  mvlladdi  8292  8th4div3  9258  nneoor  9477  nummac  9550  numadd  9552  numaddc  9553  nummul1c  9554  decbin0  9645  infrenegsupex  9717  xnn0nnen  10584  iseqvalcbv  10606  m1expcl2  10708  facnn  10874  fac0  10875  4bc3eq4  10920  fihasheq0  10940  resqrexlemcalc1  11358  sqrt1  11390  sqrt4  11391  sqrt9  11392  infxrnegsupex  11607  isumss2  11737  geo2sum2  11859  geoihalfsum  11866  sin0  12073  efival  12076  ef01bndlem  12100  cos2bnd  12104  sin4lt0  12111  flodddiv4  12280  2prm  12482  dec5dvds  12768  modxai  12772  mod2xi  12773  gcdi  12776  numexp2x  12781  decsplit  12785  znnen  12802  ennnfonelemhf1o  12817  setsslid  12916  ressressg  12940  metreslem  14885  retopbas  15028  cnfldms  15041  sinhalfpilem  15296  sincos6thpi  15347  sincos3rdpi  15348  lgsdir2lem3  15540  lgseisenlem1  15580  lgseisenlem2  15581  lgsquadlem1  15587  lgsquadlem2  15588  2lgsoddprmlem2  15616