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	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3d	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr3d

Step	Hyp	Ref	Expression
1		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3	1, 2	eqtr3d 2264	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	eqtr3d 2264	1 ⊢ (𝜑 → 𝐶 = 𝐷)

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  5733  fvmptt  5734  fsnunfv  5850  f1ocnvfv1  5913  f1ocnvfv2  5914  fcof1  5919  caov12d  6199  caov13d  6201  caov411d  6203  caovimo  6211  tfrlem5  6475  tfrlemiubacc  6491  tfr1onlemubacc  6507  tfrcllemubacc  6520  nndir  6653  en2  6993  fopwdom  7017  updjud  7272  omp1eomlem  7284  addassnqg  7592  distrnqg  7597  enq0tr  7644  distrnq0  7669  distnq0r  7673  addnqprl  7739  addnqpru  7740  appdivnq  7773  ltmprr  7852  addcmpblnr  7949  mulcmpblnrlemg  7950  ltsrprg  7957  1idsr  7978  pn0sr  7981  mulgt0sr  7988  map2psrprg  8015  axmulass  8083  ax0id  8088  recriota  8100  mul12  8298  mul4  8301  readdcan  8309  add12  8327  cnegexlem2  8345  addcan  8349  ppncan  8411  addsub4  8412  subeqxfrd  8532  subaddeqd  8538  muladd  8553  mulcanapd  8831  receuap  8839  div13ap  8863  divdivdivap  8883  divcanap5  8884  divdivap1  8893  divdivap2  8894  halfaddsub  9368  fztp  10303  fseq1p1m1  10319  flqzadd  10548  flqdiv  10573  mulp1mod1  10617  modqnegd  10631  modqsub12d  10633  q2submod  10637  modsumfzodifsn  10648  seq3m1  10725  seq3caopr  10747  seqcaoprg  10748  iseqf1olemab  10754  iseqf1olemnanb  10755  seq3f1olemqsumk  10764  seqf1og  10773  exprecap  10832  expsubap  10839  zesq  10910  nn0opthlem1d  10972  facnn2  10986  faclbnd6  10996  zfz1isolemsplit  11092  seq3coll  11096  ccatopth  11287  shftval3  11378  crre  11408  resub  11421  imsub  11429  cjsub  11443  bdtrilem  11790  bdtri  11791  climshft2  11857  nnf1o  11927  fsumf1o  11941  isumss  11942  fisumss  11943  fsumadd  11957  isumclim3  11974  fsummulc2  11999  fsumsub  12003  telfsumo  12017  telfsumo2  12018  hashiun  12029  bcxmas  12040  isumshft  12041  trireciplem  12051  geoserap  12058  geo2sum2  12066  fprodf1o  12139  prodssdc  12140  fprodssdc  12141  fprodmul  12142  fprodm1  12149  sinsub  12291  cossub  12292  p1modz1  12345  bitsinv1lem  12512  bitsinv1  12513  gcdaddm  12545  modgcd  12552  bezoutlemnewy  12557  absmulgcd  12578  gcdmultiplez  12582  eucalg  12621  lcmgcd  12640  lcmid  12642  numdensq  12764  dfphi2  12782  phiprm  12785  fermltl  12796  prmdiveq  12798  hashgcdlem  12800  odzdvds  12808  powm2modprm  12815  modprm0  12817  coprimeprodsq  12820  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem16  12842  pcaddlem  12902  sumhashdc  12910  fldivp1  12911  pcfac  12913  pockthlem  12919  4sqlem12  12965  4sqlem15  12968  ennnfonelem1  13018  ennnfonelemex  13025  topnpropgd  13326  qusaddvallemg  13406  grpinvalem  13458  grpinva  13459  grprida  13460  mnd12g  13501  resmhm  13560  grprcan  13610  grplcan  13635  grpasscan1  13636  grpinv11  13642  grpinvnz  13644  grplmulf1o  13647  grpinvpropdg  13648  grpinvadd  13651  grpsubsub4  13666  dfgrp3m  13672  imasgrp2  13687  mhmid  13692  mhmmnd  13693  mulgz  13727  mulgdirlem  13730  mulgdir  13731  mulgass  13736  mulgsubdir  13739  mulgpropdg  13741  isnsg3  13784  nmzsubg  13787  ssnmz  13788  eqger  13801  eqglact  13802  ghminv  13827  conjnmz  13856  ghmcmn  13904  gsumfzconst  13918  gsumfzmhm2  13921  rnglz  13948  rngrz  13949  isrngd  13956  ringcom  14034  crngpropd  14042  isringd  14044  ringlz  14046  ringrz  14047  ring1eq0  14051  ringmneg1  14056  mulgass3  14088  unitgrp  14120  rngidpropdg  14150  invrpropdg  14153  isrhm2d  14169  rhmunitinv  14182  subrngpropd  14220  subrginv  14241  subrgunit  14243  subrgpropd  14257  rhmpropd  14258  unitrrg  14271  lmodvs0  14326  lmodvneg1  14334  lmodcom  14337  lmodsubdi  14348  lss0v  14434  lidlrsppropdg  14499  mulgrhm2  14614  znidomb  14662  restin  14890  blpnfctr  15153  xmssym  15183  limcimolemlt  15378  dvmulxxbr  15416  dvrecap  15427  dvmptaddx  15433  dvmptmulx  15434  dvmptnegcn  15436  dvmptsubcn  15437  dvmptcjx  15438  dveflem  15440  plymullem1  15462  dvply1  15479  sin0pilem1  15495  ptolemy  15538  tangtx  15552  rpcxpneg  15621  rpcxpsub  15622  cxprec  15624  rpcxproot  15628  cxpcom  15652  rpabscxpbnd  15654  wilthlem1  15694  sgmppw  15706  1sgmprm  15708  1sgm2ppw  15709  perfectlem1  15713  perfectlem2  15714  lgsvalmod  15738  lgsneg  15743  lgsdilem  15746  lgsne0  15757  lgssq  15759  lgssq2  15760  gausslemma2dlem1f1o  15779  gausslemma2dlem6  15786  gausslemma2d  15788  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem4  15792  lgsquadlem1  15796  lgsquadlem3  15798  lgsquad3  15803  m1lgs  15804  peano4nninf  16544  nninfalllem1  16546  nninfall  16547  nninfsellemqall  16553  qdencn  16567