Theorem 3eqtr3d 2272

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  mpteqb  5746  fvmptt  5747  fsnunfv  5863  f1ocnvfv1  5928  f1ocnvfv2  5929  fcof1  5934  caov12d  6214  caov13d  6216  caov411d  6218  caovimo  6226  tfrlem5  6523  tfrlemiubacc  6539  tfr1onlemubacc  6555  tfrcllemubacc  6568  nndir  6701  en2  7041  fopwdom  7065  updjud  7341  omp1eomlem  7353  addassnqg  7662  distrnqg  7667  enq0tr  7714  distrnq0  7739  distnq0r  7743  addnqprl  7809  addnqpru  7810  appdivnq  7843  ltmprr  7922  addcmpblnr  8019  mulcmpblnrlemg  8020  ltsrprg  8027  1idsr  8048  pn0sr  8051  mulgt0sr  8058  map2psrprg  8085  axmulass  8153  ax0id  8158  recriota  8170  mul12  8367  mul4  8370  readdcan  8378  add12  8396  cnegexlem2  8414  addcan  8418  ppncan  8480  addsub4  8481  subeqxfrd  8601  subaddeqd  8607  muladd  8622  mulcanapd  8900  receuap  8908  div13ap  8932  divdivdivap  8952  divcanap5  8953  divdivap1  8962  divdivap2  8963  halfaddsub  9437  lincmble  10300  fztp  10375  fseq1p1m1  10391  flqzadd  10621  flqdiv  10646  mulp1mod1  10690  modqnegd  10704  modqsub12d  10706  q2submod  10710  modsumfzodifsn  10721  seq3m1  10798  seq3caopr  10820  seqcaoprg  10821  iseqf1olemab  10827  iseqf1olemnanb  10828  seq3f1olemqsumk  10837  seqf1og  10846  exprecap  10905  expsubap  10912  zesq  10983  nn0opthlem1d  11045  facnn2  11059  faclbnd6  11069  zfz1isolemsplit  11165  seq3coll  11169  ccatopth  11363  shftval3  11467  crre  11497  resub  11510  imsub  11518  cjsub  11532  bdtrilem  11879  bdtri  11880  climshft2  11946  nnf1o  12017  fsumf1o  12031  isumss  12032  fisumss  12033  fsumadd  12047  isumclim3  12064  fsummulc2  12089  fsumsub  12093  telfsumo  12107  telfsumo2  12108  hashiun  12119  bcxmas  12130  isumshft  12131  trireciplem  12141  geoserap  12148  geo2sum2  12156  fprodf1o  12229  prodssdc  12230  fprodssdc  12231  fprodmul  12232  fprodm1  12239  sinsub  12381  cossub  12382  p1modz1  12435  bitsinv1lem  12602  bitsinv1  12603  gcdaddm  12635  modgcd  12642  bezoutlemnewy  12647  absmulgcd  12668  gcdmultiplez  12672  eucalg  12711  lcmgcd  12730  lcmid  12732  numdensq  12854  dfphi2  12872  phiprm  12875  fermltl  12886  prmdiveq  12888  hashgcdlem  12890  odzdvds  12898  powm2modprm  12905  modprm0  12907  coprimeprodsq  12910  pythagtriplem6  12923  pythagtriplem7  12924  pythagtriplem12  12928  pythagtriplem14  12930  pythagtriplem16  12932  pcaddlem  12992  sumhashdc  13000  fldivp1  13001  pcfac  13003  pockthlem  13009  4sqlem12  13055  4sqlem15  13058  ennnfonelem1  13108  ennnfonelemex  13115  topnpropgd  13416  qusaddvallemg  13496  grpinvalem  13548  grpinva  13549  grprida  13550  mnd12g  13591  resmhm  13650  grprcan  13700  grplcan  13725  grpasscan1  13726  grpinv11  13732  grpinvnz  13734  grplmulf1o  13737  grpinvpropdg  13738  grpinvadd  13741  grpsubsub4  13756  dfgrp3m  13762  imasgrp2  13777  mhmid  13782  mhmmnd  13783  mulgz  13817  mulgdirlem  13820  mulgdir  13821  mulgass  13826  mulgsubdir  13829  mulgpropdg  13831  isnsg3  13874  nmzsubg  13877  ssnmz  13878  eqger  13891  eqglact  13892  ghminv  13917  conjnmz  13946  ghmcmn  13994  gsumfzconst  14008  gsumfzmhm2  14011  rnglz  14039  rngrz  14040  isrngd  14047  ringcom  14125  crngpropd  14133  isringd  14135  ringlz  14137  ringrz  14138  ring1eq0  14142  ringmneg1  14147  mulgass3  14179  unitgrp  14211  rngidpropdg  14241  invrpropdg  14244  isrhm2d  14260  rhmunitinv  14273  subrngpropd  14311  subrginv  14332  subrgunit  14334  subrgpropd  14348  rhmpropd  14349  unitrrg  14363  lmodvs0  14418  lmodvneg1  14426  lmodcom  14429  lmodsubdi  14440  lss0v  14526  lidlrsppropdg  14591  mulgrhm2  14706  znidomb  14754  restin  14987  blpnfctr  15250  xmssym  15280  limcimolemlt  15475  dvmulxxbr  15513  dvrecap  15524  dvmptaddx  15530  dvmptmulx  15531  dvmptnegcn  15533  dvmptsubcn  15534  dvmptcjx  15535  dveflem  15537  plymullem1  15559  dvply1  15576  sin0pilem1  15592  ptolemy  15635  tangtx  15649  rpcxpneg  15718  rpcxpsub  15719  cxprec  15721  rpcxproot  15725  cxpcom  15749  rpabscxpbnd  15751  pellexlem2  15792  wilthlem1  15794  sgmppw  15806  1sgmprm  15808  1sgm2ppw  15809  perfectlem1  15813  perfectlem2  15814  lgsvalmod  15838  lgsneg  15843  lgsdilem  15846  lgsne0  15857  lgssq  15859  lgssq2  15860  gausslemma2dlem1f1o  15879  gausslemma2dlem6  15886  gausslemma2d  15888  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem4  15892  lgsquadlem1  15896  lgsquadlem3  15898  lgsquad3  15903  m1lgs  15904  p1evtxdeqfilem  16252  peano4nninf  16732  nninfalllem1  16734  nninfall  16735  nninfsellemqall  16741  qdencn  16755  qdiff  16781