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  4383  disjdif2  4431  diftpsn3  4753  tppreqb  4756  xpid11  5874  cores2  6208  funcoeqres  6795  fvunsn  7115  caovmo  7586  dftpos2  8176  fvmpocurryd  8204  tfrlem16  8315  oev2  8441  domss2  9053  enp1ilem  9167  fipreima  9248  dfac5lem3  10019  fpwwe2lem12  10536  canthwelem  10544  canthp1lem2  10547  reclem3pr  10943  mulcmpblnrlem  10964  1idsr  10992  mulgt0sr  10999  mul02lem2  11293  ine0  11555  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  19058  symgvalstruct  19276  lsmmod2  19555  vrgpinv  19648  frgpnabllem1  19752  frgpnabllem2  19753  gsum2dlem2  19850  dprddisj2  19920  ablfac1eulem  19953  ringpropd  20173  crngpropd  20174  mulgass3  20238  rngidpropd  20300  invrpropd  20303  isrhm2d  20372  subrngpropd  20453  subrgpropd  20493  rhmpropd  20494  lss0v  20920  lidlrsppropd  21151  ressmpladd  21934  ressmplmul  21935  ressmplvsca  21936  eqcoe1ply1eq  22184  resstopn  23071  lecldbas  23104  isref  23394  txhaus  23532  qustgplem  24006  tuslem  24152  imasdsf1olem  24259  metustsym  24441  reconnlem1  24713  voliunlem1  25449  ismbf3d  25553  i1fima  25577  i1fd  25580  itgfsum  25726  dvmptc  25860  dvmptfsum  25877  dvfsumle  25924  dvfsumleOLD  25925  dvfsumlem2  25931  dvfsumlem2OLD  25932  itgsubst  25954  atantayl2  26846  chtdif  27066  ppidif  27071  fsumdvdsmul  27103  onsleft  28168  onscutlt  28172  pythi  30798  hvsubeq0i  31011  hvaddcani  31013  cmcmlem  31539  pj11i  31659  hosubeq0i  31774  riesz3i  32010  pjclem1  32143  pjclem3  32145  st0  32197  chirredi  32342  mdsymi  32359  difeq  32467  unidifsnne  32485  1nei  32689  subrgchr  33186  ressply1evls1  33509  srapwov  33571  locfinref  33824  esumpfinvallem  34057  esum2dlem  34075  carsgclctun  34305  ballotlemgun  34509  cvmliftmolem1  35274  cvmlift3lem6  35317  msubff1  35549  isfne  36333  isfne4  36334  isfne4b  36335  bj-1uplth  37001  bj-2uplth  37015  matunitlindflem1  37616  ptrest  37619  poimirlem3  37623  poimirlem4  37624  poimirlem8  37628  poimirlem15  37635  mblfinlem2  37658  voliunnfl  37664  cdlemg47  40735  ltrnco4  40738  sn-1ne2  42258  sn-00idlem3  42393  sn-0tie0  42444  sn-inelr  42480  eldioph2  42755  binomcxplemdvbinom  44346  binomcxplemnotnn0  44349  compne  44434  rnfdmpr  47285  cycl3grtri  47951