Theorem eqtr4i 2258

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

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  3203  cbvrexcsf  3204  cbvrabcsf  3206  dfin5  3220  dfdif2  3221  uneqin  3474  unrab  3494  inrab  3495  inrab2  3496  difrab  3497  dfrab3ss  3501  rabun2  3502  difidALT  3580  difdifdirss  3596  dfif3  3638  tpidm  3795  dfint2  3953  iunrab  4041  uniiun  4047  intiin  4048  0iin  4052  mptv  4209  xpundi  4808  xpundir  4809  resiun2  5060  resopab  5084  mptresid  5094  dfse2  5137  cnvun  5170  cnvin  5172  imaundir  5178  imainrect  5210  cnvcnv2  5218  cnvcnvres  5228  dmtpop  5240  rnsnopg  5243  rnco2  5272  dmco  5273  co01  5279  unidmrn  5297  dfdm2  5299  funimaexg  5442  dfmpt3  5483  mptun  5492  funcocnv2  5641  fnasrn  5858  fnasrng  5860  fpr  5868  fmptap  5876  riotav  6011  dmoprab  6136  rnoprab2  6139  mpov  6145  mpomptx  6146  abrexex2g  6315  abrexex2  6319  1stval2  6351  2ndval2  6352  fo1st  6353  fo2nd  6354  xp2  6369  dfoprab4f  6389  fmpoco  6414  tposmpo  6514  recsfval  6548  frecfnom  6634  freccllem  6635  frecfcllem  6637  frecsuclem  6639  df2o3  6664  o1p1e2  6703  ecqs  6833  qliftf  6856  erovlem  6863  mapsnf1o3  6934  ixp0x  6963  xpf1o  7099  djuunr  7359  dmaddpq  7696  dmmulpq  7697  enq0enq  7748  nqprlu  7864  m1p1sr  8077  m1m1sr  8078  caucvgsr  8119  dfcnqs  8158  3m1e2  9359  2p2e4  9366  3p2e5  9381  3p3e6  9382  4p2e6  9383  4p3e7  9384  4p4e8  9385  5p2e7  9386  5p3e8  9387  5p4e9  9388  6p2e8  9389  6p3e9  9390  7p2e9  9391  nn0supp  9554  nnzrab  9603  nn0zrab  9604  dec0u  9732  dec0h  9733  decsuc  9742  decsucc  9752  numma  9755  decma  9762  decmac  9763  decma2c  9764  decadd  9765  decaddc  9766  decmul1  9775  decmul1c  9776  decmul2c  9777  5p5e10  9782  6p4e10  9783  7p3e10  9786  8p2e10  9791  5t5e25  9814  6t6e36  9819  8t6e48  9830  nn0uz  9892  nnuz  9893  xaddcom  10197  ioomax  10284  iccmax  10285  ioopos  10286  ioorp  10287  fseq1p1m1  10432  fzo0to2pr  10567  fzo0to3tp  10568  frecfzennn  10792  irec  11005  sq10e99m1  11079  facnn  11093  fac0  11094  faclbnd2  11108  zfz1isolemsplit  11214  minmax  11919  xrminmax  11954  fisumrev2  12136  fsumparts  12160  fsumiun  12167  isumnn0nn  12183  fprod2d  12313  fprodle  12330  ege2le3  12361  cos1bnd  12449  efieq1re  12462  eirraplem  12467  3dvds  12554  m1bits  12650  phiprmpw  12923  4sqlem11  13103  4sqlem19  13111  dec5dvds  13114  decsplit1  13130  ballotfilemfval  13150  unennn  13165  ennnfonelemjn  13170  qnnen  13199  strle1g  13336  quslem  13554  rmodislmod  14516  tgrest  15051  uniretop  15407  cnfldtopn  15421  dvexp  15593  dvef  15609  elply2  15617  cospi  15682  sincos6thpi  15724  lgsdir2lem2  15919  lgsquadlem2  15968  lgsquad2lem2  15972  2lgsoddprmlem3c  15999  konigsbergumgr  16499  konigsberglem1  16500  konigsberglem2  16501  bj-omind  16721  gfsump1  16885