Theorem 3eqtr3g 2797

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

Syntax hints:   → wi 4   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  csbnest1g  4437  disjdif2  4485  diftpsn3  4806  tppreqb  4809  xpid11  5945  cores2  6280  funcoeqres  6879  fvunsn  7198  caovmo  7669  dftpos2  8266  fvmpocurryd  8294  tfrlem16  8431  oev2  8559  domss2  9174  enp1ilem  9309  fipreima  9395  dfac5lem3  10162  fpwwe2lem12  10679  canthwelem  10687  canthp1lem2  10690  reclem3pr  11086  mulcmpblnrlem  11107  1idsr  11135  mulgt0sr  11142  mul02lem2  11435  ine0  11695  lo1eq  15600  rlimeq  15601  sumeq2ii  15725  fsumf1o  15755  sumss  15756  fsumss  15757  fsumadd  15772  fsumcom2  15806  fsum0diag2  15815  fsummulc2  15816  fsumrelem  15839  isumshft  15871  mertenslem1  15916  prodeq2ii  15943  fprodf1o  15978  prodss  15979  fprodss  15980  fprodmul  15992  fproddiv  15993  fprodcom2  16016  fprodmodd  16029  fprodefsum  16127  bitsinv1  16475  bitsinvp1  16482  4sqlem10  16980  setsnid  17242  setsnidOLD  17243  topnpropd  17482  xpsff1o  17613  homfeqbas  17740  comfffval2  17745  comfeq  17750  oppchomfpropd  17772  isssc  17867  funcpropd  17953  hofpropd  18323  eqglact  19209  symgvalstruct  19428  symgvalstructOLD  19429  lsmmod2  19708  vrgpinv  19801  frgpnabllem1  19905  frgpnabllem2  19906  gsum2dlem2  20003  dprddisj2  20073  ablfac1eulem  20106  ringpropd  20301  crngpropd  20302  mulgass3  20369  rngidpropd  20431  invrpropd  20434  isrhm2d  20503  subrngpropd  20584  subrgpropd  20624  rhmpropd  20625  lss0v  21032  lidlrsppropd  21271  ressmpladd  22064  ressmplmul  22065  ressmplvsca  22066  eqcoe1ply1eq  22318  resstopn  23209  lecldbas  23242  isref  23532  txhaus  23670  qustgplem  24144  tuslem  24290  tuslemOLD  24291  imasdsf1olem  24398  metustsym  24583  reconnlem1  24861  voliunlem1  25598  ismbf3d  25702  i1fima  25726  i1fd  25729  itgfsum  25876  dvmptc  26010  dvmptfsum  26027  dvfsumle  26074  dvfsumleOLD  26075  dvfsumlem2  26081  dvfsumlem2OLD  26082  itgsubst  26104  atantayl2  26995  chtdif  27215  ppidif  27220  fsumdvdsmul  27252  sltonold  28297  pythi  30878  hvsubeq0i  31091  hvaddcani  31093  cmcmlem  31619  pj11i  31739  hosubeq0i  31854  riesz3i  32090  pjclem1  32223  pjclem3  32225  st0  32277  chirredi  32422  mdsymi  32439  difeq  32545  unidifsnne  32561  1nei  32753  subrgchr  33226  locfinref  33801  esumpfinvallem  34054  esum2dlem  34072  carsgclctun  34302  ballotlemgun  34505  cvmliftmolem1  35265  cvmlift3lem6  35308  msubff1  35540  isfne  36321  isfne4  36322  isfne4b  36323  bj-1uplth  36989  bj-2uplth  37003  matunitlindflem1  37602  ptrest  37605  poimirlem3  37609  poimirlem4  37610  poimirlem8  37614  poimirlem15  37621  mblfinlem2  37644  voliunnfl  37650  cdlemg47  40718  ltrnco4  40721  sn-1ne2  42278  sn-0tie0  42445  sn-inelr  42473  eldioph2  42749  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  compne  44436  rnfdmpr  47230