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  5652  fvmptt  5653  fsnunfv  5763  f1ocnvfv1  5824  f1ocnvfv2  5825  fcof1  5830  caov12d  6105  caov13d  6107  caov411d  6109  caovimo  6117  tfrlem5  6372  tfrlemiubacc  6388  tfr1onlemubacc  6404  tfrcllemubacc  6417  nndir  6548  fopwdom  6897  updjud  7148  omp1eomlem  7160  addassnqg  7449  distrnqg  7454  enq0tr  7501  distrnq0  7526  distnq0r  7530  addnqprl  7596  addnqpru  7597  appdivnq  7630  ltmprr  7709  addcmpblnr  7806  mulcmpblnrlemg  7807  ltsrprg  7814  1idsr  7835  pn0sr  7838  mulgt0sr  7845  map2psrprg  7872  axmulass  7940  ax0id  7945  recriota  7957  mul12  8155  mul4  8158  readdcan  8166  add12  8184  cnegexlem2  8202  addcan  8206  ppncan  8268  addsub4  8269  subeqxfrd  8389  subaddeqd  8395  muladd  8410  mulcanapd  8688  receuap  8696  div13ap  8720  divdivdivap  8740  divcanap5  8741  divdivap1  8750  divdivap2  8751  halfaddsub  9225  fztp  10153  fseq1p1m1  10169  flqzadd  10388  flqdiv  10413  mulp1mod1  10457  modqnegd  10471  modqsub12d  10473  q2submod  10477  modsumfzodifsn  10488  seq3m1  10565  seq3caopr  10587  seqcaoprg  10588  iseqf1olemab  10594  iseqf1olemnanb  10595  seq3f1olemqsumk  10604  seqf1og  10613  exprecap  10672  expsubap  10679  zesq  10750  nn0opthlem1d  10812  facnn2  10826  faclbnd6  10836  zfz1isolemsplit  10930  seq3coll  10934  shftval3  10992  crre  11022  resub  11035  imsub  11043  cjsub  11057  bdtrilem  11404  bdtri  11405  climshft2  11471  nnf1o  11541  fsumf1o  11555  isumss  11556  fisumss  11557  fsumadd  11571  isumclim3  11588  fsummulc2  11613  fsumsub  11617  telfsumo  11631  telfsumo2  11632  hashiun  11643  bcxmas  11654  isumshft  11655  trireciplem  11665  geoserap  11672  geo2sum2  11680  fprodf1o  11753  prodssdc  11754  fprodssdc  11755  fprodmul  11756  fprodm1  11763  sinsub  11905  cossub  11906  p1modz1  11959  gcdaddm  12151  modgcd  12158  bezoutlemnewy  12163  absmulgcd  12184  gcdmultiplez  12188  eucalg  12227  lcmgcd  12246  lcmid  12248  numdensq  12370  dfphi2  12388  phiprm  12391  fermltl  12402  prmdiveq  12404  hashgcdlem  12406  odzdvds  12414  powm2modprm  12421  modprm0  12423  coprimeprodsq  12426  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem16  12448  pcaddlem  12508  sumhashdc  12516  fldivp1  12517  pcfac  12519  pockthlem  12525  4sqlem12  12571  4sqlem15  12574  ennnfonelem1  12624  ennnfonelemex  12631  topnpropgd  12924  qusaddvallemg  12976  grpinvalem  13028  grpinva  13029  grprida  13030  mnd12g  13069  resmhm  13119  grprcan  13169  grplcan  13194  grpasscan1  13195  grpinv11  13201  grpinvnz  13203  grplmulf1o  13206  grpinvpropdg  13207  grpinvadd  13210  grpsubsub4  13225  dfgrp3m  13231  imasgrp2  13240  mhmid  13245  mhmmnd  13246  mulgz  13280  mulgdirlem  13283  mulgdir  13284  mulgass  13289  mulgsubdir  13292  mulgpropdg  13294  isnsg3  13337  nmzsubg  13340  ssnmz  13341  eqger  13354  eqglact  13355  ghminv  13380  conjnmz  13409  ghmcmn  13457  gsumfzconst  13471  gsumfzmhm2  13474  rnglz  13501  rngrz  13502  isrngd  13509  ringcom  13587  crngpropd  13595  isringd  13597  ringlz  13599  ringrz  13600  ring1eq0  13604  ringmneg1  13609  mulgass3  13641  unitgrp  13672  rngidpropdg  13702  invrpropdg  13705  isrhm2d  13721  rhmunitinv  13734  subrngpropd  13772  subrginv  13793  subrgunit  13795  subrgpropd  13809  rhmpropd  13810  unitrrg  13823  lmodvs0  13878  lmodvneg1  13886  lmodcom  13889  lmodsubdi  13900  lss0v  13986  lidlrsppropdg  14051  mulgrhm2  14166  znidomb  14214  restin  14412  blpnfctr  14675  xmssym  14705  limcimolemlt  14900  dvmulxxbr  14938  dvrecap  14949  dvmptaddx  14955  dvmptmulx  14956  dvmptnegcn  14958  dvmptsubcn  14959  dvmptcjx  14960  dveflem  14962  plymullem1  14984  dvply1  15001  sin0pilem1  15017  ptolemy  15060  tangtx  15074  rpcxpneg  15143  rpcxpsub  15144  cxprec  15146  rpcxproot  15150  cxpcom  15174  rpabscxpbnd  15176  wilthlem1  15216  sgmppw  15228  1sgmprm  15230  1sgm2ppw  15231  perfectlem1  15235  perfectlem2  15236  lgsvalmod  15260  lgsneg  15265  lgsdilem  15268  lgsne0  15279  lgssq  15281  lgssq2  15282  gausslemma2dlem1f1o  15301  gausslemma2dlem6  15308  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem4  15314  lgsquadlem1  15318  lgsquadlem3  15320  lgsquad3  15325  m1lgs  15326  peano4nninf  15650  nninfalllem1  15652  nninfall  15653  nninfsellemqall  15659  qdencn  15671