Theorem 3eqtr3d 2237

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  mpteqb  5655  fvmptt  5656  fsnunfv  5766  f1ocnvfv1  5827  f1ocnvfv2  5828  fcof1  5833  caov12d  6109  caov13d  6111  caov411d  6113  caovimo  6121  tfrlem5  6381  tfrlemiubacc  6397  tfr1onlemubacc  6413  tfrcllemubacc  6426  nndir  6557  fopwdom  6906  updjud  7157  omp1eomlem  7169  addassnqg  7466  distrnqg  7471  enq0tr  7518  distrnq0  7543  distnq0r  7547  addnqprl  7613  addnqpru  7614  appdivnq  7647  ltmprr  7726  addcmpblnr  7823  mulcmpblnrlemg  7824  ltsrprg  7831  1idsr  7852  pn0sr  7855  mulgt0sr  7862  map2psrprg  7889  axmulass  7957  ax0id  7962  recriota  7974  mul12  8172  mul4  8175  readdcan  8183  add12  8201  cnegexlem2  8219  addcan  8223  ppncan  8285  addsub4  8286  subeqxfrd  8406  subaddeqd  8412  muladd  8427  mulcanapd  8705  receuap  8713  div13ap  8737  divdivdivap  8757  divcanap5  8758  divdivap1  8767  divdivap2  8768  halfaddsub  9242  fztp  10170  fseq1p1m1  10186  flqzadd  10405  flqdiv  10430  mulp1mod1  10474  modqnegd  10488  modqsub12d  10490  q2submod  10494  modsumfzodifsn  10505  seq3m1  10582  seq3caopr  10604  seqcaoprg  10605  iseqf1olemab  10611  iseqf1olemnanb  10612  seq3f1olemqsumk  10621  seqf1og  10630  exprecap  10689  expsubap  10696  zesq  10767  nn0opthlem1d  10829  facnn2  10843  faclbnd6  10853  zfz1isolemsplit  10947  seq3coll  10951  shftval3  11009  crre  11039  resub  11052  imsub  11060  cjsub  11074  bdtrilem  11421  bdtri  11422  climshft2  11488  nnf1o  11558  fsumf1o  11572  isumss  11573  fisumss  11574  fsumadd  11588  isumclim3  11605  fsummulc2  11630  fsumsub  11634  telfsumo  11648  telfsumo2  11649  hashiun  11660  bcxmas  11671  isumshft  11672  trireciplem  11682  geoserap  11689  geo2sum2  11697  fprodf1o  11770  prodssdc  11771  fprodssdc  11772  fprodmul  11773  fprodm1  11780  sinsub  11922  cossub  11923  p1modz1  11976  bitsinv1lem  12143  bitsinv1  12144  gcdaddm  12176  modgcd  12183  bezoutlemnewy  12188  absmulgcd  12209  gcdmultiplez  12213  eucalg  12252  lcmgcd  12271  lcmid  12273  numdensq  12395  dfphi2  12413  phiprm  12416  fermltl  12427  prmdiveq  12429  hashgcdlem  12431  odzdvds  12439  powm2modprm  12446  modprm0  12448  coprimeprodsq  12451  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem16  12473  pcaddlem  12533  sumhashdc  12541  fldivp1  12542  pcfac  12544  pockthlem  12550  4sqlem12  12596  4sqlem15  12599  ennnfonelem1  12649  ennnfonelemex  12656  topnpropgd  12955  qusaddvallemg  13035  grpinvalem  13087  grpinva  13088  grprida  13089  mnd12g  13130  resmhm  13189  grprcan  13239  grplcan  13264  grpasscan1  13265  grpinv11  13271  grpinvnz  13273  grplmulf1o  13276  grpinvpropdg  13277  grpinvadd  13280  grpsubsub4  13295  dfgrp3m  13301  imasgrp2  13316  mhmid  13321  mhmmnd  13322  mulgz  13356  mulgdirlem  13359  mulgdir  13360  mulgass  13365  mulgsubdir  13368  mulgpropdg  13370  isnsg3  13413  nmzsubg  13416  ssnmz  13417  eqger  13430  eqglact  13431  ghminv  13456  conjnmz  13485  ghmcmn  13533  gsumfzconst  13547  gsumfzmhm2  13550  rnglz  13577  rngrz  13578  isrngd  13585  ringcom  13663  crngpropd  13671  isringd  13673  ringlz  13675  ringrz  13676  ring1eq0  13680  ringmneg1  13685  mulgass3  13717  unitgrp  13748  rngidpropdg  13778  invrpropdg  13781  isrhm2d  13797  rhmunitinv  13810  subrngpropd  13848  subrginv  13869  subrgunit  13871  subrgpropd  13885  rhmpropd  13886  unitrrg  13899  lmodvs0  13954  lmodvneg1  13962  lmodcom  13965  lmodsubdi  13976  lss0v  14062  lidlrsppropdg  14127  mulgrhm2  14242  znidomb  14290  restin  14496  blpnfctr  14759  xmssym  14789  limcimolemlt  14984  dvmulxxbr  15022  dvrecap  15033  dvmptaddx  15039  dvmptmulx  15040  dvmptnegcn  15042  dvmptsubcn  15043  dvmptcjx  15044  dveflem  15046  plymullem1  15068  dvply1  15085  sin0pilem1  15101  ptolemy  15144  tangtx  15158  rpcxpneg  15227  rpcxpsub  15228  cxprec  15230  rpcxproot  15234  cxpcom  15258  rpabscxpbnd  15260  wilthlem1  15300  sgmppw  15312  1sgmprm  15314  1sgm2ppw  15315  perfectlem1  15319  perfectlem2  15320  lgsvalmod  15344  lgsneg  15349  lgsdilem  15352  lgsne0  15363  lgssq  15365  lgssq2  15366  gausslemma2dlem1f1o  15385  gausslemma2dlem6  15392  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem4  15398  lgsquadlem1  15402  lgsquadlem3  15404  lgsquad3  15409  m1lgs  15410  peano4nninf  15737  nninfalllem1  15739  nninfall  15740  nninfsellemqall  15746  qdencn  15758