Theorem 3eqtr3g 2822

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

Syntax hints:   → wi 4   = wceq 1562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756

This theorem is referenced by:  csbnest1g  4388  disjdif2  4436  diftpsn3  4764  tppreqb  4767  xpid11  5910  cores2  6249  funcoeqres  6840  fvunsn  7165  caovmo  7635  dftpos2  8225  fvmpocurryd  8253  tfrlem16  8366  oev2  8494  domss2  9110  enp1ilem  9224  fipreima  9303  dfac5lem3  10083  fpwwe2lem12  10602  canthwelem  10610  canthp1lem2  10613  reclem3pr  11009  mulcmpblnrlem  11030  1idsr  11058  mulgt0sr  11065  mul02lem2  11362  ine0  11624  lo1eq  15597  rlimeq  15598  sumeq2ii  15722  fsumf1o  15752  sumss  15753  fsumss  15754  fsumadd  15769  fsumcom2  15803  fsum0diag2  15812  fsummulc2  15813  fsumrelem  15837  isumshft  15871  mertenslem1  15916  prodeq2ii  15943  fprodf1o  15978  prodss  15979  fprodss  15980  fprodmul  15992  fproddiv  15993  fprodcom2  16016  fprodmodd  16029  fprodefsum  16127  bitsinv1  16478  bitsinvp1  16485  4sqlem10  16985  setsnid  17246  topnpropd  17467  xpsff1o  17599  homfeqbas  17730  comfffval2  17735  comfeq  17740  oppchomfpropd  17760  isssc  17855  funcpropd  17937  hofpropd  18301  eqglact  19222  symgvalstruct  19439  lsmmod2  19718  vrgpinv  19811  frgpnabllem1  19915  frgpnabllem2  19916  gsum2dlem2  20013  dprddisj2  20083  ablfac1eulem  20116  ringpropd  20340  crngpropd  20341  mulgass3  20404  rngidpropd  20466  invrpropd  20469  isrhm2d  20538  subrngpropd  20620  subrgpropd  20660  rhmpropd  20661  lss0v  21085  lidlrsppropd  21316  ressmpladd  22083  ressmplmul  22084  ressmplvsca  22085  eqcoe1ply1eq  22364  resstopn  23248  lecldbas  23281  isref  23571  txhaus  23709  qustgplem  24183  tuslem  24328  imasdsf1olem  24435  metustsym  24617  reconnlem1  24889  voliunlem1  25614  ismbf3d  25718  i1fima  25742  i1fd  25745  itgfsum  25891  dvmptc  26022  dvmptfsum  26039  dvfsumle  26085  dvfsumlem2  26091  itgsubst  26113  atantayl2  27005  chtdif  27224  ppidif  27229  fsumdvdsmul  27261  onleft  28355  oncutlt  28359  pythi  31055  hvsubeq0i  31268  hvaddcani  31270  cmcmlem  31796  pj11i  31916  hosubeq0i  32031  riesz3i  32267  pjclem1  32400  pjclem3  32402  st0  32454  chirredi  32599  mdsymi  32616  difeq  32719  unidifsnne  32737  1nei  32941  subrgchr  33419  ressply1evls1  33763  srapwov  33888  locfinref  34140  esumpfinvallem  34373  esum2dlem  34391  carsgclctun  34620  ballotlemgun  34824  cvmliftmolem1  35636  cvmlift3lem6  35679  msubff1  35911  isfne  36704  isfne4  36705  isfne4b  36706  bj-1uplth  37497  bj-2uplth  37511  matunitlindflem1  38120  ptrest  38123  poimirlem3  38127  poimirlem4  38128  poimirlem8  38132  poimirlem15  38139  mblfinlem2  38162  voliunnfl  38168  cdlemg47  41365  ltrnco4  41368  sn-1ne2  42885  sn-00idlem3  43014  sn-0tie0  43078  sn-inelr  43114  eldioph2  43348  binomcxplemdvbinom  44934  binomcxplemnotnn0  44937  compne  45021  rnfdmpr  47880  cycl3grtri  48574