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  5670  fvmptt  5671  fsnunfv  5785  f1ocnvfv1  5846  f1ocnvfv2  5847  fcof1  5852  caov12d  6128  caov13d  6130  caov411d  6132  caovimo  6140  tfrlem5  6400  tfrlemiubacc  6416  tfr1onlemubacc  6432  tfrcllemubacc  6445  nndir  6576  en2  6912  fopwdom  6933  updjud  7184  omp1eomlem  7196  addassnqg  7495  distrnqg  7500  enq0tr  7547  distrnq0  7572  distnq0r  7576  addnqprl  7642  addnqpru  7643  appdivnq  7676  ltmprr  7755  addcmpblnr  7852  mulcmpblnrlemg  7853  ltsrprg  7860  1idsr  7881  pn0sr  7884  mulgt0sr  7891  map2psrprg  7918  axmulass  7986  ax0id  7991  recriota  8003  mul12  8201  mul4  8204  readdcan  8212  add12  8230  cnegexlem2  8248  addcan  8252  ppncan  8314  addsub4  8315  subeqxfrd  8435  subaddeqd  8441  muladd  8456  mulcanapd  8734  receuap  8742  div13ap  8766  divdivdivap  8786  divcanap5  8787  divdivap1  8796  divdivap2  8797  halfaddsub  9271  fztp  10200  fseq1p1m1  10216  flqzadd  10441  flqdiv  10466  mulp1mod1  10510  modqnegd  10524  modqsub12d  10526  q2submod  10530  modsumfzodifsn  10541  seq3m1  10618  seq3caopr  10640  seqcaoprg  10641  iseqf1olemab  10647  iseqf1olemnanb  10648  seq3f1olemqsumk  10657  seqf1og  10666  exprecap  10725  expsubap  10732  zesq  10803  nn0opthlem1d  10865  facnn2  10879  faclbnd6  10889  zfz1isolemsplit  10983  seq3coll  10987  shftval3  11138  crre  11168  resub  11181  imsub  11189  cjsub  11203  bdtrilem  11550  bdtri  11551  climshft2  11617  nnf1o  11687  fsumf1o  11701  isumss  11702  fisumss  11703  fsumadd  11717  isumclim3  11734  fsummulc2  11759  fsumsub  11763  telfsumo  11777  telfsumo2  11778  hashiun  11789  bcxmas  11800  isumshft  11801  trireciplem  11811  geoserap  11818  geo2sum2  11826  fprodf1o  11899  prodssdc  11900  fprodssdc  11901  fprodmul  11902  fprodm1  11909  sinsub  12051  cossub  12052  p1modz1  12105  bitsinv1lem  12272  bitsinv1  12273  gcdaddm  12305  modgcd  12312  bezoutlemnewy  12317  absmulgcd  12338  gcdmultiplez  12342  eucalg  12381  lcmgcd  12400  lcmid  12402  numdensq  12524  dfphi2  12542  phiprm  12545  fermltl  12556  prmdiveq  12558  hashgcdlem  12560  odzdvds  12568  powm2modprm  12575  modprm0  12577  coprimeprodsq  12580  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem12  12598  pythagtriplem14  12600  pythagtriplem16  12602  pcaddlem  12662  sumhashdc  12670  fldivp1  12671  pcfac  12673  pockthlem  12679  4sqlem12  12725  4sqlem15  12728  ennnfonelem1  12778  ennnfonelemex  12785  topnpropgd  13085  qusaddvallemg  13165  grpinvalem  13217  grpinva  13218  grprida  13219  mnd12g  13260  resmhm  13319  grprcan  13369  grplcan  13394  grpasscan1  13395  grpinv11  13401  grpinvnz  13403  grplmulf1o  13406  grpinvpropdg  13407  grpinvadd  13410  grpsubsub4  13425  dfgrp3m  13431  imasgrp2  13446  mhmid  13451  mhmmnd  13452  mulgz  13486  mulgdirlem  13489  mulgdir  13490  mulgass  13495  mulgsubdir  13498  mulgpropdg  13500  isnsg3  13543  nmzsubg  13546  ssnmz  13547  eqger  13560  eqglact  13561  ghminv  13586  conjnmz  13615  ghmcmn  13663  gsumfzconst  13677  gsumfzmhm2  13680  rnglz  13707  rngrz  13708  isrngd  13715  ringcom  13793  crngpropd  13801  isringd  13803  ringlz  13805  ringrz  13806  ring1eq0  13810  ringmneg1  13815  mulgass3  13847  unitgrp  13878  rngidpropdg  13908  invrpropdg  13911  isrhm2d  13927  rhmunitinv  13940  subrngpropd  13978  subrginv  13999  subrgunit  14001  subrgpropd  14015  rhmpropd  14016  unitrrg  14029  lmodvs0  14084  lmodvneg1  14092  lmodcom  14095  lmodsubdi  14106  lss0v  14192  lidlrsppropdg  14257  mulgrhm2  14372  znidomb  14420  restin  14648  blpnfctr  14911  xmssym  14941  limcimolemlt  15136  dvmulxxbr  15174  dvrecap  15185  dvmptaddx  15191  dvmptmulx  15192  dvmptnegcn  15194  dvmptsubcn  15195  dvmptcjx  15196  dveflem  15198  plymullem1  15220  dvply1  15237  sin0pilem1  15253  ptolemy  15296  tangtx  15310  rpcxpneg  15379  rpcxpsub  15380  cxprec  15382  rpcxproot  15386  cxpcom  15410  rpabscxpbnd  15412  wilthlem1  15452  sgmppw  15464  1sgmprm  15466  1sgm2ppw  15467  perfectlem1  15471  perfectlem2  15472  lgsvalmod  15496  lgsneg  15501  lgsdilem  15504  lgsne0  15515  lgssq  15517  lgssq2  15518  gausslemma2dlem1f1o  15537  gausslemma2dlem6  15544  gausslemma2d  15546  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem4  15550  lgsquadlem1  15554  lgsquadlem3  15556  lgsquad3  15561  m1lgs  15562  peano4nninf  15943  nninfalllem1  15945  nninfall  15946  nninfsellemqall  15952  qdencn  15966