Theorem 3eqtr3g 2795

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

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

This theorem is referenced by:  csbnest1g  4385  disjdif2  4433  diftpsn3  4759  tppreqb  4762  xpid11  5882  cores2  6219  funcoeqres  6806  fvunsn  7127  caovmo  7597  dftpos2  8187  fvmpocurryd  8215  tfrlem16  8326  oev2  8452  domss2  9068  enp1ilem  9182  fipreima  9262  dfac5lem3  10039  fpwwe2lem12  10557  canthwelem  10565  canthp1lem2  10568  reclem3pr  10964  mulcmpblnrlem  10985  1idsr  11013  mulgt0sr  11020  mul02lem2  11314  ine0  11576  lo1eq  15495  rlimeq  15496  sumeq2ii  15620  fsumf1o  15650  sumss  15651  fsumss  15652  fsumadd  15667  fsumcom2  15701  fsum0diag2  15710  fsummulc2  15711  fsumrelem  15734  isumshft  15766  mertenslem1  15811  prodeq2ii  15838  fprodf1o  15873  prodss  15874  fprodss  15875  fprodmul  15887  fproddiv  15888  fprodcom2  15911  fprodmodd  15924  fprodefsum  16022  bitsinv1  16373  bitsinvp1  16380  4sqlem10  16879  setsnid  17139  topnpropd  17360  xpsff1o  17492  homfeqbas  17623  comfffval2  17628  comfeq  17633  oppchomfpropd  17653  isssc  17748  funcpropd  17830  hofpropd  18194  eqglact  19112  symgvalstruct  19330  lsmmod2  19609  vrgpinv  19702  frgpnabllem1  19806  frgpnabllem2  19807  gsum2dlem2  19904  dprddisj2  19974  ablfac1eulem  20007  ringpropd  20227  crngpropd  20228  mulgass3  20293  rngidpropd  20355  invrpropd  20358  isrhm2d  20426  subrngpropd  20505  subrgpropd  20545  rhmpropd  20546  lss0v  20972  lidlrsppropd  21203  ressmpladd  21988  ressmplmul  21989  ressmplvsca  21990  eqcoe1ply1eq  22247  resstopn  23134  lecldbas  23167  isref  23457  txhaus  23595  qustgplem  24069  tuslem  24214  imasdsf1olem  24321  metustsym  24503  reconnlem1  24775  voliunlem1  25511  ismbf3d  25615  i1fima  25639  i1fd  25642  itgfsum  25788  dvmptc  25922  dvmptfsum  25939  dvfsumle  25986  dvfsumleOLD  25987  dvfsumlem2  25993  dvfsumlem2OLD  25994  itgsubst  26016  atantayl2  26908  chtdif  27128  ppidif  27133  fsumdvdsmul  27165  onleft  28260  oncutlt  28264  pythi  30929  hvsubeq0i  31142  hvaddcani  31144  cmcmlem  31670  pj11i  31790  hosubeq0i  31905  riesz3i  32141  pjclem1  32274  pjclem3  32276  st0  32328  chirredi  32473  mdsymi  32490  difeq  32596  unidifsnne  32614  1nei  32818  subrgchr  33321  ressply1evls1  33648  srapwov  33747  locfinref  34000  esumpfinvallem  34233  esum2dlem  34251  carsgclctun  34480  ballotlemgun  34684  cvmliftmolem1  35477  cvmlift3lem6  35520  msubff1  35752  isfne  36535  isfne4  36536  isfne4b  36537  bj-1uplth  37210  bj-2uplth  37224  matunitlindflem1  37819  ptrest  37822  poimirlem3  37826  poimirlem4  37827  poimirlem8  37831  poimirlem15  37838  mblfinlem2  37861  voliunnfl  37867  cdlemg47  41064  ltrnco4  41067  sn-1ne2  42587  sn-00idlem3  42722  sn-0tie0  42773  sn-inelr  42809  eldioph2  43071  binomcxplemdvbinom  44661  binomcxplemnotnn0  44664  compne  44748  rnfdmpr  47594  cycl3grtri  48260