Theorem eqtr4i 2189

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

Syntax hints:   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  3eqtr2i  2192  3eqtr2ri  2193  3eqtr4i  2196  3eqtr4ri  2197  rabab  2747  cbvralcsf  3107  cbvrexcsf  3108  cbvrabcsf  3110  dfin5  3123  dfdif2  3124  uneqin  3373  unrab  3393  inrab  3394  inrab2  3395  difrab  3396  dfrab3ss  3400  rabun2  3401  difidALT  3478  difdifdirss  3493  dfif3  3533  tpidm  3678  dfint2  3826  iunrab  3913  uniiun  3919  intiin  3920  0iin  3924  mptv  4079  xpundi  4660  xpundir  4661  resiun2  4904  resopab  4928  opabresid  4937  dfse2  4977  cnvun  5009  cnvin  5011  imaundir  5017  imainrect  5049  cnvcnv2  5057  cnvcnvres  5067  dmtpop  5079  rnsnopg  5082  rnco2  5111  dmco  5112  co01  5118  unidmrn  5136  dfdm2  5138  funimaexg  5272  dfmpt3  5310  mptun  5319  funcocnv2  5457  fnasrn  5663  fnasrng  5665  fpr  5667  fmptap  5675  riotav  5803  dmoprab  5923  rnoprab2  5926  mpov  5932  mpomptx  5933  abrexex2g  6088  abrexex2  6092  1stval2  6123  2ndval2  6124  fo1st  6125  fo2nd  6126  xp2  6141  dfoprab4f  6161  fmpoco  6184  tposmpo  6249  recsfval  6283  frecfnom  6369  freccllem  6370  frecfcllem  6372  frecsuclem  6374  df2o3  6398  o1p1e2  6436  ecqs  6563  qliftf  6586  erovlem  6593  mapsnf1o3  6663  ixp0x  6692  xpf1o  6810  djuunr  7031  dmaddpq  7320  dmmulpq  7321  enq0enq  7372  nqprlu  7488  m1p1sr  7701  m1m1sr  7702  caucvgsr  7743  dfcnqs  7782  3m1e2  8977  2p2e4  8984  3p2e5  8998  3p3e6  8999  4p2e6  9000  4p3e7  9001  4p4e8  9002  5p2e7  9003  5p3e8  9004  5p4e9  9005  6p2e8  9006  6p3e9  9007  7p2e9  9008  nn0supp  9166  nnzrab  9215  nn0zrab  9216  dec0u  9342  dec0h  9343  decsuc  9352  decsucc  9362  numma  9365  decma  9372  decmac  9373  decma2c  9374  decadd  9375  decaddc  9376  decmul1  9385  decmul1c  9386  decmul2c  9387  5p5e10  9392  6p4e10  9393  7p3e10  9396  8p2e10  9401  5t5e25  9424  6t6e36  9429  8t6e48  9440  nn0uz  9500  nnuz  9501  xaddcom  9797  ioomax  9884  iccmax  9885  ioopos  9886  ioorp  9887  fseq1p1m1  10029  fzo0to2pr  10153  fzo0to3tp  10154  frecfzennn  10361  irec  10554  sq10e99m1  10626  facnn  10640  fac0  10641  faclbnd2  10655  zfz1isolemsplit  10751  minmax  11171  xrminmax  11206  fisumrev2  11387  fsumparts  11411  fsumiun  11418  isumnn0nn  11434  fprod2d  11564  fprodle  11581  ege2le3  11612  cos1bnd  11700  efieq1re  11712  eirraplem  11717  phiprmpw  12154  unennn  12330  ennnfonelemjn  12335  qnnen  12364  strle1g  12485  tgrest  12809  uniretop  13165  dvexp  13315  dvef  13328  cospi  13361  sincos6thpi  13403  lgsdir2lem2  13570  bj-omind  13816