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 1541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  csbnest1g  4429  disjdif2  4479  diftpsn3  4805  tppreqb  4808  xpid11  5931  cores2  6258  funcoeqres  6864  fvunsn  7179  caovmo  7646  dftpos2  8230  fvmpocurryd  8258  tfrlem16  8395  oev2  8525  domss2  9138  enp1ilem  9280  fipreima  9360  dfac5lem3  10122  fpwwe2lem12  10639  canthwelem  10647  canthp1lem2  10650  reclem3pr  11046  mulcmpblnrlem  11067  1idsr  11095  mulgt0sr  11102  mul02lem2  11395  ine0  11653  lo1eq  15516  rlimeq  15517  sumeq2ii  15643  fsumf1o  15673  sumss  15674  fsumss  15675  fsumadd  15690  fsumcom2  15724  fsum0diag2  15733  fsummulc2  15734  fsumrelem  15757  isumshft  15789  mertenslem1  15834  prodeq2ii  15861  fprodf1o  15894  prodss  15895  fprodss  15896  fprodmul  15908  fproddiv  15909  fprodcom2  15932  fprodmodd  15945  fprodefsum  16042  bitsinv1  16387  bitsinvp1  16394  4sqlem10  16884  setsnid  17146  setsnidOLD  17147  topnpropd  17386  xpsff1o  17517  homfeqbas  17644  comfffval2  17649  comfeq  17654  oppchomfpropd  17676  isssc  17771  funcpropd  17855  hofpropd  18224  eqglact  19095  symgvalstruct  19305  symgvalstructOLD  19306  lsmmod2  19585  vrgpinv  19678  frgpnabllem1  19782  frgpnabllem2  19783  gsum2dlem2  19880  dprddisj2  19950  ablfac1eulem  19983  ringpropd  20176  crngpropd  20177  mulgass3  20244  rngidpropd  20306  invrpropd  20309  isrhm2d  20378  subrngpropd  20456  subrgpropd  20498  rhmpropd  20499  lss0v  20771  lidlrsppropd  21004  ressmpladd  21803  ressmplmul  21804  ressmplvsca  21805  eqcoe1ply1eq  22041  resstopn  22910  lecldbas  22943  isref  23233  txhaus  23371  qustgplem  23845  tuslem  23991  tuslemOLD  23992  imasdsf1olem  24099  metustsym  24284  reconnlem1  24562  voliunlem1  25291  ismbf3d  25395  i1fima  25419  i1fd  25422  itgfsum  25568  dvmptc  25699  dvmptfsum  25716  dvfsumle  25762  dvfsumlem2  25768  itgsubst  25790  atantayl2  26667  chtdif  26886  ppidif  26891  sltonold  27914  pythi  30358  hvsubeq0i  30571  hvaddcani  30573  cmcmlem  31099  pj11i  31219  hosubeq0i  31334  riesz3i  31570  pjclem1  31703  pjclem3  31705  st0  31757  chirredi  31902  mdsymi  31919  difeq  32011  unidifsnne  32028  1nei  32216  subrgchr  32644  locfinref  33107  esumpfinvallem  33358  esum2dlem  33376  carsgclctun  33606  ballotlemgun  33809  cvmliftmolem1  34558  cvmlift3lem6  34601  msubff1  34833  gg-dvfsumle  35468  gg-dvfsumlem2  35469  isfne  35527  isfne4  35528  isfne4b  35529  bj-1uplth  36191  bj-2uplth  36205  matunitlindflem1  36787  ptrest  36790  poimirlem3  36794  poimirlem4  36795  poimirlem8  36799  poimirlem15  36806  mblfinlem2  36829  voliunnfl  36835  cdlemg47  39910  ltrnco4  39913  sn-1ne2  41481  sn-0tie0  41614  sn-inelr  41640  eldioph2  41802  binomcxplemdvbinom  43414  binomcxplemnotnn0  43417  compne  43502  rnfdmpr  46288