Theorem 3eqtr3g 2793

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727

This theorem is referenced by:  csbnest1g  4383  disjdif2  4431  diftpsn3  4757  tppreqb  4760  xpid11  5880  cores2  6217  funcoeqres  6804  fvunsn  7125  caovmo  7595  dftpos2  8185  fvmpocurryd  8213  tfrlem16  8324  oev2  8450  domss2  9066  enp1ilem  9180  fipreima  9260  dfac5lem3  10037  fpwwe2lem12  10555  canthwelem  10563  canthp1lem2  10566  reclem3pr  10962  mulcmpblnrlem  10983  1idsr  11011  mulgt0sr  11018  mul02lem2  11312  ine0  11574  lo1eq  15493  rlimeq  15494  sumeq2ii  15618  fsumf1o  15648  sumss  15649  fsumss  15650  fsumadd  15665  fsumcom2  15699  fsum0diag2  15708  fsummulc2  15709  fsumrelem  15732  isumshft  15764  mertenslem1  15809  prodeq2ii  15836  fprodf1o  15871  prodss  15872  fprodss  15873  fprodmul  15885  fproddiv  15886  fprodcom2  15909  fprodmodd  15922  fprodefsum  16020  bitsinv1  16371  bitsinvp1  16378  4sqlem10  16877  setsnid  17137  topnpropd  17358  xpsff1o  17490  homfeqbas  17621  comfffval2  17626  comfeq  17631  oppchomfpropd  17651  isssc  17746  funcpropd  17828  hofpropd  18192  eqglact  19110  symgvalstruct  19328  lsmmod2  19607  vrgpinv  19700  frgpnabllem1  19804  frgpnabllem2  19805  gsum2dlem2  19902  dprddisj2  19972  ablfac1eulem  20005  ringpropd  20225  crngpropd  20226  mulgass3  20291  rngidpropd  20353  invrpropd  20356  isrhm2d  20424  subrngpropd  20503  subrgpropd  20543  rhmpropd  20544  lss0v  20970  lidlrsppropd  21201  ressmpladd  21986  ressmplmul  21987  ressmplvsca  21988  eqcoe1ply1eq  22245  resstopn  23132  lecldbas  23165  isref  23455  txhaus  23593  qustgplem  24067  tuslem  24212  imasdsf1olem  24319  metustsym  24501  reconnlem1  24773  voliunlem1  25509  ismbf3d  25613  i1fima  25637  i1fd  25640  itgfsum  25786  dvmptc  25920  dvmptfsum  25937  dvfsumle  25984  dvfsumleOLD  25985  dvfsumlem2  25991  dvfsumlem2OLD  25992  itgsubst  26014  atantayl2  26906  chtdif  27126  ppidif  27131  fsumdvdsmul  27163  onsleft  28239  onscutlt  28243  pythi  30906  hvsubeq0i  31119  hvaddcani  31121  cmcmlem  31647  pj11i  31767  hosubeq0i  31882  riesz3i  32118  pjclem1  32251  pjclem3  32253  st0  32305  chirredi  32450  mdsymi  32467  difeq  32573  unidifsnne  32591  1nei  32795  subrgchr  33298  ressply1evls1  33625  srapwov  33724  locfinref  33977  esumpfinvallem  34210  esum2dlem  34228  carsgclctun  34457  ballotlemgun  34661  cvmliftmolem1  35454  cvmlift3lem6  35497  msubff1  35729  isfne  36512  isfne4  36513  isfne4b  36514  bj-1uplth  37181  bj-2uplth  37195  matunitlindflem1  37786  ptrest  37789  poimirlem3  37793  poimirlem4  37794  poimirlem8  37798  poimirlem15  37805  mblfinlem2  37828  voliunnfl  37834  cdlemg47  41031  ltrnco4  41034  sn-1ne2  42557  sn-00idlem3  42692  sn-0tie0  42743  sn-inelr  42779  eldioph2  43041  binomcxplemdvbinom  44631  binomcxplemnotnn0  44634  compne  44718  rnfdmpr  47564  cycl3grtri  48230