Theorem 3eqtr4i 2227

Description: An inference from three chained equalities. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr4i	⊢ 𝐶 = 𝐷

Proof of Theorem 3eqtr4i

Step	Hyp	Ref	Expression
1		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
2		3eqtr4i.3	. . 3 ⊢ 𝐷 = 𝐵
3		3eqtr4i.1	. . 3 ⊢ 𝐴 = 𝐵
4	2, 3	eqtr4i 2220	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2220	1 ⊢ 𝐶 = 𝐷

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:  rabswap  2676  rabbiia  2748  cbvrab  2761  cbvcsbw  3088  cbvcsb  3089  csbco  3094  csbcow  3095  cbvrabcsf  3150  un4  3324  in13  3377  in31  3378  in4  3380  indifcom  3410  indir  3413  undir  3414  notrab  3441  dfnul3  3454  rab0  3480  prcom  3699  tprot  3716  tpcoma  3717  tpcomb  3718  tpass  3719  qdassr  3721  pw0  3770  opid  3827  int0  3889  cbviun  3954  cbviin  3955  iunrab  3965  iunin1  3982  cbvopab  4105  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  cbvopab2v  4111  unopab  4113  cbvmptf  4128  cbvmpt  4129  iunopab  4317  uniuni  4487  2ordpr  4561  rabxp  4701  fconstmpt  4711  inxp  4801  cnvco  4852  rnmpt  4915  resundi  4960  resundir  4961  resindi  4962  resindir  4963  rescom  4972  resima  4980  imadmrn  5020  cnvimarndm  5034  cnvi  5075  rnun  5079  imaundi  5083  cnvxp  5089  imainrect  5116  imacnvcnv  5135  resdmres  5162  imadmres  5163  mptpreima  5164  cbviota  5225  sb8iota  5227  resdif  5529  cbvriota  5891  dfoprab2  5973  cbvoprab1  5998  cbvoprab2  5999  cbvoprab12  6000  cbvoprab3  6002  cbvmpox  6004  resoprab  6022  caov32  6115  caov31  6117  ofmres  6202  dfopab2  6256  dfxp3  6261  dmmpossx  6266  fmpox  6267  tposco  6342  mapsncnv  6763  cbvixp  6783  xpcomco  6894  sbthlemi6  7037  xp2dju  7300  djuassen  7302  dmaddpi  7411  dmmulpi  7412  dfplpq2  7440  dfmpq2  7441  dmaddpq  7465  dmmulpq  7466  axi2m1  7961  negiso  9001  nummac  9520  decsubi  9538  9t11e99  9605  fzprval  10176  fztpval  10177  sqdivapi  10734  binom2i  10759  4bc2eq6  10885  shftidt2  11016  cji  11086  xrnegiso  11446  cbvsum  11544  fsumrelem  11655  cbvprod  11742  nn0gcdsq  12395  dec5nprm  12610  dec2nprm  12611  gcdi  12616  decsplit  12625  dfrhm2  13788  rmodislmod  13985  cnfldsub  14209  dvdsrzring  14237  restco  14518  cnmptid  14625  plyid  15090  sincos3rdpi  15187  lgsdir2lem5  15381  lgsquadlem3  15428  2lgslem1b  15438  2lgsoddprmlem3d  15459  if0ab  15559