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 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728

This theorem is referenced by:  csbnest1g  4369  disjdif2  4419  diftpsn3  4741  tppreqb  4744  xpid11  5853  cores2  6177  funcoeqres  6777  fvunsn  7083  caovmo  7541  dftpos2  8090  fvmpocurryd  8118  tfrlem16  8255  oev2  8384  domss2  8961  enp1ilem  9095  fipreima  9169  dfac5lem3  9927  fpwwe2lem12  10444  canthwelem  10452  canthp1lem2  10455  reclem3pr  10851  mulcmpblnrlem  10872  1idsr  10900  mulgt0sr  10907  mul02lem2  11198  ine0  11456  lo1eq  15322  rlimeq  15323  sumeq2ii  15450  fsumf1o  15480  sumss  15481  fsumss  15482  fsumadd  15497  fsumcom2  15531  fsum0diag2  15540  fsummulc2  15541  fsumrelem  15564  isumshft  15596  mertenslem1  15641  prodeq2ii  15668  fprodf1o  15701  prodss  15702  fprodss  15703  fprodmul  15715  fproddiv  15716  fprodcom2  15739  fprodmodd  15752  fprodefsum  15849  bitsinv1  16194  bitsinvp1  16201  4sqlem10  16693  setsnid  16955  setsnidOLD  16956  topnpropd  17192  xpsff1o  17323  homfeqbas  17450  comfffval2  17455  comfeq  17460  oppchomfpropd  17482  isssc  17577  funcpropd  17661  hofpropd  18030  eqglact  18852  symgvalstruct  19049  symgvalstructOLD  19050  lsmmod2  19327  vrgpinv  19420  frgpnabllem1  19519  frgpnabllem2  19520  gsum2dlem2  19617  dprddisj2  19687  ablfac1eulem  19720  ringpropd  19866  crngpropd  19867  mulgass3  19924  rngidpropd  19982  invrpropd  19985  isrhm2d  20017  subrgpropd  20104  rhmpropd  20105  lss0v  20323  lidlrsppropd  20546  ressmpladd  21275  ressmplmul  21276  ressmplvsca  21277  eqcoe1ply1eq  21513  resstopn  22382  lecldbas  22415  isref  22705  txhaus  22843  qustgplem  23317  tuslem  23463  tuslemOLD  23464  imasdsf1olem  23571  metustsym  23756  reconnlem1  24034  voliunlem1  24759  ismbf3d  24863  i1fima  24887  i1fd  24890  itgfsum  25036  dvmptc  25167  dvmptfsum  25184  dvfsumle  25230  dvfsumlem2  25236  itgsubst  25258  atantayl2  26133  chtdif  26352  ppidif  26357  pythi  29257  hvsubeq0i  29470  hvaddcani  29472  cmcmlem  29998  pj11i  30118  hosubeq0i  30233  riesz3i  30469  pjclem1  30602  pjclem3  30604  st0  30656  chirredi  30801  mdsymi  30818  difeq  30910  unidifsnne  30929  1nei  31116  subrgchr  31536  locfinref  31836  esumpfinvallem  32087  esum2dlem  32105  carsgclctun  32333  ballotlemgun  32536  cvmliftmolem1  33288  cvmlift3lem6  33331  msubff1  33563  isfne  34573  isfne4  34574  isfne4b  34575  bj-1uplth  35241  bj-2uplth  35255  matunitlindflem1  35817  ptrest  35820  poimirlem3  35824  poimirlem4  35825  poimirlem8  35829  poimirlem15  35836  mblfinlem2  35859  voliunnfl  35865  cdlemg47  38792  ltrnco4  38795  sn-1ne2  40332  sn-0tie0  40458  sn-inelr  40472  eldioph2  40621  binomcxplemdvbinom  42009  binomcxplemnotnn0  42012  compne  42097  rnfdmpr  44831