Theorem eqtr4i 2118

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

Syntax hints:   = wceq 1296

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077

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

This theorem is referenced by:  3eqtr2i  2121  3eqtr2ri  2122  3eqtr4i  2125  3eqtr4ri  2126  rabab  2654  cbvralcsf  3004  cbvrexcsf  3005  cbvrabcsf  3007  dfin5  3020  dfdif2  3021  uneqin  3266  unrab  3286  inrab  3287  inrab2  3288  difrab  3289  dfrab3ss  3293  rabun2  3294  difidALT  3371  difdifdirss  3386  dfif3  3426  tpidm  3564  dfint2  3712  iunrab  3799  uniiun  3805  intiin  3806  0iin  3810  mptv  3957  xpundi  4523  xpundir  4524  resiun2  4765  resopab  4789  opabresid  4798  dfse2  4838  cnvun  4870  cnvin  4872  imaundir  4878  imainrect  4910  cnvcnv2  4918  cnvcnvres  4928  dmtpop  4940  rnsnopg  4943  rnco2  4972  dmco  4973  co01  4979  unidmrn  4997  dfdm2  4999  funimaexg  5132  dfmpt3  5170  mptun  5178  funcocnv2  5313  fnasrn  5514  fnasrng  5516  fpr  5518  fmptap  5526  riotav  5651  dmoprab  5767  rnoprab2  5770  mpt2v  5776  mpt2mptx  5777  abrexex2g  5929  abrexex2  5933  1stval2  5964  2ndval2  5965  fo1st  5966  fo2nd  5967  xp2  5981  dfoprab4f  6001  fmpt2co  6019  tposmpt2  6084  recsfval  6118  frecfnom  6204  freccllem  6205  frecfcllem  6207  frecsuclem  6209  df2o3  6233  o1p1e2  6269  ecqs  6394  qliftf  6417  erovlem  6424  mapsnf1o3  6494  ixp0x  6523  xpf1o  6640  djuunr  6838  dmaddpq  7035  dmmulpq  7036  enq0enq  7087  nqprlu  7203  m1p1sr  7403  m1m1sr  7404  caucvgsr  7444  dfcnqs  7475  3m1e2  8640  2p2e4  8641  3p2e5  8655  3p3e6  8656  4p2e6  8657  4p3e7  8658  4p4e8  8659  5p2e7  8660  5p3e8  8661  5p4e9  8662  6p2e8  8663  6p3e9  8664  7p2e9  8665  nn0supp  8823  nnzrab  8872  nn0zrab  8873  dec0u  8996  dec0h  8997  decsuc  9006  decsucc  9016  numma  9019  decma  9026  decmac  9027  decma2c  9028  decadd  9029  decaddc  9030  decmul1  9039  decmul1c  9040  decmul2c  9041  5p5e10  9046  6p4e10  9047  7p3e10  9050  8p2e10  9055  5t5e25  9078  6t6e36  9083  8t6e48  9094  nn0uz  9152  nnuz  9153  xaddcom  9427  ioomax  9514  iccmax  9515  ioopos  9516  ioorp  9517  fseq1p1m1  9657  fzo0to2pr  9778  fzo0to3tp  9779  frecfzennn  9982  irec  10185  sq10e99m1  10253  facnn  10266  fac0  10267  faclbnd2  10281  zfz1isolemsplit  10374  minmax  10792  xrminmax  10824  fisumrev2  11005  fsumparts  11029  fsumiun  11036  isumnn0nn  11052  ege2le3  11126  cos1bnd  11215  efieq1re  11226  eirraplem  11229  phiprmpw  11641  unennn  11653  strle1g  11749  tgrest  12037  uniretop  12320  bj-omind  12553