Theorem eqtr4i 2229

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  3eqtr2i  2232  3eqtr2ri  2233  3eqtr4i  2236  3eqtr4ri  2237  rabab  2793  cbvralcsf  3156  cbvrexcsf  3157  cbvrabcsf  3159  dfin5  3173  dfdif2  3174  uneqin  3424  unrab  3444  inrab  3445  inrab2  3446  difrab  3447  dfrab3ss  3451  rabun2  3452  difidALT  3530  difdifdirss  3545  dfif3  3584  tpidm  3735  dfint2  3887  iunrab  3975  uniiun  3981  intiin  3982  0iin  3986  mptv  4142  xpundi  4732  xpundir  4733  resiun2  4980  resopab  5004  mptresid  5014  dfse2  5056  cnvun  5089  cnvin  5091  imaundir  5097  imainrect  5129  cnvcnv2  5137  cnvcnvres  5147  dmtpop  5159  rnsnopg  5162  rnco2  5191  dmco  5192  co01  5198  unidmrn  5216  dfdm2  5218  funimaexg  5359  dfmpt3  5400  mptun  5409  funcocnv2  5549  fnasrn  5760  fnasrng  5762  fpr  5768  fmptap  5776  riotav  5907  dmoprab  6028  rnoprab2  6031  mpov  6037  mpomptx  6038  abrexex2g  6207  abrexex2  6211  1stval2  6243  2ndval2  6244  fo1st  6245  fo2nd  6246  xp2  6261  dfoprab4f  6281  fmpoco  6304  tposmpo  6369  recsfval  6403  frecfnom  6489  freccllem  6490  frecfcllem  6492  frecsuclem  6494  df2o3  6518  o1p1e2  6556  ecqs  6686  qliftf  6709  erovlem  6716  mapsnf1o3  6786  ixp0x  6815  xpf1o  6943  djuunr  7170  dmaddpq  7494  dmmulpq  7495  enq0enq  7546  nqprlu  7662  m1p1sr  7875  m1m1sr  7876  caucvgsr  7917  dfcnqs  7956  3m1e2  9158  2p2e4  9165  3p2e5  9180  3p3e6  9181  4p2e6  9182  4p3e7  9183  4p4e8  9184  5p2e7  9185  5p3e8  9186  5p4e9  9187  6p2e8  9188  6p3e9  9189  7p2e9  9190  nn0supp  9349  nnzrab  9398  nn0zrab  9399  dec0u  9526  dec0h  9527  decsuc  9536  decsucc  9546  numma  9549  decma  9556  decmac  9557  decma2c  9558  decadd  9559  decaddc  9560  decmul1  9569  decmul1c  9570  decmul2c  9571  5p5e10  9576  6p4e10  9577  7p3e10  9580  8p2e10  9585  5t5e25  9608  6t6e36  9613  8t6e48  9624  nn0uz  9685  nnuz  9686  xaddcom  9985  ioomax  10072  iccmax  10073  ioopos  10074  ioorp  10075  fseq1p1m1  10218  fzo0to2pr  10349  fzo0to3tp  10350  frecfzennn  10573  irec  10786  sq10e99m1  10860  facnn  10874  fac0  10875  faclbnd2  10889  zfz1isolemsplit  10985  minmax  11574  xrminmax  11609  fisumrev2  11790  fsumparts  11814  fsumiun  11821  isumnn0nn  11837  fprod2d  11967  fprodle  11984  ege2le3  12015  cos1bnd  12103  efieq1re  12116  eirraplem  12121  3dvds  12208  m1bits  12304  phiprmpw  12577  4sqlem11  12757  4sqlem19  12765  dec5dvds  12768  decsplit1  12784  unennn  12801  ennnfonelemjn  12806  qnnen  12835  strle1g  12971  quslem  13189  rmodislmod  14146  tgrest  14674  uniretop  15030  cnfldtopn  15044  dvexp  15216  dvef  15232  elply2  15240  cospi  15305  sincos6thpi  15347  lgsdir2lem2  15539  lgsquadlem2  15588  lgsquad2lem2  15592  2lgsoddprmlem3c  15619  bj-omind  15907