Theorem 3eqtr4i 2208

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

Syntax hints:   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  rabswap  2656  rabbiia  2724  cbvrab  2737  cbvcsbw  3063  cbvcsb  3064  csbco  3069  csbcow  3070  cbvrabcsf  3124  un4  3297  in13  3350  in31  3351  in4  3353  indifcom  3383  indir  3386  undir  3387  notrab  3414  dfnul3  3427  rab0  3453  prcom  3670  tprot  3687  tpcoma  3688  tpcomb  3689  tpass  3690  qdassr  3692  pw0  3741  opid  3798  int0  3860  cbviun  3925  cbviin  3926  iunrab  3936  iunin1  3953  cbvopab  4076  cbvopab1  4078  cbvopab2  4079  cbvopab1s  4080  cbvopab2v  4082  unopab  4084  cbvmptf  4099  cbvmpt  4100  iunopab  4283  uniuni  4453  2ordpr  4525  rabxp  4665  fconstmpt  4675  inxp  4763  cnvco  4814  rnmpt  4877  resundi  4922  resundir  4923  resindi  4924  resindir  4925  rescom  4934  resima  4942  imadmrn  4982  cnvimarndm  4994  cnvi  5035  rnun  5039  imaundi  5043  cnvxp  5049  imainrect  5076  imacnvcnv  5095  resdmres  5122  imadmres  5123  mptpreima  5124  cbviota  5185  sb8iota  5187  resdif  5485  cbvriota  5844  dfoprab2  5925  cbvoprab1  5950  cbvoprab2  5951  cbvoprab12  5952  cbvoprab3  5954  cbvmpox  5956  resoprab  5974  caov32  6065  caov31  6067  ofmres  6140  dfopab2  6193  dfxp3  6198  dmmpossx  6203  fmpox  6204  tposco  6279  mapsncnv  6698  cbvixp  6718  xpcomco  6829  sbthlemi6  6964  xp2dju  7217  djuassen  7219  dmaddpi  7327  dmmulpi  7328  dfplpq2  7356  dfmpq2  7357  dmaddpq  7381  dmmulpq  7382  axi2m1  7877  negiso  8915  nummac  9431  decsubi  9449  9t11e99  9516  fzprval  10085  fztpval  10086  sqdivapi  10607  binom2i  10632  4bc2eq6  10757  shftidt2  10844  cji  10914  xrnegiso  11273  cbvsum  11371  fsumrelem  11482  cbvprod  11569  nn0gcdsq  12203  rmodislmod  13447  cnfldsub  13609  dvdsrzring  13633  restco  13814  cnmptid  13921  sincos3rdpi  14404  lgsdir2lem5  14573  2lgsoddprmlem3d  14598  if0ab  14697