Theorem eqtr3i 2105

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 2087	. 2 ⊢ 𝐵 = 𝐴
3		eqtr3i.2	. 2 ⊢ 𝐴 = 𝐶
4	2, 3	eqtri 2103	1 ⊢ 𝐵 = 𝐶

Syntax hints:   = wceq 1285

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-cleq 2076

This theorem is referenced by:  3eqtr3i  2111  3eqtr3ri  2112  unundi  3144  unundir  3145  inindi  3200  inindir  3201  difun1  3241  difabs  3245  notab  3251  dfrab2  3256  dif0  3331  difdifdirss  3344  tpidm13  3511  intmin2  3683  univ  4254  iunxpconst  4447  dmres  4681  opabresid  4710  rnresi  4733  cnvcnv  4824  rnresv  4831  cnvsn0  4840  cnvsn  4854  resdmres  4863  coi2  4888  coires1  4889  dfdm2  4903  isarep2  5038  ssimaex  5288  fnreseql  5331  fmptpr  5409  idref  5450  mpt2mpt  5649  caov31  5743  xpexgALT  5813  cnvoprab  5908  frec0g  6068  unfiin  6472  xpfi  6474  djuin  6563  halfnqq  6739  caucvgprlemm  6997  caucvgprprlemmu  7024  caucvgsr  7117  mvlladdi  7470  8th4div3  8394  nneoor  8607  nummac  8679  numadd  8681  numaddc  8682  nummul1c  8683  decbin0  8774  infrenegsupex  8840  iseqvalcbv  9608  m1expcl2  9672  facnn  9828  fac0  9829  4bc3eq4  9874  fihasheq0  9895  resqrexlemcalc1  10126  sqrt1  10158  sqrt4  10159  sqrt9  10160  flodddiv4  10566  2prm  10741  znnen  10843