Theorem eqtr3i 2252

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr3i  2258  3eqtr3ri  2259  unundi  3365  unundir  3366  inindi  3421  inindir  3422  difun1  3464  difabs  3468  notab  3474  dfrab2  3479  dif0  3562  difdifdirss  3576  tpidm13  3766  intmin2  3949  univ  4567  iunxpconst  4779  dmres  5026  rnresi  5085  cnvcnv  5181  rnresv  5188  cnvsn0  5197  cnvsn  5211  resdmres  5220  coi2  5245  coires1  5246  dfdm2  5263  isarep2  5408  ssimaex  5697  fnreseql  5747  fmptpr  5835  idref  5886  mpompt  6102  caov31  6201  xpexgALT  6284  cnvoprab  6386  frec0g  6549  unfiin  7099  xpfi  7105  endjusym  7274  halfnqq  7608  caucvgprlemm  7866  caucvgprprlemmu  7893  caucvgsr  8000  mvlladdi  8375  8th4div3  9341  nneoor  9560  nummac  9633  numadd  9635  numaddc  9636  nummul1c  9637  decbin0  9728  infrenegsupex  9801  xnn0nnen  10671  iseqvalcbv  10693  m1expcl2  10795  facnn  10961  fac0  10962  4bc3eq4  11007  fihasheq0  11027  resqrexlemcalc1  11541  sqrt1  11573  sqrt4  11574  sqrt9  11575  infxrnegsupex  11790  isumss2  11920  geo2sum2  12042  geoihalfsum  12049  sin0  12256  efival  12259  ef01bndlem  12283  cos2bnd  12287  sin4lt0  12294  flodddiv4  12463  2prm  12665  dec5dvds  12951  modxai  12955  mod2xi  12956  gcdi  12959  numexp2x  12964  decsplit  12968  znnen  12985  ennnfonelemhf1o  13000  setsslid  13099  ressressg  13124  metreslem  15070  retopbas  15213  cnfldms  15226  sinhalfpilem  15481  sincos6thpi  15532  sincos3rdpi  15533  lgsdir2lem3  15725  lgseisenlem1  15765  lgseisenlem2  15766  lgsquadlem1  15772  lgsquadlem2  15773  2lgsoddprmlem2  15801