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  7571  djuassen  7573  dmaddpi  7692  dmmulpi  7693  dfplpq2  7721  dfmpq2  7722  dmaddpq  7746  dmmulpq  7747  axi2m1  8242  negiso  9287  nummac  9830  decsubi  9848  9t11e99  9915  fzprval  10499  fztpval  10500  sqdivapi  11073  binom2i  11098  4bc2eq6  11227  shftidt2  11611  cji  11682  xrnegiso  12044  cbvsum  12142  fsumrelem  12254  cbvprod  12341  nn0gcdsq  12996  dec5nprm  13213  dec2nprm  13214  gcdi  13220  decsplit  13229  1259lem1  13262  1259lem4  13265  ballotfilemrinv  13326  dfrhm2  14510  rmodislmod  14737  cnfldsub  14961  dvdsrzring  14987  restco  15324  cnmptid  15431  plyid  15896  sincos3rdpi  15994  log2ublem2  16141  log2ublem3  16142  lgsdir2lem5  16249  lgsquadlem3  16296  2lgslem1b  16306  2lgsoddprmlem3d  16327  vtxval0  16392  iedgval0  16393