Theorem 3eqtr3g 2800

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 2791	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtrdi 2793	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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  csbnest1g  4432  disjdif2  4480  diftpsn3  4802  tppreqb  4805  xpid11  5943  cores2  6279  funcoeqres  6879  fvunsn  7199  caovmo  7670  dftpos2  8268  fvmpocurryd  8296  tfrlem16  8433  oev2  8561  domss2  9176  enp1ilem  9312  fipreima  9398  dfac5lem3  10165  fpwwe2lem12  10682  canthwelem  10690  canthp1lem2  10693  reclem3pr  11089  mulcmpblnrlem  11110  1idsr  11138  mulgt0sr  11145  mul02lem2  11438  ine0  11698  lo1eq  15604  rlimeq  15605  sumeq2ii  15729  fsumf1o  15759  sumss  15760  fsumss  15761  fsumadd  15776  fsumcom2  15810  fsum0diag2  15819  fsummulc2  15820  fsumrelem  15843  isumshft  15875  mertenslem1  15920  prodeq2ii  15947  fprodf1o  15982  prodss  15983  fprodss  15984  fprodmul  15996  fproddiv  15997  fprodcom2  16020  fprodmodd  16033  fprodefsum  16131  bitsinv1  16479  bitsinvp1  16486  4sqlem10  16985  setsnid  17245  setsnidOLD  17246  topnpropd  17481  xpsff1o  17612  homfeqbas  17739  comfffval2  17744  comfeq  17749  oppchomfpropd  17769  isssc  17864  funcpropd  17947  hofpropd  18312  eqglact  19197  symgvalstruct  19414  symgvalstructOLD  19415  lsmmod2  19694  vrgpinv  19787  frgpnabllem1  19891  frgpnabllem2  19892  gsum2dlem2  19989  dprddisj2  20059  ablfac1eulem  20092  ringpropd  20285  crngpropd  20286  mulgass3  20353  rngidpropd  20415  invrpropd  20418  isrhm2d  20487  subrngpropd  20568  subrgpropd  20608  rhmpropd  20609  lss0v  21015  lidlrsppropd  21254  ressmpladd  22047  ressmplmul  22048  ressmplvsca  22049  eqcoe1ply1eq  22303  resstopn  23194  lecldbas  23227  isref  23517  txhaus  23655  qustgplem  24129  tuslem  24275  tuslemOLD  24276  imasdsf1olem  24383  metustsym  24568  reconnlem1  24848  voliunlem1  25585  ismbf3d  25689  i1fima  25713  i1fd  25716  itgfsum  25862  dvmptc  25996  dvmptfsum  26013  dvfsumle  26060  dvfsumleOLD  26061  dvfsumlem2  26067  dvfsumlem2OLD  26068  itgsubst  26090  atantayl2  26981  chtdif  27201  ppidif  27206  fsumdvdsmul  27238  sltonold  28283  pythi  30869  hvsubeq0i  31082  hvaddcani  31084  cmcmlem  31610  pj11i  31730  hosubeq0i  31845  riesz3i  32081  pjclem1  32214  pjclem3  32216  st0  32268  chirredi  32413  mdsymi  32430  difeq  32537  unidifsnne  32554  1nei  32747  subrgchr  33241  locfinref  33840  esumpfinvallem  34075  esum2dlem  34093  carsgclctun  34323  ballotlemgun  34527  cvmliftmolem1  35286  cvmlift3lem6  35329  msubff1  35561  isfne  36340  isfne4  36341  isfne4b  36342  bj-1uplth  37008  bj-2uplth  37022  matunitlindflem1  37623  ptrest  37626  poimirlem3  37630  poimirlem4  37631  poimirlem8  37635  poimirlem15  37642  mblfinlem2  37665  voliunnfl  37671  cdlemg47  40738  ltrnco4  40741  sn-1ne2  42300  sn-0tie0  42469  sn-inelr  42497  eldioph2  42773  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  compne  44460  rnfdmpr  47293  cycl3grtri  47914