Theorem 3eqtr3d 2279

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  mpteqb  5796  fvmptt  5797  fsnunfv  5916  f1ocnvfv1  5983  f1ocnvfv2  5984  fcof1  5989  caov12d  6271  caov13d  6273  caov411d  6275  caovimo  6283  tfrlem5  6585  tfrlemiubacc  6601  tfr1onlemubacc  6617  tfrcllemubacc  6630  nndir  6763  en2  7112  fopwdom  7136  updjud  7422  omp1eomlem  7434  addassnqg  7749  distrnqg  7754  enq0tr  7801  distrnq0  7826  distnq0r  7830  addnqprl  7896  addnqpru  7897  appdivnq  7930  ltmprr  8009  addcmpblnr  8106  mulcmpblnrlemg  8107  ltsrprg  8114  1idsr  8135  pn0sr  8138  mulgt0sr  8145  map2psrprg  8172  axmulass  8240  ax0id  8245  recriota  8257  mul12  8455  mul4  8458  readdcan  8466  add12  8484  cnegexlem2  8502  addcan  8506  ppncan  8568  addsub4  8569  subeqxfrd  8689  subaddeqd  8695  muladd  8711  mulcanapd  8989  receuap  8999  div13ap  9023  divdivdivap  9043  divcanap5  9044  divdivap1  9053  divdivap2  9054  halfaddsub  9539  lincmble  10406  fztp  10485  fseq1p1m1  10501  flqzadd  10733  flqdiv  10758  mulp1mod1  10802  modqnegd  10816  modqsub12d  10818  q2submod  10822  modsumfzodifsn  10833  seq3m1  10910  seq3caopr  10932  seqcaoprg  10933  iseqf1olemab  10939  iseqf1olemnanb  10940  seq3f1olemqsumk  10949  seqf1og  10958  exprecap  11017  expsubap  11024  zesq  11096  nn0opthlem1d  11158  facnn2  11172  faclbnd6  11182  bcm1n  11207  hashfibclem  11282  hashfac  11288  zfz1isolemsplit  11290  seq3coll  11294  ccatopth  11488  shftval3  11592  crre  11622  resub  11635  imsub  11643  cjsub  11657  sq01  11660  bdtrilem  12005  bdtri  12006  climshft2  12072  nnf1o  12143  fsumf1o  12157  isumss  12158  fisumss  12159  fsumadd  12173  isumclim3  12190  fsummulc2  12215  fsumsub  12219  telfsumo  12233  telfsumo2  12234  hashiun  12245  bcxmas  12256  isumshft  12257  trireciplem  12267  geoserap  12274  geo2sum2  12282  fprodf1o  12355  prodssdc  12356  fprodssdc  12357  fprodmul  12358  fprodm1  12365  sinsub  12507  cossub  12508  p1modz1  12561  bitsinv1lem  12728  bitsinv1  12729  gcdaddm  12761  modgcd  12768  bezoutlemnewy  12773  absmulgcd  12794  gcdmultiplez  12798  eucalg  12837  lcmgcd  12856  lcmid  12858  numdensq  12980  dfphi2  12998  phiprm  13001  fermltl  13012  prmdiveq  13014  hashgcdlem  13016  odzdvds  13024  powm2modprm  13031  modprm0  13033  coprimeprodsq  13036  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem16  13058  pcaddlem  13118  sumhashdc  13126  fldivp1  13127  pcfac  13129  pockthlem  13135  4sqlem12  13181  4sqlem15  13184  ennnfonelem1  13298  ennnfonelemex  13305  topnpropgd  13607  qusaddvallemg  13654  grpinvalem  13705  grpinva  13706  grprida  13707  mnd12g  13741  resmhm  13794  grprcan  13842  grplcan  13867  grpasscan1  13868  grpinv11  13874  grpinvnz  13876  grplmulf1o  13879  grpinvpropdg  13880  grpinvadd  13883  grpsubsub4  13898  dfgrp3m  13904  imasgrp2  13913  mhmid  13918  mhmmnd  13919  mulgz  13953  mulgdirlem  13956  mulgdir  13957  mulgass  13962  mulgsubdir  13965  mulgpropdg  13967  isnsg3  14010  nmzsubg  14013  ssnmz  14014  eqger  14027  eqglact  14028  ghminv  14053  conjnmz  14082  ghmcmn  14131  gzsumconst  14143  gzsummhm2  14146  gsummhm2fi  14165  rnglz  14244  rngrz  14245  isrngd  14252  ringcom  14336  crngpropd  14344  isringd  14346  ringlz  14348  ringrz  14349  ring1eq0  14353  ringmneg1  14358  mulgass3  14391  unitgrp  14423  rngidpropdg  14453  invrpropdg  14456  isrhm2d  14472  rhmunitinv  14485  subrngpropd  14524  subrginv  14545  subrgunit  14547  subrgpropd  14561  rhmpropd  14562  unitrrg  14576  aprlring  14600  lmodvs0  14659  lmodvneg1  14667  lmodcom  14670  lmodsubdi  14681  lss0v  14767  lidlrsppropdg  14832  mulgrhm2  14945  znidomb  14993  asclpropd  15040  restin  15277  blpnfctr  15540  xmssym  15570  limcimolemlt  15765  dvmulxxbr  15803  dvrecap  15814  dvmptaddx  15820  dvmptmulx  15821  dvmptnegcn  15823  dvmptsubcn  15824  dvmptcjx  15825  dveflem  15827  plymullem1  15849  dvply1  15866  sin0pilem1  15882  ptolemy  15925  tangtx  15939  rpcxpneg  16009  rpcxpsub  16010  cxprec  16012  rpcxproot  16016  cxpcom  16040  rpabscxpbnd  16042  pellexlem2  16092  wilthlem1  16094  sgmppw  16106  1sgmprm  16108  1sgm2ppw  16109  perfectlem1  16113  perfectlem2  16114  lgsvalmod  16138  lgsneg  16143  lgsdilem  16146  lgsne0  16157  lgssq  16159  lgssq2  16160  gausslemma2dlem1f1o  16179  gausslemma2dlem6  16186  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem4  16192  lgsquadlem1  16196  lgsquadlem3  16198  lgsquad3  16203  m1lgs  16204  p1evtxdeqfilem  16552  peano4nninf  17049  nninfalllem1  17051  nninfall  17052  nninfsellemqall  17058  qdencn  17072  qdiff  17098