Theorem 3eqtr3d 2206

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

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

Proof of Theorem 3eqtr3d

Step	Hyp	Ref	Expression
1		3eqtr3d.1	. . 3 |- ( ph -> A = B )
2		3eqtr3d.2	. . 3 |- ( ph -> A = C )
3	1, 2	eqtr3d 2200	. 2 |- ( ph -> B = C )
4		3eqtr3d.3	. 2 |- ( ph -> B = D )
5	3, 4	eqtr3d 2200	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158

This theorem is referenced by:  mpteqb  5575  fvmptt  5576  fsnunfv  5685  f1ocnvfv1  5744  f1ocnvfv2  5745  fcof1  5750  caov12d  6019  caov13d  6021  caov411d  6023  caovimo  6031  grprinvlem  6032  grprinvd  6033  grpridd  6034  tfrlem5  6278  tfrlemiubacc  6294  tfr1onlemubacc  6310  tfrcllemubacc  6323  nndir  6454  fopwdom  6798  updjud  7043  omp1eomlem  7055  addassnqg  7319  distrnqg  7324  enq0tr  7371  distrnq0  7396  distnq0r  7400  addnqprl  7466  addnqpru  7467  appdivnq  7500  ltmprr  7579  addcmpblnr  7676  mulcmpblnrlemg  7677  ltsrprg  7684  1idsr  7705  pn0sr  7708  mulgt0sr  7715  map2psrprg  7742  axmulass  7810  ax0id  7815  recriota  7827  mul12  8023  mul4  8026  readdcan  8034  add12  8052  cnegexlem2  8070  addcan  8074  ppncan  8136  addsub4  8137  subeqxfrd  8257  subaddeqd  8263  muladd  8278  mulcanapd  8554  receuap  8562  div13ap  8585  divdivdivap  8605  divcanap5  8606  divdivap1  8615  divdivap2  8616  halfaddsub  9087  fztp  10009  fseq1p1m1  10025  flqzadd  10229  flqdiv  10252  mulp1mod1  10296  modqnegd  10310  modqsub12d  10312  q2submod  10316  modsumfzodifsn  10327  seq3m1  10399  seq3caopr  10414  iseqf1olemab  10420  iseqf1olemnanb  10421  seq3f1olemqsumk  10430  exprecap  10492  expsubap  10499  zesq  10569  nn0opthlem1d  10629  facnn2  10643  faclbnd6  10653  zfz1isolemsplit  10747  seq3coll  10751  shftval3  10765  crre  10795  resub  10808  imsub  10816  cjsub  10830  bdtrilem  11176  bdtri  11177  climshft2  11243  nnf1o  11313  fsumf1o  11327  isumss  11328  fisumss  11329  fsumadd  11343  isumclim3  11360  fsummulc2  11385  fsumsub  11389  telfsumo  11403  telfsumo2  11404  hashiun  11415  bcxmas  11426  isumshft  11427  trireciplem  11437  geoserap  11444  geo2sum2  11452  fprodf1o  11525  prodssdc  11526  fprodssdc  11527  fprodmul  11528  fprodm1  11535  sinsub  11677  cossub  11678  p1modz1  11730  gcdaddm  11913  modgcd  11920  bezoutlemnewy  11925  absmulgcd  11946  gcdmultiplez  11950  eucalg  11987  lcmgcd  12006  lcmid  12008  numdensq  12130  dfphi2  12148  phiprm  12151  fermltl  12162  prmdiveq  12164  hashgcdlem  12166  odzdvds  12173  powm2modprm  12180  modprm0  12182  coprimeprodsq  12185  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem16  12207  pcaddlem  12266  sumhashdc  12273  fldivp1  12274  pcfac  12276  pockthlem  12282  ennnfonelem1  12336  ennnfonelemex  12343  topnpropgd  12565  restin  12776  blpnfctr  13039  xmssym  13069  limcimolemlt  13233  dvmulxxbr  13266  dvrecap  13277  dvmptaddx  13281  dvmptmulx  13282  dvmptnegcn  13284  dvmptsubcn  13285  dvmptcjx  13286  dveflem  13287  sin0pilem1  13302  ptolemy  13345  tangtx  13359  rpcxpneg  13428  rpcxpsub  13429  cxprec  13431  rpcxproot  13434  cxpcom  13457  rpabscxpbnd  13459  lgsvalmod  13520  lgsneg  13525  lgsdilem  13528  lgsne0  13539  lgssq  13541  lgssq2  13542  peano4nninf  13846  nninfalllem1  13848  nninfall  13849  nninfsellemqall  13855  qdencn  13866