Theorem eqtr4i 2178

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

Syntax hints:   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1487  ax-17 1503  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-cleq 2147

This theorem is referenced by:  3eqtr2i  2181  3eqtr2ri  2182  3eqtr4i  2185  3eqtr4ri  2186  rabab  2730  cbvralcsf  3089  cbvrexcsf  3090  cbvrabcsf  3092  dfin5  3105  dfdif2  3106  uneqin  3354  unrab  3374  inrab  3375  inrab2  3376  difrab  3377  dfrab3ss  3381  rabun2  3382  difidALT  3459  difdifdirss  3474  dfif3  3514  tpidm  3657  dfint2  3805  iunrab  3892  uniiun  3898  intiin  3899  0iin  3903  mptv  4057  xpundi  4635  xpundir  4636  resiun2  4879  resopab  4903  opabresid  4912  dfse2  4952  cnvun  4984  cnvin  4986  imaundir  4992  imainrect  5024  cnvcnv2  5032  cnvcnvres  5042  dmtpop  5054  rnsnopg  5057  rnco2  5086  dmco  5087  co01  5093  unidmrn  5111  dfdm2  5113  funimaexg  5247  dfmpt3  5285  mptun  5294  funcocnv2  5432  fnasrn  5638  fnasrng  5640  fpr  5642  fmptap  5650  riotav  5775  dmoprab  5892  rnoprab2  5895  mpov  5901  mpomptx  5902  abrexex2g  6058  abrexex2  6062  1stval2  6093  2ndval2  6094  fo1st  6095  fo2nd  6096  xp2  6111  dfoprab4f  6131  fmpoco  6153  tposmpo  6218  recsfval  6252  frecfnom  6338  freccllem  6339  frecfcllem  6341  frecsuclem  6343  df2o3  6367  o1p1e2  6404  ecqs  6531  qliftf  6554  erovlem  6561  mapsnf1o3  6631  ixp0x  6660  xpf1o  6778  djuunr  6996  dmaddpq  7278  dmmulpq  7279  enq0enq  7330  nqprlu  7446  m1p1sr  7659  m1m1sr  7660  caucvgsr  7701  dfcnqs  7740  3m1e2  8932  2p2e4  8939  3p2e5  8953  3p3e6  8954  4p2e6  8955  4p3e7  8956  4p4e8  8957  5p2e7  8958  5p3e8  8959  5p4e9  8960  6p2e8  8961  6p3e9  8962  7p2e9  8963  nn0supp  9121  nnzrab  9170  nn0zrab  9171  dec0u  9294  dec0h  9295  decsuc  9304  decsucc  9314  numma  9317  decma  9324  decmac  9325  decma2c  9326  decadd  9327  decaddc  9328  decmul1  9337  decmul1c  9338  decmul2c  9339  5p5e10  9344  6p4e10  9345  7p3e10  9348  8p2e10  9353  5t5e25  9376  6t6e36  9381  8t6e48  9392  nn0uz  9452  nnuz  9453  xaddcom  9743  ioomax  9830  iccmax  9831  ioopos  9832  ioorp  9833  fseq1p1m1  9974  fzo0to2pr  10095  fzo0to3tp  10096  frecfzennn  10303  irec  10496  sq10e99m1  10564  facnn  10578  fac0  10579  faclbnd2  10593  zfz1isolemsplit  10686  minmax  11106  xrminmax  11139  fisumrev2  11320  fsumparts  11344  fsumiun  11351  isumnn0nn  11367  fprod2d  11497  fprodle  11514  ege2le3  11545  cos1bnd  11633  efieq1re  11645  eirraplem  11650  phiprmpw  12065  unennn  12077  ennnfonelemjn  12082  qnnen  12111  strle1g  12219  tgrest  12508  uniretop  12864  dvexp  13014  dvef  13027  cospi  13060  sincos6thpi  13102  bj-omind  13447