Theorem 3eqtr3g 2818

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  csbnest1g  4389  disjdif2  4435  diftpsn3  4764  tppreqb  4767  xpid11  5913  cores2  6261  funcoeqres  6856  fvunsn  7184  caovmo  7658  dftpos2  8260  fvmpocurryd  8288  tfrlem16  8401  oev2  8531  domss2  9155  enp1ilem  9269  fipreima  9347  dfac5lem3  10204  fpwwe2lem12  10727  canthwelem  10735  canthp1lem2  10738  reclem3pr  11134  mulcmpblnrlem  11155  1idsr  11183  mulgt0sr  11190  mul02lem2  11487  ine0  11751  lo1eq  15735  rlimeq  15736  sumeq2ii  15860  fsumf1o  15889  sumss  15890  fsumss  15891  fsumadd  15906  fsumcom2  15940  fsum0diag2  15949  fsummulc2  15950  fsumrelem  15974  isumshft  16008  mertenslem1  16053  prodeq2ii  16080  fprodf1o  16113  prodss  16114  fprodss  16115  fprodmul  16127  fproddiv  16128  fprodcom2  16151  fprodmodd  16164  fprodefsum  16261  bitsinv1  16612  bitsinvp1  16619  4sqlem10  17125  setsnid  17386  topnpropd  17607  xpsff1o  17739  homfeqbas  17870  comfffval2  17875  comfeq  17880  oppchomfpropd  17900  isssc  17995  funcpropd  18077  hofpropd  18441  eqglact  19391  symgvalstruct  19611  lsmmod2  19890  vrgpinv  19983  frgpnabllem1  20087  frgpnabllem2  20088  gsum2dlem2  20185  dprddisj2  20255  ablfac1eulem  20288  ringpropd  20519  crngpropd  20520  mulgass3  20583  rngidpropd  20645  invrpropd  20648  isrhm2d  20721  subrngpropd  20820  subrgpropd  20860  rhmpropd  20861  lss0v  21291  lidlrsppropd  21532  ressmpladd  22337  ressmplmul  22338  ressmplvsca  22339  eqcoe1ply1eq  22617  matunitlindflem1  22994  resstopn  23504  lecldbas  23537  isref  23828  txhaus  23966  qustgplem  24440  tuslem  24585  imasdsf1olem  24692  metustsym  24874  reconnlem1  25146  voliunlem1  25871  ismbf3d  25975  i1fima  25999  i1fd  26002  itgfsum  26147  dvmptc  26278  dvmptfsum  26295  dvfsumle  26341  dvfsumlem2  26347  itgsubst  26369  atantayl2  27266  chtdif  27485  ppidif  27490  fsumdvdsmul  27522  onleft  28646  oncutlt  28650  pythi  31452  hvsubeq0i  31665  hvaddcani  31667  cmcmlem  32193  pj11i  32313  hosubeq0i  32428  riesz3i  32664  pjclem1  32797  pjclem3  32799  st0  32851  chirredi  32996  mdsymi  33013  difeq  33156  unidifsnne  33174  1nei  33371  subrgchr  33839  ressply1evls1  34139  srapwov  34263  locfinref  34515  esumpfinvallem  34748  esum2dlem  34766  carsgclctun  34995  ballotlemgun  35199  cvmliftmolem1  36088  cvmlift3lem6  36131  msubff1  36363  isfne  37169  isfne4  37170  isfne4b  37171  bj-1uplth  37962  bj-2uplth  37976  ptrest  38580  poimirlem3  38584  poimirlem4  38585  poimirlem8  38589  poimirlem15  38596  mblfinlem2  38619  voliunnfl  38625  cdlemg47  41836  ltrnco4  41839  sn-1ne2  43373  sn-00idlem3  43494  sn-0tie0  43558  sn-inelr  43594  eldioph2  43815  binomcxplemdvbinom  45379  binomcxplemnotnn0  45382  compne  45466  rnfdmpr  48393  cycl3grtri  49087