Theorem eqtr4i 2258

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 2238	. 2 ⊢ 𝐵 = 𝐶
4	1, 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:  3eqtr2i  2261  3eqtr2ri  2262  3eqtr4i  2265  3eqtr4ri  2266  rabab  2837  cbvralcsf  3204  cbvrexcsf  3205  cbvrabcsf  3207  dfin5  3221  dfdif2  3222  uneqin  3476  unrab  3496  inrab  3497  inrab2  3498  difrab  3499  dfrab3ss  3503  rabun2  3504  difidALT  3582  difdifdirss  3598  dfif3  3640  tpidm  3798  dfint2  3956  iunrab  4044  uniiun  4050  intiin  4051  0iin  4055  mptv  4212  xpundi  4811  xpundir  4812  resiun2  5063  resopab  5087  mptresid  5097  dfse2  5140  cnvun  5173  cnvin  5175  imaundir  5181  imainrect  5213  cnvcnv2  5221  cnvcnvres  5231  dmtpop  5243  rnsnopg  5246  rnco2  5275  dmco  5276  co01  5282  unidmrn  5300  dfdm2  5302  funimaexg  5445  dfmpt3  5486  mptun  5495  funcocnv2  5644  fnasrn  5861  fnasrng  5863  fpr  5871  fmptap  5879  riotav  6017  dmoprab  6142  rnoprab2  6145  mpov  6151  mpomptx  6152  abrexex2g  6322  abrexex2  6326  1stval2  6362  2ndval2  6363  fo1st  6364  fo2nd  6365  xp2  6380  dfoprab4f  6400  fmpoco  6425  tposmpo  6525  recsfval  6559  frecfnom  6645  freccllem  6646  frecfcllem  6648  frecsuclem  6650  df2o3  6675  o1p1e2  6714  ecqs  6844  qliftf  6867  erovlem  6874  mapsnf1o3  6945  ixp0x  6974  xpf1o  7110  djuunr  7370  dmaddpq  7710  dmmulpq  7711  enq0enq  7762  nqprlu  7878  m1p1sr  8091  m1m1sr  8092  caucvgsr  8133  dfcnqs  8172  3m1e2  9374  2p2e4  9381  3p2e5  9396  3p3e6  9397  4p2e6  9398  4p3e7  9399  4p4e8  9400  5p2e7  9401  5p3e8  9402  5p4e9  9403  6p2e8  9404  6p3e9  9405  7p2e9  9406  nn0supp  9569  nnzrab  9618  nn0zrab  9619  dec0u  9747  dec0h  9748  decsuc  9757  decsucc  9767  numma  9770  decma  9777  decmac  9778  decma2c  9779  decadd  9780  decaddc  9781  decmul1  9790  decmul1c  9791  decmul2c  9792  5p5e10  9797  6p4e10  9798  7p3e10  9801  8p2e10  9806  5t5e25  9829  6t6e36  9834  8t6e48  9845  nn0uz  9907  nnuz  9908  xaddcom  10213  ioomax  10300  iccmax  10301  ioopos  10302  ioorp  10303  fseq1p1m1  10450  fzo0to2pr  10585  fzo0to3tp  10586  frecfzennn  10812  irec  11025  sq10e99m1  11100  facnn  11114  fac0  11115  faclbnd2  11129  zfz1isolemsplit  11235  minmax  11940  xrminmax  11975  fisumrev2  12157  fsumparts  12181  fsumiun  12188  isumnn0nn  12204  fprod2d  12334  fprodle  12351  ege2le3  12382  cos1bnd  12470  efieq1re  12483  eirraplem  12488  3dvds  12575  m1bits  12671  phiprmpw  12944  4sqlem11  13124  4sqlem19  13132  dec5dvds  13135  decsplit1  13151  ballotfilemfval  13173  ballotfilemth  13225  unennn  13232  ennnfonelemjn  13237  qnnen  13266  strle1g  13403  quslem  13588  gfsump1  14108  rmodislmod  14625  tgrest  15160  uniretop  15516  cnfldtopn  15530  dvexp  15702  dvef  15718  elply2  15726  cospi  15791  sincos6thpi  15833  lgsdir2lem2  16028  lgsquadlem2  16077  lgsquad2lem2  16081  2lgsoddprmlem3c  16108  konigsbergumgr  16608  konigsberglem1  16609  konigsberglem2  16610  bj-omind  16830