Theorem 3eqtr4i 2260

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222

This theorem is referenced by:  rabswap  2710  rabbiia  2784  cbvrab  2797  cbvcsbw  3128  cbvcsb  3129  csbco  3134  csbcow  3135  cbvrabcsf  3190  un4  3364  in13  3417  in31  3418  in4  3420  indifcom  3450  indir  3453  undir  3454  notrab  3481  dfnul3  3494  rab0  3520  prcom  3742  tprot  3759  tpcoma  3760  tpcomb  3761  tpass  3762  qdassr  3764  pw0  3814  opid  3874  int0  3936  cbviun  4001  cbviin  4002  iunrab  4012  iunin1  4029  cbvopab  4154  cbvopab1  4156  cbvopab2  4157  cbvopab1s  4158  cbvopab2v  4160  unopab  4162  cbvmptf  4177  cbvmpt  4178  iunopab  4369  uniuni  4541  2ordpr  4615  rabxp  4755  fconstmpt  4765  inxp  4855  cnvco  4906  rnmpt  4971  resundi  5017  resundir  5018  resindi  5019  resindir  5020  rescom  5029  resima  5037  imadmrn  5077  cnvimarndm  5091  cnvi  5132  rnun  5136  imaundi  5140  cnvxp  5146  imainrect  5173  imacnvcnv  5192  resdmres  5219  imadmres  5220  mptpreima  5221  cbviota  5282  cbviotavw  5283  sb8iota  5285  resdif  5593  cbvriotavw  5964  cbvriota  5965  dfoprab2  6050  cbvoprab1  6075  cbvoprab2  6076  cbvoprab12  6077  cbvoprab3  6079  cbvmpox  6081  resoprab  6099  caov32  6192  caov31  6194  ofmres  6279  dfopab2  6333  dfxp3  6338  dmmpossx  6343  fmpox  6344  tposco  6419  mapsncnv  6840  cbvixp  6860  xpcomco  6981  sbthlemi6  7125  xp2dju  7393  djuassen  7395  dmaddpi  7508  dmmulpi  7509  dfplpq2  7537  dfmpq2  7538  dmaddpq  7562  dmmulpq  7563  axi2m1  8058  negiso  9098  nummac  9618  decsubi  9636  9t11e99  9703  fzprval  10274  fztpval  10275  sqdivapi  10840  binom2i  10865  4bc2eq6  10991  shftidt2  11338  cji  11408  xrnegiso  11768  cbvsum  11866  fsumrelem  11977  cbvprod  12064  nn0gcdsq  12717  dec5nprm  12932  dec2nprm  12933  gcdi  12938  decsplit  12947  dfrhm2  14112  rmodislmod  14309  cnfldsub  14533  dvdsrzring  14561  restco  14842  cnmptid  14949  plyid  15414  sincos3rdpi  15511  lgsdir2lem5  15705  lgsquadlem3  15752  2lgslem1b  15762  2lgsoddprmlem3d  15783  vtxval0  15848  iedgval0  15849  if0ab  16127