Theorem 3eqtr3g 2788

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 2779	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtrdi 2781	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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  csbnest1g  4398  disjdif2  4446  diftpsn3  4769  tppreqb  4772  xpid11  5899  cores2  6235  funcoeqres  6834  fvunsn  7156  caovmo  7629  dftpos2  8225  fvmpocurryd  8253  tfrlem16  8364  oev2  8490  domss2  9106  enp1ilem  9230  fipreima  9316  dfac5lem3  10085  fpwwe2lem12  10602  canthwelem  10610  canthp1lem2  10613  reclem3pr  11009  mulcmpblnrlem  11030  1idsr  11058  mulgt0sr  11065  mul02lem2  11358  ine0  11620  lo1eq  15541  rlimeq  15542  sumeq2ii  15666  fsumf1o  15696  sumss  15697  fsumss  15698  fsumadd  15713  fsumcom2  15747  fsum0diag2  15756  fsummulc2  15757  fsumrelem  15780  isumshft  15812  mertenslem1  15857  prodeq2ii  15884  fprodf1o  15919  prodss  15920  fprodss  15921  fprodmul  15933  fproddiv  15934  fprodcom2  15957  fprodmodd  15970  fprodefsum  16068  bitsinv1  16419  bitsinvp1  16426  4sqlem10  16925  setsnid  17185  topnpropd  17406  xpsff1o  17537  homfeqbas  17664  comfffval2  17669  comfeq  17674  oppchomfpropd  17694  isssc  17789  funcpropd  17871  hofpropd  18235  eqglact  19118  symgvalstruct  19334  lsmmod2  19613  vrgpinv  19706  frgpnabllem1  19810  frgpnabllem2  19811  gsum2dlem2  19908  dprddisj2  19978  ablfac1eulem  20011  ringpropd  20204  crngpropd  20205  mulgass3  20269  rngidpropd  20331  invrpropd  20334  isrhm2d  20403  subrngpropd  20484  subrgpropd  20524  rhmpropd  20525  lss0v  20930  lidlrsppropd  21161  ressmpladd  21943  ressmplmul  21944  ressmplvsca  21945  eqcoe1ply1eq  22193  resstopn  23080  lecldbas  23113  isref  23403  txhaus  23541  qustgplem  24015  tuslem  24161  imasdsf1olem  24268  metustsym  24450  reconnlem1  24722  voliunlem1  25458  ismbf3d  25562  i1fima  25586  i1fd  25589  itgfsum  25735  dvmptc  25869  dvmptfsum  25886  dvfsumle  25933  dvfsumleOLD  25934  dvfsumlem2  25940  dvfsumlem2OLD  25941  itgsubst  25963  atantayl2  26855  chtdif  27075  ppidif  27080  fsumdvdsmul  27112  onsleft  28168  onscutlt  28172  pythi  30786  hvsubeq0i  30999  hvaddcani  31001  cmcmlem  31527  pj11i  31647  hosubeq0i  31762  riesz3i  31998  pjclem1  32131  pjclem3  32133  st0  32185  chirredi  32330  mdsymi  32347  difeq  32454  unidifsnne  32472  1nei  32667  subrgchr  33195  ressply1evls1  33541  locfinref  33838  esumpfinvallem  34071  esum2dlem  34089  carsgclctun  34319  ballotlemgun  34523  cvmliftmolem1  35275  cvmlift3lem6  35318  msubff1  35550  isfne  36334  isfne4  36335  isfne4b  36336  bj-1uplth  37002  bj-2uplth  37016  matunitlindflem1  37617  ptrest  37620  poimirlem3  37624  poimirlem4  37625  poimirlem8  37629  poimirlem15  37636  mblfinlem2  37659  voliunnfl  37665  cdlemg47  40737  ltrnco4  40740  sn-1ne2  42260  sn-00idlem3  42395  sn-0tie0  42446  sn-inelr  42482  eldioph2  42757  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  compne  44437  rnfdmpr  47286  cycl3grtri  47950