Theorem 3eqtr3d 2248

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

Syntax hints:   -> wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  mpteqb  5693  fvmptt  5694  fsnunfv  5808  f1ocnvfv1  5869  f1ocnvfv2  5870  fcof1  5875  caov12d  6151  caov13d  6153  caov411d  6155  caovimo  6163  tfrlem5  6423  tfrlemiubacc  6439  tfr1onlemubacc  6455  tfrcllemubacc  6468  nndir  6599  en2  6936  fopwdom  6958  updjud  7210  omp1eomlem  7222  addassnqg  7530  distrnqg  7535  enq0tr  7582  distrnq0  7607  distnq0r  7611  addnqprl  7677  addnqpru  7678  appdivnq  7711  ltmprr  7790  addcmpblnr  7887  mulcmpblnrlemg  7888  ltsrprg  7895  1idsr  7916  pn0sr  7919  mulgt0sr  7926  map2psrprg  7953  axmulass  8021  ax0id  8026  recriota  8038  mul12  8236  mul4  8239  readdcan  8247  add12  8265  cnegexlem2  8283  addcan  8287  ppncan  8349  addsub4  8350  subeqxfrd  8470  subaddeqd  8476  muladd  8491  mulcanapd  8769  receuap  8777  div13ap  8801  divdivdivap  8821  divcanap5  8822  divdivap1  8831  divdivap2  8832  halfaddsub  9306  fztp  10235  fseq1p1m1  10251  flqzadd  10478  flqdiv  10503  mulp1mod1  10547  modqnegd  10561  modqsub12d  10563  q2submod  10567  modsumfzodifsn  10578  seq3m1  10655  seq3caopr  10677  seqcaoprg  10678  iseqf1olemab  10684  iseqf1olemnanb  10685  seq3f1olemqsumk  10694  seqf1og  10703  exprecap  10762  expsubap  10769  zesq  10840  nn0opthlem1d  10902  facnn2  10916  faclbnd6  10926  zfz1isolemsplit  11020  seq3coll  11024  ccatopth  11207  shftval3  11253  crre  11283  resub  11296  imsub  11304  cjsub  11318  bdtrilem  11665  bdtri  11666  climshft2  11732  nnf1o  11802  fsumf1o  11816  isumss  11817  fisumss  11818  fsumadd  11832  isumclim3  11849  fsummulc2  11874  fsumsub  11878  telfsumo  11892  telfsumo2  11893  hashiun  11904  bcxmas  11915  isumshft  11916  trireciplem  11926  geoserap  11933  geo2sum2  11941  fprodf1o  12014  prodssdc  12015  fprodssdc  12016  fprodmul  12017  fprodm1  12024  sinsub  12166  cossub  12167  p1modz1  12220  bitsinv1lem  12387  bitsinv1  12388  gcdaddm  12420  modgcd  12427  bezoutlemnewy  12432  absmulgcd  12453  gcdmultiplez  12457  eucalg  12496  lcmgcd  12515  lcmid  12517  numdensq  12639  dfphi2  12657  phiprm  12660  fermltl  12671  prmdiveq  12673  hashgcdlem  12675  odzdvds  12683  powm2modprm  12690  modprm0  12692  coprimeprodsq  12695  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem16  12717  pcaddlem  12777  sumhashdc  12785  fldivp1  12786  pcfac  12788  pockthlem  12794  4sqlem12  12840  4sqlem15  12843  ennnfonelem1  12893  ennnfonelemex  12900  topnpropgd  13200  qusaddvallemg  13280  grpinvalem  13332  grpinva  13333  grprida  13334  mnd12g  13375  resmhm  13434  grprcan  13484  grplcan  13509  grpasscan1  13510  grpinv11  13516  grpinvnz  13518  grplmulf1o  13521  grpinvpropdg  13522  grpinvadd  13525  grpsubsub4  13540  dfgrp3m  13546  imasgrp2  13561  mhmid  13566  mhmmnd  13567  mulgz  13601  mulgdirlem  13604  mulgdir  13605  mulgass  13610  mulgsubdir  13613  mulgpropdg  13615  isnsg3  13658  nmzsubg  13661  ssnmz  13662  eqger  13675  eqglact  13676  ghminv  13701  conjnmz  13730  ghmcmn  13778  gsumfzconst  13792  gsumfzmhm2  13795  rnglz  13822  rngrz  13823  isrngd  13830  ringcom  13908  crngpropd  13916  isringd  13918  ringlz  13920  ringrz  13921  ring1eq0  13925  ringmneg1  13930  mulgass3  13962  unitgrp  13993  rngidpropdg  14023  invrpropdg  14026  isrhm2d  14042  rhmunitinv  14055  subrngpropd  14093  subrginv  14114  subrgunit  14116  subrgpropd  14130  rhmpropd  14131  unitrrg  14144  lmodvs0  14199  lmodvneg1  14207  lmodcom  14210  lmodsubdi  14221  lss0v  14307  lidlrsppropdg  14372  mulgrhm2  14487  znidomb  14535  restin  14763  blpnfctr  15026  xmssym  15056  limcimolemlt  15251  dvmulxxbr  15289  dvrecap  15300  dvmptaddx  15306  dvmptmulx  15307  dvmptnegcn  15309  dvmptsubcn  15310  dvmptcjx  15311  dveflem  15313  plymullem1  15335  dvply1  15352  sin0pilem1  15368  ptolemy  15411  tangtx  15425  rpcxpneg  15494  rpcxpsub  15495  cxprec  15497  rpcxproot  15501  cxpcom  15525  rpabscxpbnd  15527  wilthlem1  15567  sgmppw  15579  1sgmprm  15581  1sgm2ppw  15582  perfectlem1  15586  perfectlem2  15587  lgsvalmod  15611  lgsneg  15616  lgsdilem  15619  lgsne0  15630  lgssq  15632  lgssq2  15633  gausslemma2dlem1f1o  15652  gausslemma2dlem6  15659  gausslemma2d  15661  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem4  15665  lgsquadlem1  15669  lgsquadlem3  15671  lgsquad3  15676  m1lgs  15677  peano4nninf  16145  nninfalllem1  16147  nninfall  16148  nninfsellemqall  16154  qdencn  16168