Theorem eqtr3i 2261

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

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  3eqtr3i  2267  3eqtr3ri  2268  unundi  3390  unundir  3391  inindi  3448  inindir  3449  difun1  3491  difabs  3495  notab  3503  dfrab2  3508  dif0  3596  difdifdirss  3612  tpidm13  3811  intmin2  3996  univ  4622  iunxpconst  4835  dmres  5084  rnresi  5144  cnvcnv  5240  rnresv  5247  cnvsn0  5256  cnvsn  5270  resdmres  5279  coi2  5304  coires1  5305  dfdm2  5322  isarep2  5468  ssimaex  5764  fnreseql  5819  fmptpr  5907  idref  5962  mpompt  6180  caov31  6279  xpexgALT  6366  cnvoprab  6470  frec0g  6668  unfiin  7233  xpfi  7239  endjusym  7436  halfnqq  7777  caucvgprlemm  8035  caucvgprprlemmu  8062  caucvgsr  8169  mvlladdi  8545  8th4div3  9528  nneoor  9752  nummac  9830  numadd  9832  numaddc  9833  nummul1c  9834  decbin0  9925  infrenegsupex  10003  fz00m1  10461  xnn0nnen  10887  iseqvalcbv  10909  m1expcl2  11011  facnn  11179  fac0  11180  4bc3eq4  11226  fihasheq0  11246  resqrexlemcalc1  11794  sqrt1  11826  sqrt4  11827  sqrt9  11828  infxrnegsupex  12045  isumss2  12176  geo2sum2  12298  geoihalfsum  12305  sin0  12512  efival  12515  ef01bndlem  12539  cos2bnd  12543  sin4lt0  12550  flodddiv4  12719  2prm  12921  dec5dvds  13211  modxai  13215  mod2xi  13216  mod2xnegi  13218  gcdi  13220  numexp2x  13225  decsplit  13229  ballotfilem2  13277  znnen  13338  ennnfonelemhf1o  13353  setsslid  13452  ressressg  13478  metreslem  15530  retopbas  15673  cnfldms  15686  sinhalfpilem  15942  sincos6thpi  15993  sincos3rdpi  15994  log2tlbndlog2  16139  log2ublem2  16141  log2ublog2  16143  ppiqub  16194  lgsdir2lem3  16247  lgseisenlem1  16287  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  2lgsoddprmlem2  16323