Theorem eqtr3i 2216

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

Syntax hints:   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  3eqtr3i  2222  3eqtr3ri  2223  unundi  3321  unundir  3322  inindi  3377  inindir  3378  difun1  3420  difabs  3424  notab  3430  dfrab2  3435  dif0  3518  difdifdirss  3532  tpidm13  3719  intmin2  3897  univ  4508  iunxpconst  4720  dmres  4964  rnresi  5023  cnvcnv  5119  rnresv  5126  cnvsn0  5135  cnvsn  5149  resdmres  5158  coi2  5183  coires1  5184  dfdm2  5201  isarep2  5342  ssimaex  5619  fnreseql  5669  fmptpr  5751  idref  5800  mpompt  6011  caov31  6110  xpexgALT  6187  cnvoprab  6289  frec0g  6452  unfiin  6984  xpfi  6988  endjusym  7157  halfnqq  7472  caucvgprlemm  7730  caucvgprprlemmu  7757  caucvgsr  7864  mvlladdi  8239  8th4div3  9204  nneoor  9422  nummac  9495  numadd  9497  numaddc  9498  nummul1c  9499  decbin0  9590  infrenegsupex  9662  xnn0nnen  10511  iseqvalcbv  10533  m1expcl2  10635  facnn  10801  fac0  10802  4bc3eq4  10847  fihasheq0  10867  resqrexlemcalc1  11161  sqrt1  11193  sqrt4  11194  sqrt9  11195  infxrnegsupex  11409  isumss2  11539  geo2sum2  11661  geoihalfsum  11668  sin0  11875  efival  11878  ef01bndlem  11902  cos2bnd  11906  sin4lt0  11913  flodddiv4  12078  2prm  12268  znnen  12558  ennnfonelemhf1o  12573  setsslid  12672  ressressg  12696  metreslem  14559  retopbas  14702  cnfldms  14715  sinhalfpilem  14967  sincos6thpi  15018  sincos3rdpi  15019  lgsdir2lem3  15187  lgseisenlem1  15227  lgseisenlem2  15228  lgsquadlem1  15234  lgsquadlem2  15235  2lgsoddprmlem2  15263