Theorem 3eqtr3g 2787

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  csbnest1g  4395  disjdif2  4443  diftpsn3  4766  tppreqb  4769  xpid11  5896  cores2  6232  funcoeqres  6831  fvunsn  7153  caovmo  7626  dftpos2  8222  fvmpocurryd  8250  tfrlem16  8361  oev2  8487  domss2  9100  enp1ilem  9223  fipreima  9309  dfac5lem3  10078  fpwwe2lem12  10595  canthwelem  10603  canthp1lem2  10606  reclem3pr  11002  mulcmpblnrlem  11023  1idsr  11051  mulgt0sr  11058  mul02lem2  11351  ine0  11613  lo1eq  15534  rlimeq  15535  sumeq2ii  15659  fsumf1o  15689  sumss  15690  fsumss  15691  fsumadd  15706  fsumcom2  15740  fsum0diag2  15749  fsummulc2  15750  fsumrelem  15773  isumshft  15805  mertenslem1  15850  prodeq2ii  15877  fprodf1o  15912  prodss  15913  fprodss  15914  fprodmul  15926  fproddiv  15927  fprodcom2  15950  fprodmodd  15963  fprodefsum  16061  bitsinv1  16412  bitsinvp1  16419  4sqlem10  16918  setsnid  17178  topnpropd  17399  xpsff1o  17530  homfeqbas  17657  comfffval2  17662  comfeq  17667  oppchomfpropd  17687  isssc  17782  funcpropd  17864  hofpropd  18228  eqglact  19111  symgvalstruct  19327  lsmmod2  19606  vrgpinv  19699  frgpnabllem1  19803  frgpnabllem2  19804  gsum2dlem2  19901  dprddisj2  19971  ablfac1eulem  20004  ringpropd  20197  crngpropd  20198  mulgass3  20262  rngidpropd  20324  invrpropd  20327  isrhm2d  20396  subrngpropd  20477  subrgpropd  20517  rhmpropd  20518  lss0v  20923  lidlrsppropd  21154  ressmpladd  21936  ressmplmul  21937  ressmplvsca  21938  eqcoe1ply1eq  22186  resstopn  23073  lecldbas  23106  isref  23396  txhaus  23534  qustgplem  24008  tuslem  24154  imasdsf1olem  24261  metustsym  24443  reconnlem1  24715  voliunlem1  25451  ismbf3d  25555  i1fima  25579  i1fd  25582  itgfsum  25728  dvmptc  25862  dvmptfsum  25879  dvfsumle  25926  dvfsumleOLD  25927  dvfsumlem2  25933  dvfsumlem2OLD  25934  itgsubst  25956  atantayl2  26848  chtdif  27068  ppidif  27073  fsumdvdsmul  27105  onsleft  28161  onscutlt  28165  pythi  30779  hvsubeq0i  30992  hvaddcani  30994  cmcmlem  31520  pj11i  31640  hosubeq0i  31755  riesz3i  31991  pjclem1  32124  pjclem3  32126  st0  32178  chirredi  32323  mdsymi  32340  difeq  32447  unidifsnne  32465  1nei  32660  subrgchr  33188  ressply1evls1  33534  locfinref  33831  esumpfinvallem  34064  esum2dlem  34082  carsgclctun  34312  ballotlemgun  34516  cvmliftmolem1  35268  cvmlift3lem6  35311  msubff1  35543  isfne  36327  isfne4  36328  isfne4b  36329  bj-1uplth  36995  bj-2uplth  37009  matunitlindflem1  37610  ptrest  37613  poimirlem3  37617  poimirlem4  37618  poimirlem8  37622  poimirlem15  37629  mblfinlem2  37652  voliunnfl  37658  cdlemg47  40730  ltrnco4  40733  sn-1ne2  42253  sn-00idlem3  42388  sn-0tie0  42439  sn-inelr  42475  eldioph2  42750  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  compne  44430  rnfdmpr  47282  cycl3grtri  47946