Theorem eqtr4i 2253

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  3eqtr2i  2256  3eqtr2ri  2257  3eqtr4i  2260  3eqtr4ri  2261  rabab  2821  cbvralcsf  3187  cbvrexcsf  3188  cbvrabcsf  3190  dfin5  3204  dfdif2  3205  uneqin  3455  unrab  3475  inrab  3476  inrab2  3477  difrab  3478  dfrab3ss  3482  rabun2  3483  difidALT  3561  difdifdirss  3576  dfif3  3616  tpidm  3768  dfint2  3924  iunrab  4012  uniiun  4018  intiin  4019  0iin  4023  mptv  4180  xpundi  4774  xpundir  4775  resiun2  5024  resopab  5048  mptresid  5058  dfse2  5100  cnvun  5133  cnvin  5135  imaundir  5141  imainrect  5173  cnvcnv2  5181  cnvcnvres  5191  dmtpop  5203  rnsnopg  5206  rnco2  5235  dmco  5236  co01  5242  unidmrn  5260  dfdm2  5262  funimaexg  5404  dfmpt3  5445  mptun  5454  funcocnv2  5596  fnasrn  5812  fnasrng  5814  fpr  5820  fmptap  5828  riotav  5959  dmoprab  6084  rnoprab2  6087  mpov  6093  mpomptx  6094  abrexex2g  6263  abrexex2  6267  1stval2  6299  2ndval2  6300  fo1st  6301  fo2nd  6302  xp2  6317  dfoprab4f  6337  fmpoco  6360  tposmpo  6425  recsfval  6459  frecfnom  6545  freccllem  6546  frecfcllem  6548  frecsuclem  6550  df2o3  6574  o1p1e2  6612  ecqs  6742  qliftf  6765  erovlem  6772  mapsnf1o3  6842  ixp0x  6871  xpf1o  7001  djuunr  7229  dmaddpq  7562  dmmulpq  7563  enq0enq  7614  nqprlu  7730  m1p1sr  7943  m1m1sr  7944  caucvgsr  7985  dfcnqs  8024  3m1e2  9226  2p2e4  9233  3p2e5  9248  3p3e6  9249  4p2e6  9250  4p3e7  9251  4p4e8  9252  5p2e7  9253  5p3e8  9254  5p4e9  9255  6p2e8  9256  6p3e9  9257  7p2e9  9258  nn0supp  9417  nnzrab  9466  nn0zrab  9467  dec0u  9594  dec0h  9595  decsuc  9604  decsucc  9614  numma  9617  decma  9624  decmac  9625  decma2c  9626  decadd  9627  decaddc  9628  decmul1  9637  decmul1c  9638  decmul2c  9639  5p5e10  9644  6p4e10  9645  7p3e10  9648  8p2e10  9653  5t5e25  9676  6t6e36  9681  8t6e48  9692  nn0uz  9753  nnuz  9754  xaddcom  10053  ioomax  10140  iccmax  10141  ioopos  10142  ioorp  10143  fseq1p1m1  10286  fzo0to2pr  10419  fzo0to3tp  10420  frecfzennn  10643  irec  10856  sq10e99m1  10930  facnn  10944  fac0  10945  faclbnd2  10959  zfz1isolemsplit  11055  minmax  11736  xrminmax  11771  fisumrev2  11952  fsumparts  11976  fsumiun  11983  isumnn0nn  11999  fprod2d  12129  fprodle  12146  ege2le3  12177  cos1bnd  12265  efieq1re  12278  eirraplem  12283  3dvds  12370  m1bits  12466  phiprmpw  12739  4sqlem11  12919  4sqlem19  12927  dec5dvds  12930  decsplit1  12946  unennn  12963  ennnfonelemjn  12968  qnnen  12997  strle1g  13134  quslem  13352  rmodislmod  14309  tgrest  14837  uniretop  15193  cnfldtopn  15207  dvexp  15379  dvef  15395  elply2  15403  cospi  15468  sincos6thpi  15510  lgsdir2lem2  15702  lgsquadlem2  15751  lgsquad2lem2  15755  2lgsoddprmlem3c  15782  bj-omind  16255