Theorem eqtr4i 2123

Description: An equality transitivity inference. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtr4i.1	⊢ 𝐴 = 𝐵
eqtr4i.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eqtr4i	⊢ 𝐴 = 𝐶

Proof of Theorem eqtr4i

Step	Hyp	Ref	Expression
1		eqtr4i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqtr4i.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2104	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eqtri 2120	1 ⊢ 𝐴 = 𝐶

Syntax hints:   = wceq 1299

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 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

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

This theorem is referenced by:  3eqtr2i  2126  3eqtr2ri  2127  3eqtr4i  2130  3eqtr4ri  2131  rabab  2662  cbvralcsf  3012  cbvrexcsf  3013  cbvrabcsf  3015  dfin5  3028  dfdif2  3029  uneqin  3274  unrab  3294  inrab  3295  inrab2  3296  difrab  3297  dfrab3ss  3301  rabun2  3302  difidALT  3379  difdifdirss  3394  dfif3  3434  tpidm  3572  dfint2  3720  iunrab  3807  uniiun  3813  intiin  3814  0iin  3818  mptv  3965  xpundi  4533  xpundir  4534  resiun2  4775  resopab  4799  opabresid  4808  dfse2  4848  cnvun  4880  cnvin  4882  imaundir  4888  imainrect  4920  cnvcnv2  4928  cnvcnvres  4938  dmtpop  4950  rnsnopg  4953  rnco2  4982  dmco  4983  co01  4989  unidmrn  5007  dfdm2  5009  funimaexg  5143  dfmpt3  5181  mptun  5190  funcocnv2  5326  fnasrn  5530  fnasrng  5532  fpr  5534  fmptap  5542  riotav  5667  dmoprab  5784  rnoprab2  5787  mpov  5793  mpomptx  5794  abrexex2g  5949  abrexex2  5953  1stval2  5984  2ndval2  5985  fo1st  5986  fo2nd  5987  xp2  6001  dfoprab4f  6021  fmpoco  6043  tposmpo  6108  recsfval  6142  frecfnom  6228  freccllem  6229  frecfcllem  6231  frecsuclem  6233  df2o3  6257  o1p1e2  6294  ecqs  6421  qliftf  6444  erovlem  6451  mapsnf1o3  6521  ixp0x  6550  xpf1o  6667  djuunr  6866  dmaddpq  7088  dmmulpq  7089  enq0enq  7140  nqprlu  7256  m1p1sr  7456  m1m1sr  7457  caucvgsr  7497  dfcnqs  7528  3m1e2  8698  2p2e4  8699  3p2e5  8713  3p3e6  8714  4p2e6  8715  4p3e7  8716  4p4e8  8717  5p2e7  8718  5p3e8  8719  5p4e9  8720  6p2e8  8721  6p3e9  8722  7p2e9  8723  nn0supp  8881  nnzrab  8930  nn0zrab  8931  dec0u  9054  dec0h  9055  decsuc  9064  decsucc  9074  numma  9077  decma  9084  decmac  9085  decma2c  9086  decadd  9087  decaddc  9088  decmul1  9097  decmul1c  9098  decmul2c  9099  5p5e10  9104  6p4e10  9105  7p3e10  9108  8p2e10  9113  5t5e25  9136  6t6e36  9141  8t6e48  9152  nn0uz  9210  nnuz  9211  xaddcom  9485  ioomax  9572  iccmax  9573  ioopos  9574  ioorp  9575  fseq1p1m1  9715  fzo0to2pr  9836  fzo0to3tp  9837  frecfzennn  10040  irec  10233  sq10e99m1  10301  facnn  10314  fac0  10315  faclbnd2  10329  zfz1isolemsplit  10422  minmax  10840  xrminmax  10873  fisumrev2  11054  fsumparts  11078  fsumiun  11085  isumnn0nn  11101  ege2le3  11175  cos1bnd  11264  efieq1re  11275  eirraplem  11278  phiprmpw  11690  unennn  11702  ennnfonelemjn  11707  qnnen  11736  strle1g  11831  tgrest  12120  uniretop  12447  bj-omind  12717