Theorem 3eqtr3g 2879

Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)

Hypotheses

Ref	Expression
3eqtr3g.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3g.2	⊢ 𝐴 = 𝐶
3eqtr3g.3	⊢ 𝐵 = 𝐷

Assertion

Ref	Expression
3eqtr3g	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr3g

Step	Hyp	Ref	Expression
1		3eqtr3g.2	. . 3 ⊢ 𝐴 = 𝐶
2		3eqtr3g.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	syl5eqr 2870	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	syl6eq 2872	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  csbnest1g  4381  disjdif2  4428  diftpsn3  4735  tppreqb  4738  xpid11  5802  cores2  6112  funcoeqres  6645  fvunsn  6941  caovmo  7385  dftpos2  7909  fvmpocurryd  7937  tfrlem16  8029  oev2  8148  domss2  8676  enp1ilem  8752  fipreima  8830  dfac5lem3  9551  fpwwe2lem13  10064  canthwelem  10072  canthp1lem2  10075  reclem3pr  10471  mulcmpblnrlem  10492  1idsr  10520  mulgt0sr  10527  mul02lem2  10817  ine0  11075  lo1eq  14925  rlimeq  14926  sumeq2ii  15050  fsumf1o  15080  sumss  15081  fsumss  15082  fsumadd  15096  fsumcom2  15129  fsum0diag2  15138  fsummulc2  15139  fsumrelem  15162  isumshft  15194  mertenslem1  15240  prodeq2ii  15267  fprodf1o  15300  prodss  15301  fprodss  15302  fprodmul  15314  fproddiv  15315  fprodcom2  15338  fprodmodd  15351  fprodefsum  15448  bitsinv1  15791  bitsinvp1  15798  4sqlem10  16283  setsnid  16539  topnpropd  16710  xpsff1o  16840  homfeqbas  16966  comfffval2  16971  comfeq  16976  oppchomfpropd  16996  isssc  17090  funcpropd  17170  hofpropd  17517  eqglact  18331  symgvalstruct  18525  lsmmod2  18802  vrgpinv  18895  frgpnabllem1  18993  frgpnabllem2  18994  gsum2dlem2  19091  dprddisj2  19161  ablfac1eulem  19194  ringpropd  19332  crngpropd  19333  mulgass3  19387  rngidpropd  19445  invrpropd  19448  isrhm2d  19480  subrgpropd  19570  rhmpropd  19571  lss0v  19788  lidlrsppropd  20003  ressmpladd  20238  ressmplmul  20239  ressmplvsca  20240  eqcoe1ply1eq  20465  resstopn  21794  lecldbas  21827  isref  22117  txhaus  22255  qustgplem  22729  tuslem  22876  imasdsf1olem  22983  metustsym  23165  reconnlem1  23434  voliunlem1  24151  ismbf3d  24255  i1fima  24279  i1fd  24282  itgfsum  24427  dvmptc  24555  dvmptfsum  24572  dvfsumle  24618  dvfsumlem2  24624  itgsubst  24646  atantayl2  25516  chtdif  25735  ppidif  25740  pythi  28627  hvsubeq0i  28840  hvaddcani  28842  cmcmlem  29368  pj11i  29488  hosubeq0i  29603  riesz3i  29839  pjclem1  29972  pjclem3  29974  st0  30026  chirredi  30171  mdsymi  30188  difeq  30280  unidifsnne  30296  1nei  30472  subrgchr  30865  locfinref  31105  esumpfinvallem  31333  esum2dlem  31351  carsgclctun  31579  ballotlemgun  31782  cvmliftmolem1  32528  cvmlift3lem6  32571  msubff1  32803  isfne  33687  isfne4  33688  isfne4b  33689  bj-1uplth  34322  bj-2uplth  34336  matunitlindflem1  34903  ptrest  34906  poimirlem3  34910  poimirlem4  34911  poimirlem8  34915  poimirlem15  34922  mblfinlem2  34945  voliunnfl  34951  cdlemg47  37887  ltrnco4  37890  sn-1ne2  39178  eldioph2  39379  binomcxplemdvbinom  40705  binomcxplemnotnn0  40708  compne  40793  rnfdmpr  43500