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  5799  fvmptt  5800  fsnunfv  5919  f1ocnvfv1  5986  f1ocnvfv2  5987  fcof1  5992  caov12d  6274  caov13d  6276  caov411d  6278  caovimo  6286  tfrlem5  6589  tfrlemiubacc  6605  tfr1onlemubacc  6621  tfrcllemubacc  6634  nndir  6767  en2  7116  fopwdom  7140  updjud  7428  omp1eomlem  7440  addassnqg  7755  distrnqg  7760  enq0tr  7807  distrnq0  7832  distnq0r  7836  addnqprl  7902  addnqpru  7903  appdivnq  7936  ltmprr  8015  addcmpblnr  8112  mulcmpblnrlemg  8113  ltsrprg  8120  1idsr  8141  pn0sr  8144  mulgt0sr  8151  map2psrprg  8178  axmulass  8246  ax0id  8251  recriota  8263  mul12  8462  mul4  8465  readdcan  8473  add12  8491  cnegexlem2  8509  addcan  8513  ppncan  8575  addsub4  8576  subeqxfrd  8696  subaddeqd  8702  muladd  8718  mulcanapd  8997  receuap  9007  div13ap  9031  divdivdivap  9051  divcanap5  9052  divdivap1  9061  divdivap2  9062  halfaddsub  9550  lincmble  10423  fztp  10502  fseq1p1m1  10518  flqzadd  10754  flqdiv  10779  mulp1mod1  10823  modqnegd  10837  modqsub12d  10839  q2submod  10843  modsumfzodifsn  10854  seq3m1  10931  seq3caopr  10953  seqcaoprg  10954  iseqf1olemab  10960  iseqf1olemnanb  10961  seq3f1olemqsumk  10970  seqf1og  10979  exprecap  11038  expsubap  11045  zesq  11117  nn0opthlem1d  11180  facnn2  11194  faclbnd6  11204  bcm1n  11229  hashfibclem  11304  hashfac  11310  zfz1isolemsplit  11312  seq3coll  11316  ccatopth  11510  shftval3  11614  crre  11644  resub  11657  imsub  11665  cjsub  11679  sq01  11682  bdtrilem  12030  bdtri  12031  climshft2  12097  nnf1o  12168  fsumf1o  12182  isumss  12183  fisumss  12184  fsumadd  12198  isumclim3  12215  fsummulc2  12240  fsumsub  12244  telfsumo  12258  telfsumo2  12259  hashiun  12270  bcxmas  12281  isumshft  12282  trireciplem  12292  geoserap  12299  geo2sum2  12307  fprodf1o  12380  prodssdc  12381  fprodssdc  12382  fprodmul  12383  fprodm1  12390  sinsub  12532  cossub  12533  p1modz1  12586  bitsinv1lem  12753  bitsinv1  12754  gcdaddm  12786  modgcd  12793  bezoutlemnewy  12798  absmulgcd  12819  gcdmultiplez  12823  eucalg  12862  lcmgcd  12881  lcmid  12883  numdensq  13007  dfphi2  13027  phiprm  13030  fermltl  13041  prmdiveq  13043  hashgcdlem  13045  odzdvds  13053  powm2modprm  13060  modprm0  13062  coprimeprodsq  13065  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem12  13083  pythagtriplem14  13085  pythagtriplem16  13087  pcaddlem  13147  sumhashdc  13155  fldivp1  13156  pcfac  13158  pockthlem  13164  4sqlem12  13210  4sqlem15  13213  ennnfonelem1  13356  ennnfonelemex  13363  topnpropgd  13666  qusaddvallemg  13713  grpinvalem  13764  grpinva  13765  grprida  13766  mnd12g  13800  resmhm  13853  grprcan  13901  grplcan  13926  grpasscan1  13927  grpinv11  13933  grpinvnz  13935  grplmulf1o  13938  grpinvpropdg  13939  grpinvadd  13942  grpsubsub4  13957  dfgrp3m  13963  imasgrp2  13972  mhmid  13977  mhmmnd  13978  mulgz  14012  mulgdirlem  14015  mulgdir  14016  mulgass  14021  mulgsubdir  14024  mulgpropdg  14026  isnsg3  14069  nmzsubg  14072  ssnmz  14073  eqger  14086  eqglact  14087  ghminv  14112  conjnmz  14141  cntzsubg  14171  cntzmhm  14173  ghmcmn  14221  gzsumconst  14233  gzsummhm2  14236  gsummhm2fi  14265  rnglz  14351  rngrz  14352  isrngd  14359  ringcom  14443  crngpropd  14451  isringd  14453  ringlz  14455  ringrz  14456  ring1eq0  14460  ringmneg1  14465  mulgass3  14500  unitgrp  14532  rngidpropdg  14562  invrpropdg  14565  isrhm2d  14581  rhmunitinv  14594  subrngpropd  14633  subrginv  14654  subrgunit  14656  subrgpropd  14670  rhmpropd  14671  unitrrg  14685  aprlring  14709  lmodvs0  14768  lmodvneg1  14776  lmodcom  14779  lmodsubdi  14790  lss0v  14876  lidlrsppropdg  14941  mulgrhm2  15054  znidomb  15102  asclpropd  15149  psrass1filem  15177  psrlidmfi  15199  psrridmfi  15200  restin  15402  blpnfctr  15665  xmssym  15695  limcimolemlt  15890  dvmulxxbr  15928  dvrecap  15939  dvmptaddx  15945  dvmptmulx  15946  dvmptnegcn  15948  dvmptsubcn  15949  dvmptcjx  15950  dveflem  15952  plymullem1  15974  dvply1  15991  sin0pilem1  16008  ptolemy  16051  tangtx  16065  rpcxpneg  16140  rpcxpsub  16141  cxprec  16143  rpcxproot  16147  cxpcom  16173  rpabscxpbnd  16175  efnthr  16176  zprmlogbaplem3  16217  pellexlem2  16230  wilthlem1  16232  sgmppw  16286  1sgmprm  16288  1sgm2ppw  16289  ppiqub  16293  perfectlem1  16299  perfectlem2  16300  bposlem6  16316  bposlem9  16319  lgsvalmod  16343  lgsneg  16348  lgsdilem  16351  lgsne0  16362  lgssq  16364  lgssq2  16365  gausslemma2dlem1f1o  16384  gausslemma2dlem6  16391  gausslemma2d  16393  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem4  16397  lgsquadlem1  16401  lgsquadlem3  16403  lgsquad3  16408  m1lgs  16409  p1evtxdeqfilem  16757  peano4nninf  17255  nninfalllem1  17257  nninfall  17258  nninfsellemqall  17264  qdencn  17278  qdiff  17305