Theorem 3eqtr3g 2820

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754

This theorem is used by:  csbnest1g  4393  disjdif2  4439  diftpsn3  4768  tppreqb  4771  xpid11  5920  cores2  6260  funcoeqres  6853  fvunsn  7180  caovmo  7654  dftpos2  8244  fvmpocurryd  8272  tfrlem16  8385  oev2  8513  domss2  9137  enp1ilem  9251  fipreima  9328  dfac5lem3  10131  fpwwe2lem12  10652  canthwelem  10660  canthp1lem2  10663  reclem3pr  11059  mulcmpblnrlem  11080  1idsr  11108  mulgt0sr  11115  mul02lem2  11412  ine0  11674  lo1eq  15655  rlimeq  15656  sumeq2ii  15780  fsumf1o  15809  sumss  15810  fsumss  15811  fsumadd  15826  fsumcom2  15860  fsum0diag2  15869  fsummulc2  15870  fsumrelem  15894  isumshft  15928  mertenslem1  15973  prodeq2ii  16000  fprodf1o  16035  prodss  16036  fprodss  16037  fprodmul  16049  fproddiv  16050  fprodcom2  16073  fprodmodd  16086  fprodefsum  16183  bitsinv1  16534  bitsinvp1  16541  4sqlem10  17041  setsnid  17302  topnpropd  17523  xpsff1o  17655  homfeqbas  17786  comfffval2  17791  comfeq  17796  oppchomfpropd  17816  isssc  17911  funcpropd  17993  hofpropd  18357  eqglact  19303  symgvalstruct  19523  lsmmod2  19802  vrgpinv  19895  frgpnabllem1  19999  frgpnabllem2  20000  gsum2dlem2  20097  dprddisj2  20167  ablfac1eulem  20200  ringpropd  20429  crngpropd  20430  mulgass3  20493  rngidpropd  20555  invrpropd  20558  isrhm2d  20631  subrngpropd  20729  subrgpropd  20769  rhmpropd  20770  lss0v  21199  lidlrsppropd  21440  ressmpladd  22243  ressmplmul  22244  ressmplvsca  22245  eqcoe1ply1eq  22523  matunitlindflem1  22900  resstopn  23410  lecldbas  23443  isref  23734  txhaus  23872  qustgplem  24346  tuslem  24491  imasdsf1olem  24598  metustsym  24780  reconnlem1  25052  voliunlem1  25777  ismbf3d  25881  i1fima  25905  i1fd  25908  itgfsum  26054  dvmptc  26185  dvmptfsum  26202  dvfsumle  26248  dvfsumlem2  26254  itgsubst  26276  atantayl2  27171  chtdif  27390  ppidif  27395  fsumdvdsmul  27427  onleft  28521  oncutlt  28525  pythi  31315  hvsubeq0i  31528  hvaddcani  31530  cmcmlem  32056  pj11i  32176  hosubeq0i  32291  riesz3i  32527  pjclem1  32660  pjclem3  32662  st0  32714  chirredi  32859  mdsymi  32876  difeq  32977  unidifsnne  32995  1nei  33193  subrgchr  33661  ressply1evls1  33960  srapwov  34084  locfinref  34336  esumpfinvallem  34569  esum2dlem  34587  carsgclctun  34817  ballotlemgun  35021  cvmliftmolem1  35845  cvmlift3lem6  35888  msubff1  36120  isfne  36943  isfne4  36944  isfne4b  36945  bj-1uplth  37736  bj-2uplth  37750  ptrest  38353  poimirlem3  38357  poimirlem4  38358  poimirlem8  38362  poimirlem15  38369  mblfinlem2  38392  voliunnfl  38398  cdlemg47  41594  ltrnco4  41597  sn-1ne2  43131  sn-00idlem3  43260  sn-0tie0  43324  sn-inelr  43360  eldioph2  43592  binomcxplemdvbinom  45162  binomcxplemnotnn0  45165  compne  45249  rnfdmpr  48154  cycl3grtri  48848