Theorem eqtr3i 2254

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

Syntax hints:   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  3eqtr3i  2260  3eqtr3ri  2261  unundi  3368  unundir  3369  inindi  3424  inindir  3425  difun1  3467  difabs  3471  notab  3477  dfrab2  3482  dif0  3565  difdifdirss  3579  tpidm13  3771  intmin2  3954  univ  4573  iunxpconst  4786  dmres  5034  rnresi  5093  cnvcnv  5189  rnresv  5196  cnvsn0  5205  cnvsn  5219  resdmres  5228  coi2  5253  coires1  5254  dfdm2  5271  isarep2  5417  ssimaex  5707  fnreseql  5757  fmptpr  5846  idref  5897  mpompt  6113  caov31  6212  xpexgALT  6295  cnvoprab  6399  frec0g  6563  unfiin  7118  xpfi  7124  endjusym  7295  halfnqq  7630  caucvgprlemm  7888  caucvgprprlemmu  7915  caucvgsr  8022  mvlladdi  8397  8th4div3  9363  nneoor  9582  nummac  9655  numadd  9657  numaddc  9658  nummul1c  9659  decbin0  9750  infrenegsupex  9828  xnn0nnen  10700  iseqvalcbv  10722  m1expcl2  10824  facnn  10990  fac0  10991  4bc3eq4  11036  fihasheq0  11056  resqrexlemcalc1  11592  sqrt1  11624  sqrt4  11625  sqrt9  11626  infxrnegsupex  11841  isumss2  11972  geo2sum2  12094  geoihalfsum  12101  sin0  12308  efival  12311  ef01bndlem  12335  cos2bnd  12339  sin4lt0  12346  flodddiv4  12515  2prm  12717  dec5dvds  13003  modxai  13007  mod2xi  13008  gcdi  13011  numexp2x  13016  decsplit  13020  znnen  13037  ennnfonelemhf1o  13052  setsslid  13151  ressressg  13176  metreslem  15123  retopbas  15266  cnfldms  15279  sinhalfpilem  15534  sincos6thpi  15585  sincos3rdpi  15586  lgsdir2lem3  15778  lgseisenlem1  15818  lgseisenlem2  15819  lgsquadlem1  15825  lgsquadlem2  15826  2lgsoddprmlem2  15854