Theorem 3eqtr3g 2679

Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)

Hypotheses

Ref	Expression
3eqtr3g.1	|- ( ph -> A = B )
3eqtr3g.2	|- A = C
3eqtr3g.3	|- B = D

Assertion

Ref	Expression
3eqtr3g	|- ( ph -> C = D )

Proof of Theorem 3eqtr3g

Step	Hyp	Ref	Expression
1		3eqtr3g.2	. . 3 |- A = C
2		3eqtr3g.1	. . 3 |- ( ph -> A = B )
3	1, 2	syl5eqr 2670	. 2 |- ( ph -> C = B )
4		3eqtr3g.3	. 2 |- B = D
5	3, 4	syl6eq 2672	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  csbnest1g  4001  disjdif2  4047  diftpsn3  4332  tppreqb  4336  xpid11  5347  cores2  5648  funcoeqres  6167  fvunsn  6445  caovmo  6871  dftpos2  7369  fvmpt2curryd  7397  tfrlem16  7489  oev2  7603  domss2  8119  enp1ilem  8194  fipreima  8272  dfac5lem3  8948  fpwwe2lem13  9464  canthwelem  9472  canthp1lem2  9475  reclem3pr  9871  mulcmpblnrlem  9891  1idsr  9919  mulgt0sr  9926  mul02lem2  10213  ine0  10465  s1nzOLD  13387  lo1eq  14299  rlimeq  14300  sumeq2ii  14423  fsumf1o  14454  sumss  14455  fsumss  14456  fsumadd  14470  fsumcom2  14505  fsumcom2OLD  14506  fsum0diag2  14515  fsummulc2  14516  fsumrelem  14539  isumshft  14571  mertenslem1  14616  prodeq2ii  14643  fprodf1o  14676  prodss  14677  fprodss  14678  fprodmul  14690  fproddiv  14691  fprodcom2  14714  fprodcom2OLD  14715  fprodmodd  14728  fprodefsum  14825  bitsinv1  15164  bitsinvp1  15171  4sqlem10  15651  setsnid  15915  topnpropd  16097  xpsff1o  16228  homfeqbas  16356  comfffval2  16361  comfeq  16366  oppchomfpropd  16386  isssc  16480  funcpropd  16560  hofpropd  16907  eqglact  17645  lsmmod2  18089  vrgpinv  18182  frgpnabllem1  18276  frgpnabllem2  18277  gsum2dlem2  18370  dprddisj2  18438  ablfac1eulem  18471  ringpropd  18582  crngpropd  18583  mulgass3  18637  rngidpropd  18695  invrpropd  18698  isrhm2d  18728  subrgpropd  18814  rhmpropd  18815  lss0v  19016  lidlrsppropd  19230  ressmpladd  19457  ressmplmul  19458  ressmplvsca  19459  eqcoe1ply1eq  19667  resstopn  20990  lecldbas  21023  isref  21312  txhaus  21450  qustgplem  21924  tuslem  22071  imasdsf1olem  22178  metustsym  22360  reconnlem1  22629  voliunlem1  23318  ismbf3d  23421  i1fima  23445  i1fd  23448  itgfsum  23593  dvmptc  23721  dvmptfsum  23738  dvfsumle  23784  dvfsumlem2  23790  itgsubst  23812  atantayl2  24665  chtdif  24884  ppidif  24889  pythi  27705  hvsubeq0i  27920  hvaddcani  27922  cmcmlem  28450  pj11i  28570  hosubeq0i  28685  riesz3i  28921  pjclem1  29054  pjclem3  29056  st0  29108  chirredi  29253  mdsymi  29270  difeq  29355  subrgchr  29794  locfinref  29908  esumpfinvallem  30136  esum2dlem  30154  carsgclctun  30383  ballotlemgun  30586  cvmliftmolem1  31263  cvmlift3lem6  31306  msubff1  31453  isfne  32334  isfne4  32335  isfne4b  32336  bj-1uplth  32995  bj-2uplth  33009  matunitlindflem1  33405  ptrest  33408  poimirlem3  33412  poimirlem4  33413  poimirlem8  33417  poimirlem15  33424  mblfinlem2  33447  voliunnfl  33453  cdlemg47  36024  ltrnco4  36027  eldioph2  37325  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  compne  38643  rnfdmpr  41300