Theorem 3eqtr4i 2269

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 2262	. 2 ⊢ 𝐷 = 𝐴
5	1, 4	eqtr4i 2262	1 ⊢ 𝐶 = 𝐷

This proof depends on syntax axioms:   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  rabswap  2731  rabbiia  2807  cbvrab  2819  cbvcsbw  3151  cbvcsb  3152  csbco  3157  csbcow  3158  cbvrabcsf  3213  un4  3389  in13  3444  in31  3445  in4  3447  indifcom  3477  indir  3480  undir  3481  notrab  3510  dfnul3  3524  rab0  3551  rabsnifsb  3777  prcom  3787  tprot  3804  tpcoma  3805  tpcomb  3806  tpass  3807  qdassr  3809  pw0  3862  opid  3922  int0  3984  cbviun  4049  cbviin  4050  iunrab  4060  iunin1  4077  cbvopab  4202  cbvopab1  4204  cbvopab2  4205  cbvopab1s  4206  cbvopab2v  4208  unopab  4210  cbvmptf  4225  cbvmpt  4226  iunopab  4424  uniuni  4597  2ordpr  4671  rabxp  4812  fconstmpt  4822  inxp  4914  cnvco  4965  rnmpt  5030  resundi  5076  resundir  5077  resindi  5078  resindir  5079  rescom  5088  resima  5096  imadmrn  5136  cnvimarndm  5151  cnvi  5192  rnun  5196  imaundi  5200  cnvxp  5206  imainrect  5233  imacnvcnv  5252  resdmres  5279  imadmres  5280  mptpreima  5281  cbviota  5342  cbviotavw  5343  sb8iota  5345  resdif  5661  cbvriotavw  6049  cbvriota  6050  dfoprab2  6135  cbvoprab1  6160  cbvoprab2  6161  cbvoprab12  6162  cbvoprab3  6164  cbvmpox  6166  resoprab  6184  caov32  6277  caov31  6279  ofmres  6369  dfopab2  6423  dfxp3  6430  dmmpossx  6435  fmpox  6436  tposco  6546  mapsncnv  6977  cbvixp  6997  xpcomco  7124  sbthlemi6  7279  xp2dju  7572  djuassen  7574  dmaddpi  7693  dmmulpi  7694  dfplpq2  7722  dfmpq2  7723  dmaddpq  7747  dmmulpq  7748  axi2m1  8243  negiso  9288  nummac  9831  decsubi  9849  9t11e99  9916  fzprval  10500  fztpval  10501  sqdivapi  11075  binom2i  11100  4bc2eq6  11229  shftidt2  11613  cji  11684  xrnegiso  12047  cbvsum  12145  fsumrelem  12257  cbvprod  12344  nn0gcdsq  12999  dec5nprm  13216  dec2nprm  13217  gcdi  13223  decsplit  13232  1259lem1  13265  1259lem4  13268  ballotfilemrinv  13329  dfrhm2  14513  rmodislmod  14740  cnfldsub  14964  dvdsrzring  14990  restco  15328  cnmptid  15435  plyid  15900  sincos3rdpi  15998  log2ublem2  16145  log2ublem3  16146  lgsdir2lem5  16279  lgsquadlem3  16326  2lgslem1b  16336  2lgsoddprmlem3d  16357  vtxval0  16422  iedgval0  16423