Theorem 3eqtr3d 2218

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  mpteqb  5608  fvmptt  5609  fsnunfv  5719  f1ocnvfv1  5780  f1ocnvfv2  5781  fcof1  5786  caov12d  6058  caov13d  6060  caov411d  6062  caovimo  6070  tfrlem5  6317  tfrlemiubacc  6333  tfr1onlemubacc  6349  tfrcllemubacc  6362  nndir  6493  fopwdom  6838  updjud  7083  omp1eomlem  7095  addassnqg  7383  distrnqg  7388  enq0tr  7435  distrnq0  7460  distnq0r  7464  addnqprl  7530  addnqpru  7531  appdivnq  7564  ltmprr  7643  addcmpblnr  7740  mulcmpblnrlemg  7741  ltsrprg  7748  1idsr  7769  pn0sr  7772  mulgt0sr  7779  map2psrprg  7806  axmulass  7874  ax0id  7879  recriota  7891  mul12  8088  mul4  8091  readdcan  8099  add12  8117  cnegexlem2  8135  addcan  8139  ppncan  8201  addsub4  8202  subeqxfrd  8322  subaddeqd  8328  muladd  8343  mulcanapd  8620  receuap  8628  div13ap  8652  divdivdivap  8672  divcanap5  8673  divdivap1  8682  divdivap2  8683  halfaddsub  9155  fztp  10080  fseq1p1m1  10096  flqzadd  10300  flqdiv  10323  mulp1mod1  10367  modqnegd  10381  modqsub12d  10383  q2submod  10387  modsumfzodifsn  10398  seq3m1  10470  seq3caopr  10485  iseqf1olemab  10491  iseqf1olemnanb  10492  seq3f1olemqsumk  10501  exprecap  10563  expsubap  10570  zesq  10641  nn0opthlem1d  10702  facnn2  10716  faclbnd6  10726  zfz1isolemsplit  10820  seq3coll  10824  shftval3  10838  crre  10868  resub  10881  imsub  10889  cjsub  10903  bdtrilem  11249  bdtri  11250  climshft2  11316  nnf1o  11386  fsumf1o  11400  isumss  11401  fisumss  11402  fsumadd  11416  isumclim3  11433  fsummulc2  11458  fsumsub  11462  telfsumo  11476  telfsumo2  11477  hashiun  11488  bcxmas  11499  isumshft  11500  trireciplem  11510  geoserap  11517  geo2sum2  11525  fprodf1o  11598  prodssdc  11599  fprodssdc  11600  fprodmul  11601  fprodm1  11608  sinsub  11750  cossub  11751  p1modz1  11803  gcdaddm  11987  modgcd  11994  bezoutlemnewy  11999  absmulgcd  12020  gcdmultiplez  12024  eucalg  12061  lcmgcd  12080  lcmid  12082  numdensq  12204  dfphi2  12222  phiprm  12225  fermltl  12236  prmdiveq  12238  hashgcdlem  12240  odzdvds  12247  powm2modprm  12254  modprm0  12256  coprimeprodsq  12259  pythagtriplem6  12272  pythagtriplem7  12273  pythagtriplem12  12277  pythagtriplem14  12279  pythagtriplem16  12281  pcaddlem  12340  sumhashdc  12347  fldivp1  12348  pcfac  12350  pockthlem  12356  ennnfonelem1  12410  ennnfonelemex  12417  topnpropgd  12707  qusaddvallemg  12757  grprinvlem  12809  grprinvd  12810  grpridd  12811  mnd12g  12834  grprcan  12915  grplcan  12937  grpasscan1  12938  grpinv11  12944  grpinvnz  12946  grplmulf1o  12949  grpinvpropdg  12950  grpinvadd  12953  grpsubsub4  12968  dfgrp3m  12974  mhmid  12984  mhmmnd  12985  mulgz  13016  mulgdirlem  13019  mulgdir  13020  mulgass  13025  mulgsubdir  13028  mulgpropdg  13030  isnsg3  13072  nmzsubg  13075  ssnmz  13076  eqger  13088  eqglact  13089  ringcom  13219  crngpropd  13223  isringd  13225  ringlz  13227  ringrz  13228  ring1eq0  13230  ringmneg1  13235  mulgass3  13259  unitgrp  13290  rngidpropdg  13320  invrpropdg  13323  subrginv  13363  subrgunit  13365  subrgpropd  13374  lmodvs0  13417  lmodvneg1  13425  lmodcom  13428  lmodsubdi  13439  restin  13715  blpnfctr  13978  xmssym  14008  limcimolemlt  14172  dvmulxxbr  14205  dvrecap  14216  dvmptaddx  14220  dvmptmulx  14221  dvmptnegcn  14223  dvmptsubcn  14224  dvmptcjx  14225  dveflem  14226  sin0pilem1  14241  ptolemy  14284  tangtx  14298  rpcxpneg  14367  rpcxpsub  14368  cxprec  14370  rpcxproot  14373  cxpcom  14396  rpabscxpbnd  14398  lgsvalmod  14459  lgsneg  14464  lgsdilem  14467  lgsne0  14478  lgssq  14480  lgssq2  14481  lgseisenlem1  14489  lgseisenlem2  14490  m1lgs  14491  peano4nninf  14794  nninfalllem1  14796  nninfall  14797  nninfsellemqall  14803  qdencn  14814