Theorem 3eqtr3d 2246

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 2240	. 2 |- ( ph -> B = C )
4		3eqtr3d.3	. 2 |- ( ph -> B = D )
5	3, 4	eqtr3d 2240	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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  mpteqb  5672  fvmptt  5673  fsnunfv  5787  f1ocnvfv1  5848  f1ocnvfv2  5849  fcof1  5854  caov12d  6130  caov13d  6132  caov411d  6134  caovimo  6142  tfrlem5  6402  tfrlemiubacc  6418  tfr1onlemubacc  6434  tfrcllemubacc  6447  nndir  6578  en2  6914  fopwdom  6935  updjud  7186  omp1eomlem  7198  addassnqg  7497  distrnqg  7502  enq0tr  7549  distrnq0  7574  distnq0r  7578  addnqprl  7644  addnqpru  7645  appdivnq  7678  ltmprr  7757  addcmpblnr  7854  mulcmpblnrlemg  7855  ltsrprg  7862  1idsr  7883  pn0sr  7886  mulgt0sr  7893  map2psrprg  7920  axmulass  7988  ax0id  7993  recriota  8005  mul12  8203  mul4  8206  readdcan  8214  add12  8232  cnegexlem2  8250  addcan  8254  ppncan  8316  addsub4  8317  subeqxfrd  8437  subaddeqd  8443  muladd  8458  mulcanapd  8736  receuap  8744  div13ap  8768  divdivdivap  8788  divcanap5  8789  divdivap1  8798  divdivap2  8799  halfaddsub  9273  fztp  10202  fseq1p1m1  10218  flqzadd  10443  flqdiv  10468  mulp1mod1  10512  modqnegd  10526  modqsub12d  10528  q2submod  10532  modsumfzodifsn  10543  seq3m1  10620  seq3caopr  10642  seqcaoprg  10643  iseqf1olemab  10649  iseqf1olemnanb  10650  seq3f1olemqsumk  10659  seqf1og  10668  exprecap  10727  expsubap  10734  zesq  10805  nn0opthlem1d  10867  facnn2  10881  faclbnd6  10891  zfz1isolemsplit  10985  seq3coll  10989  shftval3  11171  crre  11201  resub  11214  imsub  11222  cjsub  11236  bdtrilem  11583  bdtri  11584  climshft2  11650  nnf1o  11720  fsumf1o  11734  isumss  11735  fisumss  11736  fsumadd  11750  isumclim3  11767  fsummulc2  11792  fsumsub  11796  telfsumo  11810  telfsumo2  11811  hashiun  11822  bcxmas  11833  isumshft  11834  trireciplem  11844  geoserap  11851  geo2sum2  11859  fprodf1o  11932  prodssdc  11933  fprodssdc  11934  fprodmul  11935  fprodm1  11942  sinsub  12084  cossub  12085  p1modz1  12138  bitsinv1lem  12305  bitsinv1  12306  gcdaddm  12338  modgcd  12345  bezoutlemnewy  12350  absmulgcd  12371  gcdmultiplez  12375  eucalg  12414  lcmgcd  12433  lcmid  12435  numdensq  12557  dfphi2  12575  phiprm  12578  fermltl  12589  prmdiveq  12591  hashgcdlem  12593  odzdvds  12601  powm2modprm  12608  modprm0  12610  coprimeprodsq  12613  pythagtriplem6  12626  pythagtriplem7  12627  pythagtriplem12  12631  pythagtriplem14  12633  pythagtriplem16  12635  pcaddlem  12695  sumhashdc  12703  fldivp1  12704  pcfac  12706  pockthlem  12712  4sqlem12  12758  4sqlem15  12761  ennnfonelem1  12811  ennnfonelemex  12818  topnpropgd  13118  qusaddvallemg  13198  grpinvalem  13250  grpinva  13251  grprida  13252  mnd12g  13293  resmhm  13352  grprcan  13402  grplcan  13427  grpasscan1  13428  grpinv11  13434  grpinvnz  13436  grplmulf1o  13439  grpinvpropdg  13440  grpinvadd  13443  grpsubsub4  13458  dfgrp3m  13464  imasgrp2  13479  mhmid  13484  mhmmnd  13485  mulgz  13519  mulgdirlem  13522  mulgdir  13523  mulgass  13528  mulgsubdir  13531  mulgpropdg  13533  isnsg3  13576  nmzsubg  13579  ssnmz  13580  eqger  13593  eqglact  13594  ghminv  13619  conjnmz  13648  ghmcmn  13696  gsumfzconst  13710  gsumfzmhm2  13713  rnglz  13740  rngrz  13741  isrngd  13748  ringcom  13826  crngpropd  13834  isringd  13836  ringlz  13838  ringrz  13839  ring1eq0  13843  ringmneg1  13848  mulgass3  13880  unitgrp  13911  rngidpropdg  13941  invrpropdg  13944  isrhm2d  13960  rhmunitinv  13973  subrngpropd  14011  subrginv  14032  subrgunit  14034  subrgpropd  14048  rhmpropd  14049  unitrrg  14062  lmodvs0  14117  lmodvneg1  14125  lmodcom  14128  lmodsubdi  14139  lss0v  14225  lidlrsppropdg  14290  mulgrhm2  14405  znidomb  14453  restin  14681  blpnfctr  14944  xmssym  14974  limcimolemlt  15169  dvmulxxbr  15207  dvrecap  15218  dvmptaddx  15224  dvmptmulx  15225  dvmptnegcn  15227  dvmptsubcn  15228  dvmptcjx  15229  dveflem  15231  plymullem1  15253  dvply1  15270  sin0pilem1  15286  ptolemy  15329  tangtx  15343  rpcxpneg  15412  rpcxpsub  15413  cxprec  15415  rpcxproot  15419  cxpcom  15443  rpabscxpbnd  15445  wilthlem1  15485  sgmppw  15497  1sgmprm  15499  1sgm2ppw  15500  perfectlem1  15504  perfectlem2  15505  lgsvalmod  15529  lgsneg  15534  lgsdilem  15537  lgsne0  15548  lgssq  15550  lgssq2  15551  gausslemma2dlem1f1o  15570  gausslemma2dlem6  15577  gausslemma2d  15579  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem4  15583  lgsquadlem1  15587  lgsquadlem3  15589  lgsquad3  15594  m1lgs  15595  peano4nninf  15980  nninfalllem1  15982  nninfall  15983  nninfsellemqall  15989  qdencn  16003