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  5695  fnreseql  5745  fmptpr  5831  idref  5880  mpompt  6096  caov31  6195  xpexgALT  6278  cnvoprab  6380  frec0g  6543  unfiin  7088  xpfi  7094  endjusym  7263  halfnqq  7597  caucvgprlemm  7855  caucvgprprlemmu  7882  caucvgsr  7989  mvlladdi  8364  8th4div3  9330  nneoor  9549  nummac  9622  numadd  9624  numaddc  9625  nummul1c  9626  decbin0  9717  infrenegsupex  9789  xnn0nnen  10659  iseqvalcbv  10681  m1expcl2  10783  facnn  10949  fac0  10950  4bc3eq4  10995  fihasheq0  11015  resqrexlemcalc1  11525  sqrt1  11557  sqrt4  11558  sqrt9  11559  infxrnegsupex  11774  isumss2  11904  geo2sum2  12026  geoihalfsum  12033  sin0  12240  efival  12243  ef01bndlem  12267  cos2bnd  12271  sin4lt0  12278  flodddiv4  12447  2prm  12649  dec5dvds  12935  modxai  12939  mod2xi  12940  gcdi  12943  numexp2x  12948  decsplit  12952  znnen  12969  ennnfonelemhf1o  12984  setsslid  13083  ressressg  13108  metreslem  15054  retopbas  15197  cnfldms  15210  sinhalfpilem  15465  sincos6thpi  15516  sincos3rdpi  15517  lgsdir2lem3  15709  lgseisenlem1  15749  lgseisenlem2  15750  lgsquadlem1  15756  lgsquadlem2  15757  2lgsoddprmlem2  15785