Theorem eqtr4i 2217

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 2197	. 2 |- B = C
4	1, 3	eqtri 2214	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 2175

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

This theorem is referenced by:  3eqtr2i  2220  3eqtr2ri  2221  3eqtr4i  2224  3eqtr4ri  2225  rabab  2781  cbvralcsf  3143  cbvrexcsf  3144  cbvrabcsf  3146  dfin5  3160  dfdif2  3161  uneqin  3410  unrab  3430  inrab  3431  inrab2  3432  difrab  3433  dfrab3ss  3437  rabun2  3438  difidALT  3516  difdifdirss  3531  dfif3  3570  tpidm  3720  dfint2  3872  iunrab  3960  uniiun  3966  intiin  3967  0iin  3971  mptv  4126  xpundi  4715  xpundir  4716  resiun2  4962  resopab  4986  mptresid  4996  dfse2  5038  cnvun  5071  cnvin  5073  imaundir  5079  imainrect  5111  cnvcnv2  5119  cnvcnvres  5129  dmtpop  5141  rnsnopg  5144  rnco2  5173  dmco  5174  co01  5180  unidmrn  5198  dfdm2  5200  funimaexg  5338  dfmpt3  5376  mptun  5385  funcocnv2  5525  fnasrn  5736  fnasrng  5738  fpr  5740  fmptap  5748  riotav  5879  dmoprab  5999  rnoprab2  6002  mpov  6008  mpomptx  6009  abrexex2g  6172  abrexex2  6176  1stval2  6208  2ndval2  6209  fo1st  6210  fo2nd  6211  xp2  6226  dfoprab4f  6246  fmpoco  6269  tposmpo  6334  recsfval  6368  frecfnom  6454  freccllem  6455  frecfcllem  6457  frecsuclem  6459  df2o3  6483  o1p1e2  6521  ecqs  6651  qliftf  6674  erovlem  6681  mapsnf1o3  6751  ixp0x  6780  xpf1o  6900  djuunr  7125  dmaddpq  7439  dmmulpq  7440  enq0enq  7491  nqprlu  7607  m1p1sr  7820  m1m1sr  7821  caucvgsr  7862  dfcnqs  7901  3m1e2  9102  2p2e4  9109  3p2e5  9123  3p3e6  9124  4p2e6  9125  4p3e7  9126  4p4e8  9127  5p2e7  9128  5p3e8  9129  5p4e9  9130  6p2e8  9131  6p3e9  9132  7p2e9  9133  nn0supp  9292  nnzrab  9341  nn0zrab  9342  dec0u  9468  dec0h  9469  decsuc  9478  decsucc  9488  numma  9491  decma  9498  decmac  9499  decma2c  9500  decadd  9501  decaddc  9502  decmul1  9511  decmul1c  9512  decmul2c  9513  5p5e10  9518  6p4e10  9519  7p3e10  9522  8p2e10  9527  5t5e25  9550  6t6e36  9555  8t6e48  9566  nn0uz  9627  nnuz  9628  xaddcom  9927  ioomax  10014  iccmax  10015  ioopos  10016  ioorp  10017  fseq1p1m1  10160  fzo0to2pr  10285  fzo0to3tp  10286  frecfzennn  10497  irec  10710  sq10e99m1  10784  facnn  10798  fac0  10799  faclbnd2  10813  zfz1isolemsplit  10909  minmax  11373  xrminmax  11408  fisumrev2  11589  fsumparts  11613  fsumiun  11620  isumnn0nn  11636  fprod2d  11766  fprodle  11783  ege2le3  11814  cos1bnd  11902  efieq1re  11915  eirraplem  11920  phiprmpw  12360  4sqlem11  12539  4sqlem19  12547  unennn  12554  ennnfonelemjn  12559  qnnen  12588  strle1g  12724  quslem  12907  rmodislmod  13847  tgrest  14337  uniretop  14693  dvexp  14860  dvef  14873  elply2  14881  cospi  14935  sincos6thpi  14977  lgsdir2lem2  15145  2lgsoddprmlem3c  15197  bj-omind  15426