Theorem 3eqtr4ri 2770

Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr4ri	⊢ 𝐷 = 𝐶

Proof of Theorem 3eqtr4ri

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

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728

This theorem is referenced by:  cbvreucsf  3923  dfin3  4257  dfsymdif3  4286  rabdif  4301  dfif6  4508  dfsn2ALT  4628  qdass  4734  tpidm12  4736  iinvdif  5061  unidif0  5335  csbcnv  5868  dfdm4  5880  dmun  5895  resres  5984  inres  5989  resdifcom  5990  resiun1  5991  imainrect  6175  cnvcnv  6186  coundi  6241  coundir  6242  funopg  6575  csbov  7455  elrnmpores  7550  offres  7987  1st2val  8021  2nd2val  8022  mpomptsx  8068  oeoalem  8613  omopthlem1  8676  snec  8799  tcsni  9762  infmap2  10236  ackbij2lem3  10259  itunisuc  10438  axmulass  11176  divmul13i  12007  dfnn3  12259  numsucc  12753  decbin2  12854  uzrdgxfr  13990  hashxplem  14456  prprrab  14496  ids1  14620  s3s4  14957  s2s5  14958  s5s2  14959  fsumadd  15761  fsum2d  15792  fprodmul  15981  bpoly3  16079  bezout  16567  oppchomf  17737  dfinito3  18023  dftermo3  18024  smndex1iidm  18884  symgbas  19358  oppr1  20315  opsrtoslem1  22018  m2detleiblem2  22571  txswaphmeolem  23747  cnfldnm  24722  cnrbas  25098  cnnm  25117  volres  25486  voliunlem1  25508  uniioombllem4  25544  itg11  25649  dfrelog  26531  log2ublem3  26915  bposlem8  27259  noinfbnd2  27700  addsasslem1  27967  uhgrspan1  29287  ip2i  30814  bcseqi  31106  hilnormi  31149  cmcmlem  31577  fh3i  31609  fh4i  31610  pjadjii  31660  resf1o  32712  dp3mul10  32877  dpmul4  32893  threehalves  32894  ressplusf  32944  cycpmconjs  33172  resvsca  33353  cos9thpiminplylem5  33825  xpinpreima  33942  cnre2csqima  33947  esum2dlem  34128  eulerpartgbij  34409  ballotth  34575  plymulx  34585  hgt750lem2  34689  elrn3  35784  itg2addnclem2  37701  dfcoss3  38437  cossid  38503  dfssr2  38522  areaquad  43207  cnvrcl0  43616  stoweidlem13  46009  wallispi2  46069  fourierdlem96  46198  fourierdlem97  46199  fourierdlem98  46200  fourierdlem99  46201  fourierdlem113  46215  fourierswlem  46226  dfafv2  47128  dfnelbr2  47269  ceil5half3  47336  fmtnorec2  47524  fmtno5fac  47563  tposrescnv  48821  tposres3  48823  dfswapf2  49145  setrec2  49526