Theorem eqtr3i 2257

Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)

Hypotheses

Ref	Expression
eqtr3i.1	⊢ 𝐴 = 𝐵
eqtr3i.2	⊢ 𝐴 = 𝐶

Assertion

Ref	Expression
eqtr3i	⊢ 𝐵 = 𝐶

Proof of Theorem eqtr3i

Step	Hyp	Ref	Expression
1		eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
2	1	eqcomi 2238	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2255	1 ⊢ 𝐵 = 𝐶

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  3384  unundir  3385  inindi  3442  inindir  3443  difun1  3485  difabs  3489  notab  3495  dfrab2  3500  dif0  3584  difdifdirss  3599  tpidm13  3797  intmin2  3981  univ  4604  iunxpconst  4817  dmres  5066  rnresi  5126  cnvcnv  5222  rnresv  5229  cnvsn0  5238  cnvsn  5252  resdmres  5261  coi2  5286  coires1  5287  dfdm2  5304  isarep2  5450  ssimaex  5745  fnreseql  5795  fmptpr  5883  idref  5937  mpompt  6155  caov31  6254  xpexgALT  6341  cnvoprab  6445  frec0g  6643  unfiin  7201  xpfi  7207  endjusym  7402  halfnqq  7743  caucvgprlemm  8001  caucvgprprlemmu  8028  caucvgsr  8135  mvlladdi  8510  8th4div3  9479  nneoor  9703  nummac  9776  numadd  9778  numaddc  9779  nummul1c  9780  decbin0  9871  infrenegsupex  9949  xnn0nnen  10828  iseqvalcbv  10850  m1expcl2  10952  facnn  11119  fac0  11120  4bc3eq4  11166  fihasheq0  11186  resqrexlemcalc1  11730  sqrt1  11762  sqrt4  11763  sqrt9  11764  infxrnegsupex  11979  isumss2  12110  geo2sum2  12232  geoihalfsum  12239  sin0  12446  efival  12449  ef01bndlem  12473  cos2bnd  12477  sin4lt0  12484  flodddiv4  12653  2prm  12855  dec5dvds  13141  modxai  13145  mod2xi  13146  gcdi  13149  numexp2x  13154  decsplit  13158  ballotfilem2  13178  znnen  13239  ennnfonelemhf1o  13254  setsslid  13353  ressressg  13378  metreslem  15376  retopbas  15519  cnfldms  15532  sinhalfpilem  15787  sincos6thpi  15838  sincos3rdpi  15839  lgsdir2lem3  16034  lgseisenlem1  16074  lgseisenlem2  16075  lgsquadlem1  16081  lgsquadlem2  16082  2lgsoddprmlem2  16110