Theorem 3eqtr3d 2211

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 2205	. 2 |- ( ph -> B = C )
4		3eqtr3d.3	. 2 |- ( ph -> B = D )
5	3, 4	eqtr3d 2205	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  mpteqb  5586  fvmptt  5587  fsnunfv  5697  f1ocnvfv1  5756  f1ocnvfv2  5757  fcof1  5762  caov12d  6034  caov13d  6036  caov411d  6038  caovimo  6046  tfrlem5  6293  tfrlemiubacc  6309  tfr1onlemubacc  6325  tfrcllemubacc  6338  nndir  6469  fopwdom  6814  updjud  7059  omp1eomlem  7071  addassnqg  7344  distrnqg  7349  enq0tr  7396  distrnq0  7421  distnq0r  7425  addnqprl  7491  addnqpru  7492  appdivnq  7525  ltmprr  7604  addcmpblnr  7701  mulcmpblnrlemg  7702  ltsrprg  7709  1idsr  7730  pn0sr  7733  mulgt0sr  7740  map2psrprg  7767  axmulass  7835  ax0id  7840  recriota  7852  mul12  8048  mul4  8051  readdcan  8059  add12  8077  cnegexlem2  8095  addcan  8099  ppncan  8161  addsub4  8162  subeqxfrd  8282  subaddeqd  8288  muladd  8303  mulcanapd  8579  receuap  8587  div13ap  8610  divdivdivap  8630  divcanap5  8631  divdivap1  8640  divdivap2  8641  halfaddsub  9112  fztp  10034  fseq1p1m1  10050  flqzadd  10254  flqdiv  10277  mulp1mod1  10321  modqnegd  10335  modqsub12d  10337  q2submod  10341  modsumfzodifsn  10352  seq3m1  10424  seq3caopr  10439  iseqf1olemab  10445  iseqf1olemnanb  10446  seq3f1olemqsumk  10455  exprecap  10517  expsubap  10524  zesq  10594  nn0opthlem1d  10654  facnn2  10668  faclbnd6  10678  zfz1isolemsplit  10773  seq3coll  10777  shftval3  10791  crre  10821  resub  10834  imsub  10842  cjsub  10856  bdtrilem  11202  bdtri  11203  climshft2  11269  nnf1o  11339  fsumf1o  11353  isumss  11354  fisumss  11355  fsumadd  11369  isumclim3  11386  fsummulc2  11411  fsumsub  11415  telfsumo  11429  telfsumo2  11430  hashiun  11441  bcxmas  11452  isumshft  11453  trireciplem  11463  geoserap  11470  geo2sum2  11478  fprodf1o  11551  prodssdc  11552  fprodssdc  11553  fprodmul  11554  fprodm1  11561  sinsub  11703  cossub  11704  p1modz1  11756  gcdaddm  11939  modgcd  11946  bezoutlemnewy  11951  absmulgcd  11972  gcdmultiplez  11976  eucalg  12013  lcmgcd  12032  lcmid  12034  numdensq  12156  dfphi2  12174  phiprm  12177  fermltl  12188  prmdiveq  12190  hashgcdlem  12192  odzdvds  12199  powm2modprm  12206  modprm0  12208  coprimeprodsq  12211  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem16  12233  pcaddlem  12292  sumhashdc  12299  fldivp1  12300  pcfac  12302  pockthlem  12308  ennnfonelem1  12362  ennnfonelemex  12369  topnpropgd  12593  grprinvlem  12639  grprinvd  12640  grpridd  12641  mnd12g  12664  grprcan  12740  grplcan  12761  grpasscan1  12762  grpinv11  12768  grpinvnz  12770  restin  12970  blpnfctr  13233  xmssym  13263  limcimolemlt  13427  dvmulxxbr  13460  dvrecap  13471  dvmptaddx  13475  dvmptmulx  13476  dvmptnegcn  13478  dvmptsubcn  13479  dvmptcjx  13480  dveflem  13481  sin0pilem1  13496  ptolemy  13539  tangtx  13553  rpcxpneg  13622  rpcxpsub  13623  cxprec  13625  rpcxproot  13628  cxpcom  13651  rpabscxpbnd  13653  lgsvalmod  13714  lgsneg  13719  lgsdilem  13722  lgsne0  13733  lgssq  13735  lgssq2  13736  peano4nninf  14039  nninfalllem1  14041  nninfall  14042  nninfsellemqall  14048  qdencn  14059