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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  3eqtr3i  2260  3eqtr3ri  2261  unundi  3370  unundir  3371  inindi  3426  inindir  3427  difun1  3469  difabs  3473  notab  3479  dfrab2  3484  dif0  3567  difdifdirss  3581  tpidm13  3775  intmin2  3959  univ  4579  iunxpconst  4792  dmres  5040  rnresi  5100  cnvcnv  5196  rnresv  5203  cnvsn0  5212  cnvsn  5226  resdmres  5235  coi2  5260  coires1  5261  dfdm2  5278  isarep2  5424  ssimaex  5716  fnreseql  5766  fmptpr  5854  idref  5907  mpompt  6123  caov31  6222  xpexgALT  6304  cnvoprab  6408  frec0g  6606  unfiin  7161  xpfi  7167  endjusym  7355  halfnqq  7690  caucvgprlemm  7948  caucvgprprlemmu  7975  caucvgsr  8082  mvlladdi  8456  8th4div3  9422  nneoor  9643  nummac  9716  numadd  9718  numaddc  9719  nummul1c  9720  decbin0  9811  infrenegsupex  9889  xnn0nnen  10762  iseqvalcbv  10784  m1expcl2  10886  facnn  11052  fac0  11053  4bc3eq4  11098  fihasheq0  11118  resqrexlemcalc1  11654  sqrt1  11686  sqrt4  11687  sqrt9  11688  infxrnegsupex  11903  isumss2  12034  geo2sum2  12156  geoihalfsum  12163  sin0  12370  efival  12373  ef01bndlem  12397  cos2bnd  12401  sin4lt0  12408  flodddiv4  12577  2prm  12779  dec5dvds  13065  modxai  13069  mod2xi  13070  gcdi  13073  numexp2x  13078  decsplit  13082  znnen  13099  ennnfonelemhf1o  13114  setsslid  13213  ressressg  13238  metreslem  15191  retopbas  15334  cnfldms  15347  sinhalfpilem  15602  sincos6thpi  15653  sincos3rdpi  15654  lgsdir2lem3  15849  lgseisenlem1  15889  lgseisenlem2  15890  lgsquadlem1  15896  lgsquadlem2  15897  2lgsoddprmlem2  15925