Theorem 3eqtr3d 2270

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  mpteqb  5727  fvmptt  5728  fsnunfv  5844  f1ocnvfv1  5907  f1ocnvfv2  5908  fcof1  5913  caov12d  6193  caov13d  6195  caov411d  6197  caovimo  6205  tfrlem5  6466  tfrlemiubacc  6482  tfr1onlemubacc  6498  tfrcllemubacc  6511  nndir  6644  en2  6981  fopwdom  7005  updjud  7260  omp1eomlem  7272  addassnqg  7580  distrnqg  7585  enq0tr  7632  distrnq0  7657  distnq0r  7661  addnqprl  7727  addnqpru  7728  appdivnq  7761  ltmprr  7840  addcmpblnr  7937  mulcmpblnrlemg  7938  ltsrprg  7945  1idsr  7966  pn0sr  7969  mulgt0sr  7976  map2psrprg  8003  axmulass  8071  ax0id  8076  recriota  8088  mul12  8286  mul4  8289  readdcan  8297  add12  8315  cnegexlem2  8333  addcan  8337  ppncan  8399  addsub4  8400  subeqxfrd  8520  subaddeqd  8526  muladd  8541  mulcanapd  8819  receuap  8827  div13ap  8851  divdivdivap  8871  divcanap5  8872  divdivap1  8881  divdivap2  8882  halfaddsub  9356  fztp  10286  fseq1p1m1  10302  flqzadd  10530  flqdiv  10555  mulp1mod1  10599  modqnegd  10613  modqsub12d  10615  q2submod  10619  modsumfzodifsn  10630  seq3m1  10707  seq3caopr  10729  seqcaoprg  10730  iseqf1olemab  10736  iseqf1olemnanb  10737  seq3f1olemqsumk  10746  seqf1og  10755  exprecap  10814  expsubap  10821  zesq  10892  nn0opthlem1d  10954  facnn2  10968  faclbnd6  10978  zfz1isolemsplit  11073  seq3coll  11077  ccatopth  11264  shftval3  11354  crre  11384  resub  11397  imsub  11405  cjsub  11419  bdtrilem  11766  bdtri  11767  climshft2  11833  nnf1o  11903  fsumf1o  11917  isumss  11918  fisumss  11919  fsumadd  11933  isumclim3  11950  fsummulc2  11975  fsumsub  11979  telfsumo  11993  telfsumo2  11994  hashiun  12005  bcxmas  12016  isumshft  12017  trireciplem  12027  geoserap  12034  geo2sum2  12042  fprodf1o  12115  prodssdc  12116  fprodssdc  12117  fprodmul  12118  fprodm1  12125  sinsub  12267  cossub  12268  p1modz1  12321  bitsinv1lem  12488  bitsinv1  12489  gcdaddm  12521  modgcd  12528  bezoutlemnewy  12533  absmulgcd  12554  gcdmultiplez  12558  eucalg  12597  lcmgcd  12616  lcmid  12618  numdensq  12740  dfphi2  12758  phiprm  12761  fermltl  12772  prmdiveq  12774  hashgcdlem  12776  odzdvds  12784  powm2modprm  12791  modprm0  12793  coprimeprodsq  12796  pythagtriplem6  12809  pythagtriplem7  12810  pythagtriplem12  12814  pythagtriplem14  12816  pythagtriplem16  12818  pcaddlem  12878  sumhashdc  12886  fldivp1  12887  pcfac  12889  pockthlem  12895  4sqlem12  12941  4sqlem15  12944  ennnfonelem1  12994  ennnfonelemex  13001  topnpropgd  13302  qusaddvallemg  13382  grpinvalem  13434  grpinva  13435  grprida  13436  mnd12g  13477  resmhm  13536  grprcan  13586  grplcan  13611  grpasscan1  13612  grpinv11  13618  grpinvnz  13620  grplmulf1o  13623  grpinvpropdg  13624  grpinvadd  13627  grpsubsub4  13642  dfgrp3m  13648  imasgrp2  13663  mhmid  13668  mhmmnd  13669  mulgz  13703  mulgdirlem  13706  mulgdir  13707  mulgass  13712  mulgsubdir  13715  mulgpropdg  13717  isnsg3  13760  nmzsubg  13763  ssnmz  13764  eqger  13777  eqglact  13778  ghminv  13803  conjnmz  13832  ghmcmn  13880  gsumfzconst  13894  gsumfzmhm2  13897  rnglz  13924  rngrz  13925  isrngd  13932  ringcom  14010  crngpropd  14018  isringd  14020  ringlz  14022  ringrz  14023  ring1eq0  14027  ringmneg1  14032  mulgass3  14064  unitgrp  14096  rngidpropdg  14126  invrpropdg  14129  isrhm2d  14145  rhmunitinv  14158  subrngpropd  14196  subrginv  14217  subrgunit  14219  subrgpropd  14233  rhmpropd  14234  unitrrg  14247  lmodvs0  14302  lmodvneg1  14310  lmodcom  14313  lmodsubdi  14324  lss0v  14410  lidlrsppropdg  14475  mulgrhm2  14590  znidomb  14638  restin  14866  blpnfctr  15129  xmssym  15159  limcimolemlt  15354  dvmulxxbr  15392  dvrecap  15403  dvmptaddx  15409  dvmptmulx  15410  dvmptnegcn  15412  dvmptsubcn  15413  dvmptcjx  15414  dveflem  15416  plymullem1  15438  dvply1  15455  sin0pilem1  15471  ptolemy  15514  tangtx  15528  rpcxpneg  15597  rpcxpsub  15598  cxprec  15600  rpcxproot  15604  cxpcom  15628  rpabscxpbnd  15630  wilthlem1  15670  sgmppw  15682  1sgmprm  15684  1sgm2ppw  15685  perfectlem1  15689  perfectlem2  15690  lgsvalmod  15714  lgsneg  15719  lgsdilem  15722  lgsne0  15733  lgssq  15735  lgssq2  15736  gausslemma2dlem1f1o  15755  gausslemma2dlem6  15762  gausslemma2d  15764  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem4  15768  lgsquadlem1  15772  lgsquadlem3  15774  lgsquad3  15779  m1lgs  15780  peano4nninf  16460  nninfalllem1  16462  nninfall  16463  nninfsellemqall  16469  qdencn  16483