Theorem 3eqtr3g 2799

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

Syntax hints:   → wi 4   = wceq 1540

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2728

This theorem is referenced by:  csbnest1g  4375  disjdif2  4425  diftpsn3  4748  tppreqb  4751  xpid11  5867  cores2  6191  funcoeqres  6792  fvunsn  7101  caovmo  7563  dftpos2  8121  fvmpocurryd  8149  tfrlem16  8286  oev2  8416  domss2  8993  enp1ilem  9135  fipreima  9215  dfac5lem3  9974  fpwwe2lem12  10491  canthwelem  10499  canthp1lem2  10502  reclem3pr  10898  mulcmpblnrlem  10919  1idsr  10947  mulgt0sr  10954  mul02lem2  11245  ine0  11503  lo1eq  15368  rlimeq  15369  sumeq2ii  15496  fsumf1o  15526  sumss  15527  fsumss  15528  fsumadd  15543  fsumcom2  15577  fsum0diag2  15586  fsummulc2  15587  fsumrelem  15610  isumshft  15642  mertenslem1  15687  prodeq2ii  15714  fprodf1o  15747  prodss  15748  fprodss  15749  fprodmul  15761  fproddiv  15762  fprodcom2  15785  fprodmodd  15798  fprodefsum  15895  bitsinv1  16240  bitsinvp1  16247  4sqlem10  16737  setsnid  16999  setsnidOLD  17000  topnpropd  17236  xpsff1o  17367  homfeqbas  17494  comfffval2  17499  comfeq  17504  oppchomfpropd  17526  isssc  17621  funcpropd  17705  hofpropd  18074  eqglact  18895  symgvalstruct  19092  symgvalstructOLD  19093  lsmmod2  19369  vrgpinv  19462  frgpnabllem1  19561  frgpnabllem2  19562  gsum2dlem2  19659  dprddisj2  19729  ablfac1eulem  19762  ringpropd  19908  crngpropd  19909  mulgass3  19966  rngidpropd  20024  invrpropd  20027  isrhm2d  20060  subrgpropd  20156  rhmpropd  20157  lss0v  20376  lidlrsppropd  20599  ressmpladd  21328  ressmplmul  21329  ressmplvsca  21330  eqcoe1ply1eq  21566  resstopn  22435  lecldbas  22468  isref  22758  txhaus  22896  qustgplem  23370  tuslem  23516  tuslemOLD  23517  imasdsf1olem  23624  metustsym  23809  reconnlem1  24087  voliunlem1  24812  ismbf3d  24916  i1fima  24940  i1fd  24943  itgfsum  25089  dvmptc  25220  dvmptfsum  25237  dvfsumle  25283  dvfsumlem2  25289  itgsubst  25311  atantayl2  26186  chtdif  26405  ppidif  26410  pythi  29441  hvsubeq0i  29654  hvaddcani  29656  cmcmlem  30182  pj11i  30302  hosubeq0i  30417  riesz3i  30653  pjclem1  30786  pjclem3  30788  st0  30840  chirredi  30985  mdsymi  31002  difeq  31094  unidifsnne  31112  1nei  31299  subrgchr  31719  locfinref  32030  esumpfinvallem  32281  esum2dlem  32299  carsgclctun  32529  ballotlemgun  32732  cvmliftmolem1  33483  cvmlift3lem6  33526  msubff1  33758  isfne  34619  isfne4  34620  isfne4b  34621  bj-1uplth  35286  bj-2uplth  35300  matunitlindflem1  35871  ptrest  35874  poimirlem3  35878  poimirlem4  35879  poimirlem8  35883  poimirlem15  35890  mblfinlem2  35913  voliunnfl  35919  cdlemg47  38997  ltrnco4  39000  sn-1ne2  40545  sn-0tie0  40671  sn-inelr  40685  eldioph2  40834  binomcxplemdvbinom  42281  binomcxplemnotnn0  42284  compne  42369  rnfdmpr  45113