Theorem eqtr3i 2257

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 2238	. 2 |- B = A
3		eqtr3i.2	. 2 |- A = C
4	2, 3	eqtri 2255	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 2216

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

This theorem is referenced by:  3eqtr3i  2263  3eqtr3ri  2264  unundi  3382  unundir  3383  inindi  3440  inindir  3441  difun1  3483  difabs  3487  notab  3493  dfrab2  3498  dif0  3581  difdifdirss  3596  tpidm13  3793  intmin2  3977  univ  4599  iunxpconst  4812  dmres  5061  rnresi  5121  cnvcnv  5217  rnresv  5224  cnvsn0  5233  cnvsn  5247  resdmres  5256  coi2  5281  coires1  5282  dfdm2  5299  isarep2  5445  ssimaex  5740  fnreseql  5790  fmptpr  5878  idref  5931  mpompt  6147  caov31  6246  xpexgALT  6328  cnvoprab  6432  frec0g  6630  unfiin  7188  xpfi  7194  endjusym  7389  halfnqq  7727  caucvgprlemm  7985  caucvgprprlemmu  8012  caucvgsr  8119  mvlladdi  8493  8th4div3  9459  nneoor  9683  nummac  9756  numadd  9758  numaddc  9759  nummul1c  9760  decbin0  9851  infrenegsupex  9929  xnn0nnen  10803  iseqvalcbv  10825  m1expcl2  10927  facnn  11093  fac0  11094  4bc3eq4  11140  fihasheq0  11160  resqrexlemcalc1  11703  sqrt1  11735  sqrt4  11736  sqrt9  11737  infxrnegsupex  11952  isumss2  12083  geo2sum2  12205  geoihalfsum  12212  sin0  12419  efival  12422  ef01bndlem  12446  cos2bnd  12450  sin4lt0  12457  flodddiv4  12626  2prm  12828  dec5dvds  13114  modxai  13118  mod2xi  13119  gcdi  13122  numexp2x  13127  decsplit  13131  ballotfilem2  13149  znnen  13166  ennnfonelemhf1o  13181  setsslid  13280  ressressg  13305  metreslem  15262  retopbas  15405  cnfldms  15418  sinhalfpilem  15673  sincos6thpi  15724  sincos3rdpi  15725  lgsdir2lem3  15920  lgseisenlem1  15960  lgseisenlem2  15961  lgsquadlem1  15967  lgsquadlem2  15968  2lgsoddprmlem2  15996