Theorem eqtr4i 2228

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

Syntax hints:   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  3eqtr2i  2231  3eqtr2ri  2232  3eqtr4i  2235  3eqtr4ri  2236  rabab  2792  cbvralcsf  3155  cbvrexcsf  3156  cbvrabcsf  3158  dfin5  3172  dfdif2  3173  uneqin  3423  unrab  3443  inrab  3444  inrab2  3445  difrab  3446  dfrab3ss  3450  rabun2  3451  difidALT  3529  difdifdirss  3544  dfif3  3583  tpidm  3734  dfint2  3886  iunrab  3974  uniiun  3980  intiin  3981  0iin  3985  mptv  4140  xpundi  4730  xpundir  4731  resiun2  4978  resopab  5002  mptresid  5012  dfse2  5054  cnvun  5087  cnvin  5089  imaundir  5095  imainrect  5127  cnvcnv2  5135  cnvcnvres  5145  dmtpop  5157  rnsnopg  5160  rnco2  5189  dmco  5190  co01  5196  unidmrn  5214  dfdm2  5216  funimaexg  5357  dfmpt3  5397  mptun  5406  funcocnv2  5546  fnasrn  5757  fnasrng  5759  fpr  5765  fmptap  5773  riotav  5904  dmoprab  6025  rnoprab2  6028  mpov  6034  mpomptx  6035  abrexex2g  6204  abrexex2  6208  1stval2  6240  2ndval2  6241  fo1st  6242  fo2nd  6243  xp2  6258  dfoprab4f  6278  fmpoco  6301  tposmpo  6366  recsfval  6400  frecfnom  6486  freccllem  6487  frecfcllem  6489  frecsuclem  6491  df2o3  6515  o1p1e2  6553  ecqs  6683  qliftf  6706  erovlem  6713  mapsnf1o3  6783  ixp0x  6812  xpf1o  6940  djuunr  7167  dmaddpq  7491  dmmulpq  7492  enq0enq  7543  nqprlu  7659  m1p1sr  7872  m1m1sr  7873  caucvgsr  7914  dfcnqs  7953  3m1e2  9155  2p2e4  9162  3p2e5  9177  3p3e6  9178  4p2e6  9179  4p3e7  9180  4p4e8  9181  5p2e7  9182  5p3e8  9183  5p4e9  9184  6p2e8  9185  6p3e9  9186  7p2e9  9187  nn0supp  9346  nnzrab  9395  nn0zrab  9396  dec0u  9523  dec0h  9524  decsuc  9533  decsucc  9543  numma  9546  decma  9553  decmac  9554  decma2c  9555  decadd  9556  decaddc  9557  decmul1  9566  decmul1c  9567  decmul2c  9568  5p5e10  9573  6p4e10  9574  7p3e10  9577  8p2e10  9582  5t5e25  9605  6t6e36  9610  8t6e48  9621  nn0uz  9682  nnuz  9683  xaddcom  9982  ioomax  10069  iccmax  10070  ioopos  10071  ioorp  10072  fseq1p1m1  10215  fzo0to2pr  10345  fzo0to3tp  10346  frecfzennn  10569  irec  10782  sq10e99m1  10856  facnn  10870  fac0  10871  faclbnd2  10885  zfz1isolemsplit  10981  minmax  11483  xrminmax  11518  fisumrev2  11699  fsumparts  11723  fsumiun  11730  isumnn0nn  11746  fprod2d  11876  fprodle  11893  ege2le3  11924  cos1bnd  12012  efieq1re  12025  eirraplem  12030  3dvds  12117  m1bits  12213  phiprmpw  12486  4sqlem11  12666  4sqlem19  12674  dec5dvds  12677  decsplit1  12693  unennn  12710  ennnfonelemjn  12715  qnnen  12744  strle1g  12880  quslem  13098  rmodislmod  14055  tgrest  14583  uniretop  14939  cnfldtopn  14953  dvexp  15125  dvef  15141  elply2  15149  cospi  15214  sincos6thpi  15256  lgsdir2lem2  15448  lgsquadlem2  15497  lgsquad2lem2  15501  2lgsoddprmlem3c  15528  bj-omind  15803