Theorem 3eqtr3g 2818

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

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

This theorem is used by:  csbnest1g  4390  disjdif2  4436  diftpsn3  4765  tppreqb  4768  xpid11  5916  cores2  6256  funcoeqres  6849  fvunsn  7177  caovmo  7651  dftpos2  8241  fvmpocurryd  8269  tfrlem16  8382  oev2  8510  domss2  9134  enp1ilem  9248  fipreima  9325  dfac5lem3  10128  fpwwe2lem12  10651  canthwelem  10659  canthp1lem2  10662  reclem3pr  11058  mulcmpblnrlem  11079  1idsr  11107  mulgt0sr  11114  mul02lem2  11411  ine0  11673  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  16033  prodss  16034  fprodss  16035  fprodmul  16047  fproddiv  16048  fprodcom2  16071  fprodmodd  16084  fprodefsum  16181  bitsinv1  16532  bitsinvp1  16539  4sqlem10  17039  setsnid  17300  topnpropd  17521  xpsff1o  17653  homfeqbas  17784  comfffval2  17789  comfeq  17794  oppchomfpropd  17814  isssc  17909  funcpropd  17991  hofpropd  18355  eqglact  19304  symgvalstruct  19524  lsmmod2  19803  vrgpinv  19896  frgpnabllem1  20000  frgpnabllem2  20001  gsum2dlem2  20098  dprddisj2  20168  ablfac1eulem  20201  ringpropd  20430  crngpropd  20431  mulgass3  20494  rngidpropd  20556  invrpropd  20559  isrhm2d  20632  subrngpropd  20730  subrgpropd  20770  rhmpropd  20771  lss0v  21200  lidlrsppropd  21441  ressmpladd  22244  ressmplmul  22245  ressmplvsca  22246  eqcoe1ply1eq  22524  matunitlindflem1  22901  resstopn  23411  lecldbas  23444  isref  23735  txhaus  23873  qustgplem  24347  tuslem  24492  imasdsf1olem  24599  metustsym  24781  reconnlem1  25053  voliunlem1  25778  ismbf3d  25882  i1fima  25906  i1fd  25909  itgfsum  26054  dvmptc  26185  dvmptfsum  26202  dvfsumle  26248  dvfsumlem2  26254  itgsubst  26276  atantayl2  27175  chtdif  27394  ppidif  27399  fsumdvdsmul  27431  onleft  28525  oncutlt  28529  pythi  31331  hvsubeq0i  31544  hvaddcani  31546  cmcmlem  32072  pj11i  32192  hosubeq0i  32307  riesz3i  32543  pjclem1  32676  pjclem3  32678  st0  32730  chirredi  32875  mdsymi  32892  difeq  32993  unidifsnne  33011  1nei  33208  subrgchr  33676  ressply1evls1  33975  srapwov  34099  locfinref  34351  esumpfinvallem  34584  esum2dlem  34602  carsgclctun  34832  ballotlemgun  35036  cvmliftmolem1  35860  cvmlift3lem6  35903  msubff1  36135  isfne  36958  isfne4  36959  isfne4b  36960  bj-1uplth  37751  bj-2uplth  37765  ptrest  38368  poimirlem3  38372  poimirlem4  38373  poimirlem8  38377  poimirlem15  38384  mblfinlem2  38407  voliunnfl  38413  cdlemg47  41609  ltrnco4  41612  sn-1ne2  43146  sn-00idlem3  43275  sn-0tie0  43339  sn-inelr  43375  eldioph2  43607  binomcxplemdvbinom  45177  binomcxplemnotnn0  45180  compne  45264  rnfdmpr  48169  cycl3grtri  48863