Theorem eqtr4i 2220

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  3eqtr2i  2223  3eqtr2ri  2224  3eqtr4i  2227  3eqtr4ri  2228  rabab  2784  cbvralcsf  3147  cbvrexcsf  3148  cbvrabcsf  3150  dfin5  3164  dfdif2  3165  uneqin  3414  unrab  3434  inrab  3435  inrab2  3436  difrab  3437  dfrab3ss  3441  rabun2  3442  difidALT  3520  difdifdirss  3535  dfif3  3574  tpidm  3724  dfint2  3876  iunrab  3964  uniiun  3970  intiin  3971  0iin  3975  mptv  4130  xpundi  4719  xpundir  4720  resiun2  4966  resopab  4990  mptresid  5000  dfse2  5042  cnvun  5075  cnvin  5077  imaundir  5083  imainrect  5115  cnvcnv2  5123  cnvcnvres  5133  dmtpop  5145  rnsnopg  5148  rnco2  5177  dmco  5178  co01  5184  unidmrn  5202  dfdm2  5204  funimaexg  5342  dfmpt3  5380  mptun  5389  funcocnv2  5529  fnasrn  5740  fnasrng  5742  fpr  5744  fmptap  5752  riotav  5883  dmoprab  6003  rnoprab2  6006  mpov  6012  mpomptx  6013  abrexex2g  6177  abrexex2  6181  1stval2  6213  2ndval2  6214  fo1st  6215  fo2nd  6216  xp2  6231  dfoprab4f  6251  fmpoco  6274  tposmpo  6339  recsfval  6373  frecfnom  6459  freccllem  6460  frecfcllem  6462  frecsuclem  6464  df2o3  6488  o1p1e2  6526  ecqs  6656  qliftf  6679  erovlem  6686  mapsnf1o3  6756  ixp0x  6785  xpf1o  6905  djuunr  7132  dmaddpq  7446  dmmulpq  7447  enq0enq  7498  nqprlu  7614  m1p1sr  7827  m1m1sr  7828  caucvgsr  7869  dfcnqs  7908  3m1e2  9110  2p2e4  9117  3p2e5  9132  3p3e6  9133  4p2e6  9134  4p3e7  9135  4p4e8  9136  5p2e7  9137  5p3e8  9138  5p4e9  9139  6p2e8  9140  6p3e9  9141  7p2e9  9142  nn0supp  9301  nnzrab  9350  nn0zrab  9351  dec0u  9477  dec0h  9478  decsuc  9487  decsucc  9497  numma  9500  decma  9507  decmac  9508  decma2c  9509  decadd  9510  decaddc  9511  decmul1  9520  decmul1c  9521  decmul2c  9522  5p5e10  9527  6p4e10  9528  7p3e10  9531  8p2e10  9536  5t5e25  9559  6t6e36  9564  8t6e48  9575  nn0uz  9636  nnuz  9637  xaddcom  9936  ioomax  10023  iccmax  10024  ioopos  10025  ioorp  10026  fseq1p1m1  10169  fzo0to2pr  10294  fzo0to3tp  10295  frecfzennn  10518  irec  10731  sq10e99m1  10805  facnn  10819  fac0  10820  faclbnd2  10834  zfz1isolemsplit  10930  minmax  11395  xrminmax  11430  fisumrev2  11611  fsumparts  11635  fsumiun  11642  isumnn0nn  11658  fprod2d  11788  fprodle  11805  ege2le3  11836  cos1bnd  11924  efieq1re  11937  eirraplem  11942  3dvds  12029  phiprmpw  12390  4sqlem11  12570  4sqlem19  12578  dec5dvds  12581  decsplit1  12597  unennn  12614  ennnfonelemjn  12619  qnnen  12648  strle1g  12784  quslem  12967  rmodislmod  13907  tgrest  14405  uniretop  14761  cnfldtopn  14775  dvexp  14947  dvef  14963  elply2  14971  cospi  15036  sincos6thpi  15078  lgsdir2lem2  15270  lgsquadlem2  15319  lgsquad2lem2  15323  2lgsoddprmlem3c  15350  bj-omind  15580