Theorem eqtr4i 2201

Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
eqtr4i	⊢ 𝐴 = 𝐶

Proof of Theorem eqtr4i

Step	Hyp	Ref	Expression
1		eqtr4i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqtr4i.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2181	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2198	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  3eqtr2i  2204  3eqtr2ri  2205  3eqtr4i  2208  3eqtr4ri  2209  rabab  2760  cbvralcsf  3121  cbvrexcsf  3122  cbvrabcsf  3124  dfin5  3138  dfdif2  3139  uneqin  3388  unrab  3408  inrab  3409  inrab2  3410  difrab  3411  dfrab3ss  3415  rabun2  3416  difidALT  3494  difdifdirss  3509  dfif3  3549  tpidm  3696  dfint2  3848  iunrab  3936  uniiun  3942  intiin  3943  0iin  3947  mptv  4102  xpundi  4684  xpundir  4685  resiun2  4929  resopab  4953  opabresid  4962  dfse2  5003  cnvun  5036  cnvin  5038  imaundir  5044  imainrect  5076  cnvcnv2  5084  cnvcnvres  5094  dmtpop  5106  rnsnopg  5109  rnco2  5138  dmco  5139  co01  5145  unidmrn  5163  dfdm2  5165  funimaexg  5302  dfmpt3  5340  mptun  5349  funcocnv2  5488  fnasrn  5696  fnasrng  5698  fpr  5700  fmptap  5708  riotav  5838  dmoprab  5958  rnoprab2  5961  mpov  5967  mpomptx  5968  abrexex2g  6123  abrexex2  6127  1stval2  6158  2ndval2  6159  fo1st  6160  fo2nd  6161  xp2  6176  dfoprab4f  6196  fmpoco  6219  tposmpo  6284  recsfval  6318  frecfnom  6404  freccllem  6405  frecfcllem  6407  frecsuclem  6409  df2o3  6433  o1p1e2  6471  ecqs  6599  qliftf  6622  erovlem  6629  mapsnf1o3  6699  ixp0x  6728  xpf1o  6846  djuunr  7067  dmaddpq  7380  dmmulpq  7381  enq0enq  7432  nqprlu  7548  m1p1sr  7761  m1m1sr  7762  caucvgsr  7803  dfcnqs  7842  3m1e2  9041  2p2e4  9048  3p2e5  9062  3p3e6  9063  4p2e6  9064  4p3e7  9065  4p4e8  9066  5p2e7  9067  5p3e8  9068  5p4e9  9069  6p2e8  9070  6p3e9  9071  7p2e9  9072  nn0supp  9230  nnzrab  9279  nn0zrab  9280  dec0u  9406  dec0h  9407  decsuc  9416  decsucc  9426  numma  9429  decma  9436  decmac  9437  decma2c  9438  decadd  9439  decaddc  9440  decmul1  9449  decmul1c  9450  decmul2c  9451  5p5e10  9456  6p4e10  9457  7p3e10  9460  8p2e10  9465  5t5e25  9488  6t6e36  9493  8t6e48  9504  nn0uz  9564  nnuz  9565  xaddcom  9863  ioomax  9950  iccmax  9951  ioopos  9952  ioorp  9953  fseq1p1m1  10096  fzo0to2pr  10220  fzo0to3tp  10221  frecfzennn  10428  irec  10622  sq10e99m1  10695  facnn  10709  fac0  10710  faclbnd2  10724  zfz1isolemsplit  10820  minmax  11240  xrminmax  11275  fisumrev2  11456  fsumparts  11480  fsumiun  11487  isumnn0nn  11503  fprod2d  11633  fprodle  11650  ege2le3  11681  cos1bnd  11769  efieq1re  11781  eirraplem  11786  phiprmpw  12224  unennn  12400  ennnfonelemjn  12405  qnnen  12434  strle1g  12567  quslem  12750  rmodislmod  13446  tgrest  13708  uniretop  14064  dvexp  14214  dvef  14227  cospi  14260  sincos6thpi  14302  lgsdir2lem2  14469  2lgsoddprmlem3c  14496  bj-omind  14725