Theorem 3eqtr3g 2803

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  csbnest1g  4455  disjdif2  4503  diftpsn3  4827  tppreqb  4830  xpid11  5957  cores2  6290  funcoeqres  6893  fvunsn  7213  caovmo  7687  dftpos2  8284  fvmpocurryd  8312  tfrlem16  8449  oev2  8579  domss2  9202  enp1ilem  9340  fipreima  9428  dfac5lem3  10194  fpwwe2lem12  10711  canthwelem  10719  canthp1lem2  10722  reclem3pr  11118  mulcmpblnrlem  11139  1idsr  11167  mulgt0sr  11174  mul02lem2  11467  ine0  11725  lo1eq  15614  rlimeq  15615  sumeq2ii  15741  fsumf1o  15771  sumss  15772  fsumss  15773  fsumadd  15788  fsumcom2  15822  fsum0diag2  15831  fsummulc2  15832  fsumrelem  15855  isumshft  15887  mertenslem1  15932  prodeq2ii  15959  fprodf1o  15994  prodss  15995  fprodss  15996  fprodmul  16008  fproddiv  16009  fprodcom2  16032  fprodmodd  16045  fprodefsum  16143  bitsinv1  16488  bitsinvp1  16495  4sqlem10  16994  setsnid  17256  setsnidOLD  17257  topnpropd  17496  xpsff1o  17627  homfeqbas  17754  comfffval2  17759  comfeq  17764  oppchomfpropd  17786  isssc  17881  funcpropd  17967  hofpropd  18337  eqglact  19219  symgvalstruct  19438  symgvalstructOLD  19439  lsmmod2  19718  vrgpinv  19811  frgpnabllem1  19915  frgpnabllem2  19916  gsum2dlem2  20013  dprddisj2  20083  ablfac1eulem  20116  ringpropd  20311  crngpropd  20312  mulgass3  20379  rngidpropd  20441  invrpropd  20444  isrhm2d  20513  subrngpropd  20594  subrgpropd  20636  rhmpropd  20637  lss0v  21038  lidlrsppropd  21277  ressmpladd  22070  ressmplmul  22071  ressmplvsca  22072  eqcoe1ply1eq  22324  resstopn  23215  lecldbas  23248  isref  23538  txhaus  23676  qustgplem  24150  tuslem  24296  tuslemOLD  24297  imasdsf1olem  24404  metustsym  24589  reconnlem1  24867  voliunlem1  25604  ismbf3d  25708  i1fima  25732  i1fd  25735  itgfsum  25882  dvmptc  26016  dvmptfsum  26033  dvfsumle  26080  dvfsumleOLD  26081  dvfsumlem2  26087  dvfsumlem2OLD  26088  itgsubst  26110  atantayl2  26999  chtdif  27219  ppidif  27224  fsumdvdsmul  27256  sltonold  28301  pythi  30882  hvsubeq0i  31095  hvaddcani  31097  cmcmlem  31623  pj11i  31743  hosubeq0i  31858  riesz3i  32094  pjclem1  32227  pjclem3  32229  st0  32281  chirredi  32426  mdsymi  32443  difeq  32548  unidifsnne  32564  1nei  32750  subrgchr  33217  locfinref  33787  esumpfinvallem  34038  esum2dlem  34056  carsgclctun  34286  ballotlemgun  34489  cvmliftmolem1  35249  cvmlift3lem6  35292  msubff1  35524  isfne  36305  isfne4  36306  isfne4b  36307  bj-1uplth  36973  bj-2uplth  36987  matunitlindflem1  37576  ptrest  37579  poimirlem3  37583  poimirlem4  37584  poimirlem8  37588  poimirlem15  37595  mblfinlem2  37618  voliunnfl  37624  cdlemg47  40693  ltrnco4  40696  sn-1ne2  42254  sn-0tie0  42415  sn-inelr  42443  eldioph2  42718  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  compne  44410  rnfdmpr  47196