Theorem 3eqtr3g 2794

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	eqtr3id 2785	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtrdi 2787	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  csbnest1g  4394  disjdif2  4444  diftpsn3  4767  tppreqb  4770  xpid11  5892  cores2  6216  funcoeqres  6820  fvunsn  7130  caovmo  7596  dftpos2  8179  fvmpocurryd  8207  tfrlem16  8344  oev2  8474  domss2  9087  enp1ilem  9229  fipreima  9309  dfac5lem3  10070  fpwwe2lem12  10587  canthwelem  10595  canthp1lem2  10598  reclem3pr  10994  mulcmpblnrlem  11015  1idsr  11043  mulgt0sr  11050  mul02lem2  11341  ine0  11599  lo1eq  15462  rlimeq  15463  sumeq2ii  15589  fsumf1o  15619  sumss  15620  fsumss  15621  fsumadd  15636  fsumcom2  15670  fsum0diag2  15679  fsummulc2  15680  fsumrelem  15703  isumshft  15735  mertenslem1  15780  prodeq2ii  15807  fprodf1o  15840  prodss  15841  fprodss  15842  fprodmul  15854  fproddiv  15855  fprodcom2  15878  fprodmodd  15891  fprodefsum  15988  bitsinv1  16333  bitsinvp1  16340  4sqlem10  16830  setsnid  17092  setsnidOLD  17093  topnpropd  17332  xpsff1o  17463  homfeqbas  17590  comfffval2  17595  comfeq  17600  oppchomfpropd  17622  isssc  17717  funcpropd  17801  hofpropd  18170  eqglact  18995  symgvalstruct  19192  symgvalstructOLD  19193  lsmmod2  19472  vrgpinv  19565  frgpnabllem1  19665  frgpnabllem2  19666  gsum2dlem2  19762  dprddisj2  19832  ablfac1eulem  19865  ringpropd  20020  crngpropd  20021  mulgass3  20080  rngidpropd  20140  invrpropd  20143  isrhm2d  20176  subrgpropd  20307  rhmpropd  20308  lss0v  20534  lidlrsppropd  20759  ressmpladd  21467  ressmplmul  21468  ressmplvsca  21469  eqcoe1ply1eq  21705  resstopn  22574  lecldbas  22607  isref  22897  txhaus  23035  qustgplem  23509  tuslem  23655  tuslemOLD  23656  imasdsf1olem  23763  metustsym  23948  reconnlem1  24226  voliunlem1  24951  ismbf3d  25055  i1fima  25079  i1fd  25082  itgfsum  25228  dvmptc  25359  dvmptfsum  25376  dvfsumle  25422  dvfsumlem2  25428  itgsubst  25450  atantayl2  26325  chtdif  26544  ppidif  26549  pythi  29855  hvsubeq0i  30068  hvaddcani  30070  cmcmlem  30596  pj11i  30716  hosubeq0i  30831  riesz3i  31067  pjclem1  31200  pjclem3  31202  st0  31254  chirredi  31399  mdsymi  31416  difeq  31509  unidifsnne  31527  1nei  31721  subrgchr  32142  locfinref  32511  esumpfinvallem  32762  esum2dlem  32780  carsgclctun  33010  ballotlemgun  33213  cvmliftmolem1  33962  cvmlift3lem6  34005  msubff1  34237  isfne  34887  isfne4  34888  isfne4b  34889  bj-1uplth  35551  bj-2uplth  35565  matunitlindflem1  36147  ptrest  36150  poimirlem3  36154  poimirlem4  36155  poimirlem8  36159  poimirlem15  36166  mblfinlem2  36189  voliunnfl  36195  cdlemg47  39272  ltrnco4  39275  sn-1ne2  40839  sn-0tie0  40966  sn-inelr  40992  eldioph2  41143  binomcxplemdvbinom  42755  binomcxplemnotnn0  42758  compne  42843  rnfdmpr  45633