Theorem eqtr4i 2213

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

Hypotheses

Ref	Expression
eqtr4i.1	|- A = B
eqtr4i.2	|- C = B

Assertion

Ref	Expression
eqtr4i	|- A = C

Proof of Theorem eqtr4i

Step	Hyp	Ref	Expression
1		eqtr4i.1	. 2 |- A = B
2		eqtr4i.2	. . 3 |- C = B
3	2	eqcomi 2193	. 2 |- B = C
4	1, 3	eqtri 2210	1 |- A = C

Syntax hints:   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171

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

This theorem is referenced by:  3eqtr2i  2216  3eqtr2ri  2217  3eqtr4i  2220  3eqtr4ri  2221  rabab  2777  cbvralcsf  3138  cbvrexcsf  3139  cbvrabcsf  3141  dfin5  3155  dfdif2  3156  uneqin  3405  unrab  3425  inrab  3426  inrab2  3427  difrab  3428  dfrab3ss  3432  rabun2  3433  difidALT  3511  difdifdirss  3526  dfif3  3566  tpidm  3716  dfint2  3868  iunrab  3956  uniiun  3962  intiin  3963  0iin  3967  mptv  4122  xpundi  4707  xpundir  4708  resiun2  4952  resopab  4976  opabresid  4985  dfse2  5026  cnvun  5059  cnvin  5061  imaundir  5067  imainrect  5099  cnvcnv2  5107  cnvcnvres  5117  dmtpop  5129  rnsnopg  5132  rnco2  5161  dmco  5162  co01  5168  unidmrn  5186  dfdm2  5188  funimaexg  5326  dfmpt3  5364  mptun  5373  funcocnv2  5512  fnasrn  5722  fnasrng  5724  fpr  5726  fmptap  5734  riotav  5865  dmoprab  5985  rnoprab2  5988  mpov  5994  mpomptx  5995  abrexex2g  6153  abrexex2  6157  1stval2  6188  2ndval2  6189  fo1st  6190  fo2nd  6191  xp2  6206  dfoprab4f  6226  fmpoco  6249  tposmpo  6314  recsfval  6348  frecfnom  6434  freccllem  6435  frecfcllem  6437  frecsuclem  6439  df2o3  6463  o1p1e2  6501  ecqs  6631  qliftf  6654  erovlem  6661  mapsnf1o3  6731  ixp0x  6760  xpf1o  6880  djuunr  7104  dmaddpq  7418  dmmulpq  7419  enq0enq  7470  nqprlu  7586  m1p1sr  7799  m1m1sr  7800  caucvgsr  7841  dfcnqs  7880  3m1e2  9080  2p2e4  9087  3p2e5  9101  3p3e6  9102  4p2e6  9103  4p3e7  9104  4p4e8  9105  5p2e7  9106  5p3e8  9107  5p4e9  9108  6p2e8  9109  6p3e9  9110  7p2e9  9111  nn0supp  9269  nnzrab  9318  nn0zrab  9319  dec0u  9445  dec0h  9446  decsuc  9455  decsucc  9465  numma  9468  decma  9475  decmac  9476  decma2c  9477  decadd  9478  decaddc  9479  decmul1  9488  decmul1c  9489  decmul2c  9490  5p5e10  9495  6p4e10  9496  7p3e10  9499  8p2e10  9504  5t5e25  9527  6t6e36  9532  8t6e48  9543  nn0uz  9604  nnuz  9605  xaddcom  9903  ioomax  9990  iccmax  9991  ioopos  9992  ioorp  9993  fseq1p1m1  10136  fzo0to2pr  10260  fzo0to3tp  10261  frecfzennn  10469  irec  10666  sq10e99m1  10740  facnn  10754  fac0  10755  faclbnd2  10769  zfz1isolemsplit  10865  minmax  11285  xrminmax  11320  fisumrev2  11501  fsumparts  11525  fsumiun  11532  isumnn0nn  11548  fprod2d  11678  fprodle  11695  ege2le3  11726  cos1bnd  11814  efieq1re  11826  eirraplem  11831  phiprmpw  12271  4sqlem11  12450  4sqlem19  12458  unennn  12465  ennnfonelemjn  12470  qnnen  12499  strle1g  12635  quslem  12818  rmodislmod  13710  tgrest  14190  uniretop  14546  dvexp  14713  dvef  14726  cospi  14759  sincos6thpi  14801  lgsdir2lem2  14969  2lgsoddprmlem3c  14996  bj-omind  15225