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  3583  difdifdirss  3598  tpidm13  3796  intmin2  3980  univ  4602  iunxpconst  4815  dmres  5064  rnresi  5124  cnvcnv  5220  rnresv  5227  cnvsn0  5236  cnvsn  5250  resdmres  5259  coi2  5284  coires1  5285  dfdm2  5302  isarep2  5448  ssimaex  5743  fnreseql  5793  fmptpr  5881  idref  5935  mpompt  6153  caov31  6252  xpexgALT  6339  cnvoprab  6443  frec0g  6641  unfiin  7199  xpfi  7205  endjusym  7400  halfnqq  7741  caucvgprlemm  7999  caucvgprprlemmu  8026  caucvgsr  8133  mvlladdi  8507  8th4div3  9474  nneoor  9698  nummac  9771  numadd  9773  numaddc  9774  nummul1c  9775  decbin0  9866  infrenegsupex  9944  xnn0nnen  10823  iseqvalcbv  10845  m1expcl2  10947  facnn  11114  fac0  11115  4bc3eq4  11161  fihasheq0  11181  resqrexlemcalc1  11724  sqrt1  11756  sqrt4  11757  sqrt9  11758  infxrnegsupex  11973  isumss2  12104  geo2sum2  12226  geoihalfsum  12233  sin0  12440  efival  12443  ef01bndlem  12467  cos2bnd  12471  sin4lt0  12478  flodddiv4  12647  2prm  12849  dec5dvds  13135  modxai  13139  mod2xi  13140  gcdi  13143  numexp2x  13148  decsplit  13152  ballotfilem2  13172  znnen  13233  ennnfonelemhf1o  13248  setsslid  13347  ressressg  13372  metreslem  15371  retopbas  15514  cnfldms  15527  sinhalfpilem  15782  sincos6thpi  15833  sincos3rdpi  15834  lgsdir2lem3  16029  lgseisenlem1  16069  lgseisenlem2  16070  lgsquadlem1  16076  lgsquadlem2  16077  2lgsoddprmlem2  16105