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  4141  xpundi  4731  xpundir  4732  resiun2  4979  resopab  5003  mptresid  5013  dfse2  5055  cnvun  5088  cnvin  5090  imaundir  5096  imainrect  5128  cnvcnv2  5136  cnvcnvres  5146  dmtpop  5158  rnsnopg  5161  rnco2  5190  dmco  5191  co01  5197  unidmrn  5215  dfdm2  5217  funimaexg  5358  dfmpt3  5398  mptun  5407  funcocnv2  5547  fnasrn  5758  fnasrng  5760  fpr  5766  fmptap  5774  riotav  5905  dmoprab  6026  rnoprab2  6029  mpov  6035  mpomptx  6036  abrexex2g  6205  abrexex2  6209  1stval2  6241  2ndval2  6242  fo1st  6243  fo2nd  6244  xp2  6259  dfoprab4f  6279  fmpoco  6302  tposmpo  6367  recsfval  6401  frecfnom  6487  freccllem  6488  frecfcllem  6490  frecsuclem  6492  df2o3  6516  o1p1e2  6554  ecqs  6684  qliftf  6707  erovlem  6714  mapsnf1o3  6784  ixp0x  6813  xpf1o  6941  djuunr  7168  dmaddpq  7492  dmmulpq  7493  enq0enq  7544  nqprlu  7660  m1p1sr  7873  m1m1sr  7874  caucvgsr  7915  dfcnqs  7954  3m1e2  9156  2p2e4  9163  3p2e5  9178  3p3e6  9179  4p2e6  9180  4p3e7  9181  4p4e8  9182  5p2e7  9183  5p3e8  9184  5p4e9  9185  6p2e8  9186  6p3e9  9187  7p2e9  9188  nn0supp  9347  nnzrab  9396  nn0zrab  9397  dec0u  9524  dec0h  9525  decsuc  9534  decsucc  9544  numma  9547  decma  9554  decmac  9555  decma2c  9556  decadd  9557  decaddc  9558  decmul1  9567  decmul1c  9568  decmul2c  9569  5p5e10  9574  6p4e10  9575  7p3e10  9578  8p2e10  9583  5t5e25  9606  6t6e36  9611  8t6e48  9622  nn0uz  9683  nnuz  9684  xaddcom  9983  ioomax  10070  iccmax  10071  ioopos  10072  ioorp  10073  fseq1p1m1  10216  fzo0to2pr  10347  fzo0to3tp  10348  frecfzennn  10571  irec  10784  sq10e99m1  10858  facnn  10872  fac0  10873  faclbnd2  10887  zfz1isolemsplit  10983  minmax  11541  xrminmax  11576  fisumrev2  11757  fsumparts  11781  fsumiun  11788  isumnn0nn  11804  fprod2d  11934  fprodle  11951  ege2le3  11982  cos1bnd  12070  efieq1re  12083  eirraplem  12088  3dvds  12175  m1bits  12271  phiprmpw  12544  4sqlem11  12724  4sqlem19  12732  dec5dvds  12735  decsplit1  12751  unennn  12768  ennnfonelemjn  12773  qnnen  12802  strle1g  12938  quslem  13156  rmodislmod  14113  tgrest  14641  uniretop  14997  cnfldtopn  15011  dvexp  15183  dvef  15199  elply2  15207  cospi  15272  sincos6thpi  15314  lgsdir2lem2  15506  lgsquadlem2  15555  lgsquad2lem2  15559  2lgsoddprmlem3c  15586  bj-omind  15874