Theorem 3eqtr3d 2181

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

Syntax hints:   -> wi 4   = wceq 1332

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

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

This theorem is referenced by:  mpteqb  5519  fvmptt  5520  fsnunfv  5629  f1ocnvfv1  5686  f1ocnvfv2  5687  fcof1  5692  caov12d  5960  caov13d  5962  caov411d  5964  caovimo  5972  grprinvlem  5973  grprinvd  5974  grpridd  5975  tfrlem5  6219  tfrlemiubacc  6235  tfr1onlemubacc  6251  tfrcllemubacc  6264  nndir  6394  fopwdom  6738  updjud  6975  omp1eomlem  6987  addassnqg  7214  distrnqg  7219  enq0tr  7266  distrnq0  7291  distnq0r  7295  addnqprl  7361  addnqpru  7362  appdivnq  7395  ltmprr  7474  addcmpblnr  7571  mulcmpblnrlemg  7572  ltsrprg  7579  1idsr  7600  pn0sr  7603  mulgt0sr  7610  map2psrprg  7637  axmulass  7705  ax0id  7710  recriota  7722  mul12  7915  mul4  7918  readdcan  7926  add12  7944  cnegexlem2  7962  addcan  7966  ppncan  8028  addsub4  8029  subeqxfrd  8149  subaddeqd  8155  muladd  8170  mulcanapd  8446  receuap  8454  div13ap  8477  divdivdivap  8497  divcanap5  8498  divdivap1  8507  divdivap2  8508  halfaddsub  8978  fztp  9889  fseq1p1m1  9905  flqzadd  10102  flqdiv  10125  mulp1mod1  10169  modqnegd  10183  modqsub12d  10185  q2submod  10189  modsumfzodifsn  10200  seq3m1  10272  seq3caopr  10287  iseqf1olemab  10293  iseqf1olemnanb  10294  seq3f1olemqsumk  10303  exprecap  10365  expsubap  10372  zesq  10441  nn0opthlem1d  10498  facnn2  10512  faclbnd6  10522  zfz1isolemsplit  10613  seq3coll  10617  shftval3  10631  crre  10661  resub  10674  imsub  10682  cjsub  10696  bdtrilem  11042  bdtri  11043  climshft2  11107  nnf1o  11177  fsumf1o  11191  isumss  11192  fisumss  11193  fsumadd  11207  isumclim3  11224  fsummulc2  11249  fsumsub  11253  telfsumo  11267  telfsumo2  11268  hashiun  11279  bcxmas  11290  isumshft  11291  trireciplem  11301  geoserap  11308  geo2sum2  11316  sinsub  11483  cossub  11484  gcdaddm  11708  modgcd  11715  bezoutlemnewy  11720  absmulgcd  11741  gcdmultiplez  11745  eucalg  11776  lcmgcd  11795  lcmid  11797  numdensq  11916  dfphi2  11932  phiprm  11935  hashgcdlem  11939  ennnfonelem1  11956  ennnfonelemex  11963  topnpropgd  12173  restin  12384  blpnfctr  12647  xmssym  12677  limcimolemlt  12841  dvmulxxbr  12874  dvrecap  12885  dvmptaddx  12889  dvmptmulx  12890  dvmptnegcn  12892  dvmptsubcn  12893  dvmptcjx  12894  dveflem  12895  sin0pilem1  12910  ptolemy  12953  tangtx  12967  rpcxpneg  13036  rpcxpsub  13037  cxprec  13039  rpcxproot  13042  cxpcom  13065  rpabscxpbnd  13067  peano4nninf  13375  nninfalllem1  13378  nninfall  13379  nninfsellemqall  13386  qdencn  13397