Theorem 3eqtr3g 2884

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	syl5eqr 2875	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	syl6eq 2877	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818

This theorem is referenced by:  csbnest1g  4227  disjdif2  4272  diftpsn3  4553  tppreqb  4556  xpid11  5583  cores2  5893  funcoeqres  6412  fvunsn  6702  caovmo  7136  dftpos2  7639  fvmpt2curryd  7667  tfrlem16  7760  oev2  7875  domss2  8394  enp1ilem  8469  fipreima  8547  dfac5lem3  9268  fpwwe2lem13  9786  canthwelem  9794  canthp1lem2  9797  reclem3pr  10193  mulcmpblnrlem  10214  1idsr  10242  mulgt0sr  10249  mul02lem2  10539  ine0  10796  lo1eq  14683  rlimeq  14684  sumeq2ii  14807  fsumf1o  14838  sumss  14839  fsumss  14840  fsumadd  14854  fsumcom2  14887  fsum0diag2  14896  fsummulc2  14897  fsumrelem  14920  isumshft  14952  mertenslem1  14996  prodeq2ii  15023  fprodf1o  15056  prodss  15057  fprodss  15058  fprodmul  15070  fproddiv  15071  fprodcom2  15094  fprodmodd  15107  fprodefsum  15204  bitsinv1  15544  bitsinvp1  15551  4sqlem10  16029  setsnid  16285  topnpropd  16457  xpsff1o  16588  homfeqbas  16715  comfffval2  16720  comfeq  16725  oppchomfpropd  16745  isssc  16839  funcpropd  16919  hofpropd  17267  eqglact  18003  lsmmod2  18447  vrgpinv  18542  frgpnabllem1  18636  frgpnabllem2  18637  gsum2dlem2  18730  dprddisj2  18799  ablfac1eulem  18832  ringpropd  18943  crngpropd  18944  mulgass3  18998  rngidpropd  19056  invrpropd  19059  isrhm2d  19091  subrgpropd  19177  rhmpropd  19178  lss0v  19382  lidlrsppropd  19598  ressmpladd  19825  ressmplmul  19826  ressmplvsca  19827  eqcoe1ply1eq  20034  resstopn  21368  lecldbas  21401  isref  21690  txhaus  21828  qustgplem  22301  tuslem  22448  imasdsf1olem  22555  metustsym  22737  reconnlem1  23006  voliunlem1  23723  ismbf3d  23827  i1fima  23851  i1fd  23854  itgfsum  23999  dvmptc  24127  dvmptfsum  24144  dvfsumle  24190  dvfsumlem2  24196  itgsubst  24218  atantayl2  25085  chtdif  25304  ppidif  25309  pythi  28256  hvsubeq0i  28471  hvaddcani  28473  cmcmlem  29001  pj11i  29121  hosubeq0i  29236  riesz3i  29472  pjclem1  29605  pjclem3  29607  st0  29659  chirredi  29804  mdsymi  29821  difeq  29899  subrgchr  30335  locfinref  30449  esumpfinvallem  30677  esum2dlem  30695  carsgclctun  30924  ballotlemgun  31128  cvmliftmolem1  31805  cvmlift3lem6  31848  msubff1  31995  isfne  32867  isfne4  32868  isfne4b  32869  bj-1uplth  33512  bj-2uplth  33526  matunitlindflem1  33944  ptrest  33947  poimirlem3  33951  poimirlem4  33952  poimirlem8  33956  poimirlem15  33963  mblfinlem2  33986  voliunnfl  33992  cdlemg47  36806  ltrnco4  36809  eldioph2  38164  binomcxplemdvbinom  39387  binomcxplemnotnn0  39390  compne  39477  rnfdmpr  42178