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  4386  disjdif2  4434  diftpsn3  4760  tppreqb  4763  xpid11  5891  cores2  6228  funcoeqres  6815  fvunsn  7137  caovmo  7607  dftpos2  8197  fvmpocurryd  8225  tfrlem16  8336  oev2  8462  domss2  9078  enp1ilem  9192  fipreima  9272  dfac5lem3  10049  fpwwe2lem12  10567  canthwelem  10575  canthp1lem2  10578  reclem3pr  10974  mulcmpblnrlem  10995  1idsr  11023  mulgt0sr  11030  mul02lem2  11324  ine0  11586  lo1eq  15505  rlimeq  15506  sumeq2ii  15630  fsumf1o  15660  sumss  15661  fsumss  15662  fsumadd  15677  fsumcom2  15711  fsum0diag2  15720  fsummulc2  15721  fsumrelem  15744  isumshft  15776  mertenslem1  15821  prodeq2ii  15848  fprodf1o  15883  prodss  15884  fprodss  15885  fprodmul  15897  fproddiv  15898  fprodcom2  15921  fprodmodd  15934  fprodefsum  16032  bitsinv1  16383  bitsinvp1  16390  4sqlem10  16889  setsnid  17149  topnpropd  17370  xpsff1o  17502  homfeqbas  17633  comfffval2  17638  comfeq  17643  oppchomfpropd  17663  isssc  17758  funcpropd  17840  hofpropd  18204  eqglact  19125  symgvalstruct  19343  lsmmod2  19622  vrgpinv  19715  frgpnabllem1  19819  frgpnabllem2  19820  gsum2dlem2  19917  dprddisj2  19987  ablfac1eulem  20020  ringpropd  20240  crngpropd  20241  mulgass3  20306  rngidpropd  20368  invrpropd  20371  isrhm2d  20439  subrngpropd  20518  subrgpropd  20558  rhmpropd  20559  lss0v  20985  lidlrsppropd  21216  ressmpladd  22001  ressmplmul  22002  ressmplvsca  22003  eqcoe1ply1eq  22260  resstopn  23147  lecldbas  23180  isref  23470  txhaus  23608  qustgplem  24082  tuslem  24227  imasdsf1olem  24334  metustsym  24516  reconnlem1  24788  voliunlem1  25524  ismbf3d  25628  i1fima  25652  i1fd  25655  itgfsum  25801  dvmptc  25935  dvmptfsum  25952  dvfsumle  25999  dvfsumleOLD  26000  dvfsumlem2  26006  dvfsumlem2OLD  26007  itgsubst  26029  atantayl2  26921  chtdif  27141  ppidif  27146  fsumdvdsmul  27178  onleft  28273  oncutlt  28277  pythi  30944  hvsubeq0i  31157  hvaddcani  31159  cmcmlem  31685  pj11i  31805  hosubeq0i  31920  riesz3i  32156  pjclem1  32289  pjclem3  32291  st0  32343  chirredi  32488  mdsymi  32505  difeq  32611  unidifsnne  32629  1nei  32833  subrgchr  33337  ressply1evls1  33664  srapwov  33772  locfinref  34025  esumpfinvallem  34258  esum2dlem  34276  carsgclctun  34505  ballotlemgun  34709  cvmliftmolem1  35503  cvmlift3lem6  35546  msubff1  35778  isfne  36561  isfne4  36562  isfne4b  36563  bj-1uplth  37282  bj-2uplth  37296  matunitlindflem1  37896  ptrest  37899  poimirlem3  37903  poimirlem4  37904  poimirlem8  37908  poimirlem15  37915  mblfinlem2  37938  voliunnfl  37944  cdlemg47  41141  ltrnco4  41144  sn-1ne2  42664  sn-00idlem3  42799  sn-0tie0  42850  sn-inelr  42886  eldioph2  43148  binomcxplemdvbinom  44738  binomcxplemnotnn0  44741  compne  44825  rnfdmpr  47670  cycl3grtri  48336