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 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

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

This theorem is referenced by:  csbnest1g  4380  disjdif2  4427  diftpsn3  4734  tppreqb  4737  xpid11  5801  cores2  6111  funcoeqres  6644  fvunsn  6940  caovmo  7384  dftpos2  7908  fvmpocurryd  7936  tfrlem16  8028  oev2  8147  domss2  8675  enp1ilem  8751  fipreima  8829  dfac5lem3  9550  fpwwe2lem13  10063  canthwelem  10071  canthp1lem2  10074  reclem3pr  10470  mulcmpblnrlem  10491  1idsr  10519  mulgt0sr  10526  mul02lem2  10816  ine0  11074  lo1eq  14924  rlimeq  14925  sumeq2ii  15049  fsumf1o  15079  sumss  15080  fsumss  15081  fsumadd  15095  fsumcom2  15128  fsum0diag2  15137  fsummulc2  15138  fsumrelem  15161  isumshft  15193  mertenslem1  15239  prodeq2ii  15266  fprodf1o  15299  prodss  15300  fprodss  15301  fprodmul  15313  fproddiv  15314  fprodcom2  15337  fprodmodd  15350  fprodefsum  15447  bitsinv1  15790  bitsinvp1  15797  4sqlem10  16282  setsnid  16538  topnpropd  16709  xpsff1o  16839  homfeqbas  16965  comfffval2  16970  comfeq  16975  oppchomfpropd  16995  isssc  17089  funcpropd  17169  hofpropd  17516  eqglact  18330  symgvalstruct  18524  lsmmod2  18801  vrgpinv  18894  frgpnabllem1  18992  frgpnabllem2  18993  gsum2dlem2  19090  dprddisj2  19160  ablfac1eulem  19193  ringpropd  19331  crngpropd  19332  mulgass3  19386  rngidpropd  19444  invrpropd  19447  isrhm2d  19479  subrgpropd  19569  rhmpropd  19570  lss0v  19787  lidlrsppropd  20002  ressmpladd  20237  ressmplmul  20238  ressmplvsca  20239  eqcoe1ply1eq  20464  resstopn  21793  lecldbas  21826  isref  22116  txhaus  22254  qustgplem  22728  tuslem  22875  imasdsf1olem  22982  metustsym  23164  reconnlem1  23433  voliunlem1  24150  ismbf3d  24254  i1fima  24278  i1fd  24281  itgfsum  24426  dvmptc  24554  dvmptfsum  24571  dvfsumle  24617  dvfsumlem2  24623  itgsubst  24645  atantayl2  25515  chtdif  25734  ppidif  25739  pythi  28626  hvsubeq0i  28839  hvaddcani  28841  cmcmlem  29367  pj11i  29487  hosubeq0i  29602  riesz3i  29838  pjclem1  29971  pjclem3  29973  st0  30025  chirredi  30170  mdsymi  30187  difeq  30279  unidifsnne  30295  1nei  30471  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  34319  bj-2uplth  34333  matunitlindflem1  34887  ptrest  34890  poimirlem3  34894  poimirlem4  34895  poimirlem8  34899  poimirlem15  34906  mblfinlem2  34929  voliunnfl  34935  cdlemg47  37871  ltrnco4  37874  sn-1ne2  39156  eldioph2  39357  binomcxplemdvbinom  40683  binomcxplemnotnn0  40686  compne  40771  rnfdmpr  43479