Theorem 3eqtr3g 2789

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 2780	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtrdi 2782	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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  csbnest1g  4379  disjdif2  4427  diftpsn3  4751  tppreqb  4754  xpid11  5871  cores2  6207  funcoeqres  6794  fvunsn  7113  caovmo  7583  dftpos2  8173  fvmpocurryd  8201  tfrlem16  8312  oev2  8438  domss2  9049  enp1ilem  9162  fipreima  9242  dfac5lem3  10016  fpwwe2lem12  10533  canthwelem  10541  canthp1lem2  10544  reclem3pr  10940  mulcmpblnrlem  10961  1idsr  10989  mulgt0sr  10996  mul02lem2  11290  ine0  11552  lo1eq  15475  rlimeq  15476  sumeq2ii  15600  fsumf1o  15630  sumss  15631  fsumss  15632  fsumadd  15647  fsumcom2  15681  fsum0diag2  15690  fsummulc2  15691  fsumrelem  15714  isumshft  15746  mertenslem1  15791  prodeq2ii  15818  fprodf1o  15853  prodss  15854  fprodss  15855  fprodmul  15867  fproddiv  15868  fprodcom2  15891  fprodmodd  15904  fprodefsum  16002  bitsinv1  16353  bitsinvp1  16360  4sqlem10  16859  setsnid  17119  topnpropd  17340  xpsff1o  17471  homfeqbas  17602  comfffval2  17607  comfeq  17612  oppchomfpropd  17632  isssc  17727  funcpropd  17809  hofpropd  18173  eqglact  19091  symgvalstruct  19309  lsmmod2  19588  vrgpinv  19681  frgpnabllem1  19785  frgpnabllem2  19786  gsum2dlem2  19883  dprddisj2  19953  ablfac1eulem  19986  ringpropd  20206  crngpropd  20207  mulgass3  20271  rngidpropd  20333  invrpropd  20336  isrhm2d  20404  subrngpropd  20483  subrgpropd  20523  rhmpropd  20524  lss0v  20950  lidlrsppropd  21181  ressmpladd  21964  ressmplmul  21965  ressmplvsca  21966  eqcoe1ply1eq  22214  resstopn  23101  lecldbas  23134  isref  23424  txhaus  23562  qustgplem  24036  tuslem  24181  imasdsf1olem  24288  metustsym  24470  reconnlem1  24742  voliunlem1  25478  ismbf3d  25582  i1fima  25606  i1fd  25609  itgfsum  25755  dvmptc  25889  dvmptfsum  25906  dvfsumle  25953  dvfsumleOLD  25954  dvfsumlem2  25960  dvfsumlem2OLD  25961  itgsubst  25983  atantayl2  26875  chtdif  27095  ppidif  27100  fsumdvdsmul  27132  onsleft  28197  onscutlt  28201  pythi  30830  hvsubeq0i  31043  hvaddcani  31045  cmcmlem  31571  pj11i  31691  hosubeq0i  31806  riesz3i  32042  pjclem1  32175  pjclem3  32177  st0  32229  chirredi  32374  mdsymi  32391  difeq  32498  unidifsnne  32516  1nei  32720  subrgchr  33204  ressply1evls1  33528  srapwov  33601  locfinref  33854  esumpfinvallem  34087  esum2dlem  34105  carsgclctun  34334  ballotlemgun  34538  cvmliftmolem1  35325  cvmlift3lem6  35368  msubff1  35600  isfne  36383  isfne4  36384  isfne4b  36385  bj-1uplth  37051  bj-2uplth  37065  matunitlindflem1  37655  ptrest  37658  poimirlem3  37662  poimirlem4  37663  poimirlem8  37667  poimirlem15  37674  mblfinlem2  37697  voliunnfl  37703  cdlemg47  40834  ltrnco4  40837  sn-1ne2  42357  sn-00idlem3  42492  sn-0tie0  42543  sn-inelr  42579  eldioph2  42854  binomcxplemdvbinom  44445  binomcxplemnotnn0  44448  compne  44532  rnfdmpr  47380  cycl3grtri  48046