Theorem 3eqtr3d 2218

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

Syntax hints:   -> wi 4   = wceq 1353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170

This theorem is referenced by:  mpteqb  5603  fvmptt  5604  fsnunfv  5714  f1ocnvfv1  5773  f1ocnvfv2  5774  fcof1  5779  caov12d  6051  caov13d  6053  caov411d  6055  caovimo  6063  tfrlem5  6310  tfrlemiubacc  6326  tfr1onlemubacc  6342  tfrcllemubacc  6355  nndir  6486  fopwdom  6831  updjud  7076  omp1eomlem  7088  addassnqg  7376  distrnqg  7381  enq0tr  7428  distrnq0  7453  distnq0r  7457  addnqprl  7523  addnqpru  7524  appdivnq  7557  ltmprr  7636  addcmpblnr  7733  mulcmpblnrlemg  7734  ltsrprg  7741  1idsr  7762  pn0sr  7765  mulgt0sr  7772  map2psrprg  7799  axmulass  7867  ax0id  7872  recriota  7884  mul12  8080  mul4  8083  readdcan  8091  add12  8109  cnegexlem2  8127  addcan  8131  ppncan  8193  addsub4  8194  subeqxfrd  8314  subaddeqd  8320  muladd  8335  mulcanapd  8612  receuap  8620  div13ap  8644  divdivdivap  8664  divcanap5  8665  divdivap1  8674  divdivap2  8675  halfaddsub  9147  fztp  10071  fseq1p1m1  10087  flqzadd  10291  flqdiv  10314  mulp1mod1  10358  modqnegd  10372  modqsub12d  10374  q2submod  10378  modsumfzodifsn  10389  seq3m1  10461  seq3caopr  10476  iseqf1olemab  10482  iseqf1olemnanb  10483  seq3f1olemqsumk  10492  exprecap  10554  expsubap  10561  zesq  10631  nn0opthlem1d  10691  facnn2  10705  faclbnd6  10715  zfz1isolemsplit  10809  seq3coll  10813  shftval3  10827  crre  10857  resub  10870  imsub  10878  cjsub  10892  bdtrilem  11238  bdtri  11239  climshft2  11305  nnf1o  11375  fsumf1o  11389  isumss  11390  fisumss  11391  fsumadd  11405  isumclim3  11422  fsummulc2  11447  fsumsub  11451  telfsumo  11465  telfsumo2  11466  hashiun  11477  bcxmas  11488  isumshft  11489  trireciplem  11499  geoserap  11506  geo2sum2  11514  fprodf1o  11587  prodssdc  11588  fprodssdc  11589  fprodmul  11590  fprodm1  11597  sinsub  11739  cossub  11740  p1modz1  11792  gcdaddm  11975  modgcd  11982  bezoutlemnewy  11987  absmulgcd  12008  gcdmultiplez  12012  eucalg  12049  lcmgcd  12068  lcmid  12070  numdensq  12192  dfphi2  12210  phiprm  12213  fermltl  12224  prmdiveq  12226  hashgcdlem  12228  odzdvds  12235  powm2modprm  12242  modprm0  12244  coprimeprodsq  12247  pythagtriplem6  12260  pythagtriplem7  12261  pythagtriplem12  12265  pythagtriplem14  12267  pythagtriplem16  12269  pcaddlem  12328  sumhashdc  12335  fldivp1  12336  pcfac  12338  pockthlem  12344  ennnfonelem1  12398  ennnfonelemex  12405  topnpropgd  12688  grprinvlem  12734  grprinvd  12735  grpridd  12736  mnd12g  12759  grprcan  12838  grplcan  12860  grpasscan1  12861  grpinv11  12867  grpinvnz  12869  grplmulf1o  12872  grpinvpropdg  12873  grpinvadd  12876  grpsubsub4  12891  dfgrp3m  12897  mhmid  12907  mhmmnd  12908  mulgz  12938  mulgdirlem  12941  mulgdir  12942  mulgass  12947  mulgsubdir  12950  mulgpropdg  12952  ringcom  13114  crngpropd  13118  isringd  13120  ringlz  13122  ringrz  13123  ring1eq0  13125  ringmneg1  13130  mulgass3  13153  unitgrp  13184  rngidpropdg  13214  invrpropdg  13217  restin  13458  blpnfctr  13721  xmssym  13751  limcimolemlt  13915  dvmulxxbr  13948  dvrecap  13959  dvmptaddx  13963  dvmptmulx  13964  dvmptnegcn  13966  dvmptsubcn  13967  dvmptcjx  13968  dveflem  13969  sin0pilem1  13984  ptolemy  14027  tangtx  14041  rpcxpneg  14110  rpcxpsub  14111  cxprec  14113  rpcxproot  14116  cxpcom  14139  rpabscxpbnd  14141  lgsvalmod  14202  lgsneg  14207  lgsdilem  14210  lgsne0  14221  lgssq  14223  lgssq2  14224  peano4nninf  14526  nninfalllem1  14528  nninfall  14529  nninfsellemqall  14535  qdencn  14546