Theorem 3eqtr3d 2275

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

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

This theorem is referenced by:  mpteqb  5773  fvmptt  5774  fsnunfv  5890  f1ocnvfv1  5956  f1ocnvfv2  5957  fcof1  5962  caov12d  6244  caov13d  6246  caov411d  6248  caovimo  6256  tfrlem5  6558  tfrlemiubacc  6574  tfr1onlemubacc  6590  tfrcllemubacc  6603  nndir  6736  en2  7078  fopwdom  7102  updjud  7386  omp1eomlem  7398  addassnqg  7713  distrnqg  7718  enq0tr  7765  distrnq0  7790  distnq0r  7794  addnqprl  7860  addnqpru  7861  appdivnq  7894  ltmprr  7973  addcmpblnr  8070  mulcmpblnrlemg  8071  ltsrprg  8078  1idsr  8099  pn0sr  8102  mulgt0sr  8109  map2psrprg  8136  axmulass  8204  ax0id  8209  recriota  8221  mul12  8418  mul4  8421  readdcan  8429  add12  8447  cnegexlem2  8465  addcan  8469  ppncan  8531  addsub4  8532  subeqxfrd  8652  subaddeqd  8658  muladd  8674  mulcanapd  8952  receuap  8960  div13ap  8984  divdivdivap  9004  divcanap5  9005  divdivap1  9014  divdivap2  9015  halfaddsub  9489  lincmble  10356  fztp  10434  fseq1p1m1  10450  flqzadd  10682  flqdiv  10707  mulp1mod1  10751  modqnegd  10765  modqsub12d  10767  q2submod  10771  modsumfzodifsn  10782  seq3m1  10859  seq3caopr  10881  seqcaoprg  10882  iseqf1olemab  10888  iseqf1olemnanb  10889  seq3f1olemqsumk  10898  seqf1og  10907  exprecap  10966  expsubap  10973  zesq  11045  nn0opthlem1d  11107  facnn2  11121  faclbnd6  11131  bcm1n  11156  hashfibclem  11231  zfz1isolemsplit  11235  seq3coll  11239  ccatopth  11433  shftval3  11537  crre  11567  resub  11580  imsub  11588  cjsub  11602  bdtrilem  11949  bdtri  11950  climshft2  12016  nnf1o  12087  fsumf1o  12101  isumss  12102  fisumss  12103  fsumadd  12117  isumclim3  12134  fsummulc2  12159  fsumsub  12163  telfsumo  12177  telfsumo2  12178  hashiun  12189  bcxmas  12200  isumshft  12201  trireciplem  12211  geoserap  12218  geo2sum2  12226  fprodf1o  12299  prodssdc  12300  fprodssdc  12301  fprodmul  12302  fprodm1  12309  sinsub  12451  cossub  12452  p1modz1  12505  bitsinv1lem  12672  bitsinv1  12673  gcdaddm  12705  modgcd  12712  bezoutlemnewy  12717  absmulgcd  12738  gcdmultiplez  12742  eucalg  12781  lcmgcd  12800  lcmid  12802  numdensq  12924  dfphi2  12942  phiprm  12945  fermltl  12956  prmdiveq  12958  hashgcdlem  12960  odzdvds  12968  powm2modprm  12975  modprm0  12977  coprimeprodsq  12980  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem16  13002  pcaddlem  13062  sumhashdc  13070  fldivp1  13071  pcfac  13073  pockthlem  13079  4sqlem12  13125  4sqlem15  13128  ennnfonelem1  13242  ennnfonelemex  13249  topnpropgd  13550  qusaddvallemg  13597  grpinvalem  13648  grpinva  13649  grprida  13650  mnd12g  13689  resmhm  13742  grprcan  13792  grplcan  13817  grpasscan1  13818  grpinv11  13824  grpinvnz  13826  grplmulf1o  13829  grpinvpropdg  13830  grpinvadd  13833  grpsubsub4  13848  dfgrp3m  13854  imasgrp2  13863  mhmid  13868  mhmmnd  13869  mulgz  13903  mulgdirlem  13906  mulgdir  13907  mulgass  13912  mulgsubdir  13915  mulgpropdg  13917  isnsg3  13960  nmzsubg  13963  ssnmz  13964  eqger  13977  eqglact  13978  ghminv  14003  conjnmz  14032  ghmcmn  14080  gsumfzconst  14094  gsumfzmhm2  14097  rnglz  14184  rngrz  14185  isrngd  14192  ringcom  14274  crngpropd  14282  isringd  14284  ringlz  14286  ringrz  14287  ring1eq0  14291  ringmneg1  14296  mulgass3  14329  unitgrp  14361  rngidpropdg  14391  invrpropdg  14394  isrhm2d  14410  rhmunitinv  14423  subrngpropd  14462  subrginv  14483  subrgunit  14485  subrgpropd  14499  rhmpropd  14500  unitrrg  14514  aprlring  14538  lmodvs0  14596  lmodvneg1  14604  lmodcom  14607  lmodsubdi  14618  lss0v  14704  lidlrsppropdg  14769  mulgrhm2  14884  znidomb  14932  restin  15167  blpnfctr  15430  xmssym  15460  limcimolemlt  15655  dvmulxxbr  15693  dvrecap  15704  dvmptaddx  15710  dvmptmulx  15711  dvmptnegcn  15713  dvmptsubcn  15714  dvmptcjx  15715  dveflem  15717  plymullem1  15739  dvply1  15756  sin0pilem1  15772  ptolemy  15815  tangtx  15829  rpcxpneg  15898  rpcxpsub  15899  cxprec  15901  rpcxproot  15905  cxpcom  15929  rpabscxpbnd  15931  pellexlem2  15972  wilthlem1  15974  sgmppw  15986  1sgmprm  15988  1sgm2ppw  15989  perfectlem1  15993  perfectlem2  15994  lgsvalmod  16018  lgsneg  16023  lgsdilem  16026  lgsne0  16037  lgssq  16039  lgssq2  16040  gausslemma2dlem1f1o  16059  gausslemma2dlem6  16066  gausslemma2d  16068  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem4  16072  lgsquadlem1  16076  lgsquadlem3  16078  lgsquad3  16083  m1lgs  16084  p1evtxdeqfilem  16432  peano4nninf  16910  nninfalllem1  16912  nninfall  16913  nninfsellemqall  16919  qdencn  16933  qdiff  16959