Theorem eqtr4i 2063

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

Syntax hints:   = wceq 1243

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033

This theorem is referenced by:  3eqtr2i  2066  3eqtr2ri  2067  3eqtr4i  2070  3eqtr4ri  2071  rabab  2575  cbvralcsf  2908  cbvrexcsf  2909  cbvrabcsf  2911  dfin5  2925  dfdif2  2926  uneqin  3188  unrab  3208  inrab  3209  inrab2  3210  difrab  3211  dfrab3ss  3215  rabun2  3216  difidALT  3293  difdifdirss  3307  dfif3  3343  tpidm  3472  dfint2  3617  iunrab  3704  uniiun  3710  intiin  3711  0iin  3715  mptv  3853  xpundi  4396  xpundir  4397  resiun2  4631  resopab  4652  opabresid  4659  dfse2  4698  cnvun  4729  cnvin  4731  imaundir  4737  imainrect  4766  cnvcnv2  4774  cnvcnvres  4784  dmtpop  4796  rnsnopg  4799  rnco2  4828  dmco  4829  co01  4835  unidmrn  4850  dfdm2  4852  funimaexg  4983  dfmpt3  5021  mptun  5029  funcocnv2  5151  fnasrn  5341  fnasrng  5343  fpr  5345  fmptap  5353  riotav  5473  dmoprab  5585  rnoprab2  5588  mpt2v  5594  mpt2mptx  5595  abrexex2g  5747  abrexex2  5751  1stval2  5782  2ndval2  5783  fo1st  5784  fo2nd  5785  xp2  5799  dfoprab4f  5819  fmpt2co  5837  tposmpt2  5896  recsfval  5931  frecfnom  5986  frecsuclem1  5987  frecsuclem2  5989  df2o3  6014  o1p1e2  6048  ecqs  6168  qliftf  6191  erovlem  6198  dmaddpq  6477  dmmulpq  6478  enq0enq  6529  nqprlu  6645  m1p1sr  6845  m1m1sr  6846  caucvgsr  6886  dfcnqs  6917  3m1e2  8036  2p2e4  8037  3p2e5  8052  3p3e6  8053  4p2e6  8054  4p3e7  8055  4p4e8  8056  5p2e7  8057  5p3e8  8058  5p4e9  8059  5p5e10  8060  6p2e8  8061  6p3e9  8062  6p4e10  8063  7p2e9  8064  7p3e10  8065  8p2e10  8066  nn0supp  8234  nnzrab  8269  nn0zrab  8270  dec0u  8382  dec0h  8383  decsuc  8390  decsucc  8394  numma  8398  decma  8405  decmac  8406  decma2c  8407  decadd  8408  decaddc  8409  decmul1c  8414  decmul2c  8415  5t5e25  8443  6t6e36  8448  8t6e48  8459  nn0uz  8507  nnuz  8508  ioomax  8817  iccmax  8818  ioopos  8819  ioorp  8820  fseq1p1m1  8956  fzo0to2pr  9074  fzo0to3tp  9075  frecfzennn  9203  irec  9352  bj-omind  10058