Theorem 3eqtr3d 2272

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 2266	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	eqtr3d 2266	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  mpteqb  5746  fvmptt  5747  fsnunfv  5863  f1ocnvfv1  5928  f1ocnvfv2  5929  fcof1  5934  caov12d  6214  caov13d  6216  caov411d  6218  caovimo  6226  tfrlem5  6523  tfrlemiubacc  6539  tfr1onlemubacc  6555  tfrcllemubacc  6568  nndir  6701  en2  7041  fopwdom  7065  updjud  7324  omp1eomlem  7336  addassnqg  7645  distrnqg  7650  enq0tr  7697  distrnq0  7722  distnq0r  7726  addnqprl  7792  addnqpru  7793  appdivnq  7826  ltmprr  7905  addcmpblnr  8002  mulcmpblnrlemg  8003  ltsrprg  8010  1idsr  8031  pn0sr  8034  mulgt0sr  8041  map2psrprg  8068  axmulass  8136  ax0id  8141  recriota  8153  mul12  8350  mul4  8353  readdcan  8361  add12  8379  cnegexlem2  8397  addcan  8401  ppncan  8463  addsub4  8464  subeqxfrd  8584  subaddeqd  8590  muladd  8605  mulcanapd  8883  receuap  8891  div13ap  8915  divdivdivap  8935  divcanap5  8936  divdivap1  8945  divdivap2  8946  halfaddsub  9420  lincmble  10283  fztp  10358  fseq1p1m1  10374  flqzadd  10604  flqdiv  10629  mulp1mod1  10673  modqnegd  10687  modqsub12d  10689  q2submod  10693  modsumfzodifsn  10704  seq3m1  10781  seq3caopr  10803  seqcaoprg  10804  iseqf1olemab  10810  iseqf1olemnanb  10811  seq3f1olemqsumk  10820  seqf1og  10829  exprecap  10888  expsubap  10895  zesq  10966  nn0opthlem1d  11028  facnn2  11042  faclbnd6  11052  zfz1isolemsplit  11148  seq3coll  11152  ccatopth  11346  shftval3  11450  crre  11480  resub  11493  imsub  11501  cjsub  11515  bdtrilem  11862  bdtri  11863  climshft2  11929  nnf1o  12000  fsumf1o  12014  isumss  12015  fisumss  12016  fsumadd  12030  isumclim3  12047  fsummulc2  12072  fsumsub  12076  telfsumo  12090  telfsumo2  12091  hashiun  12102  bcxmas  12113  isumshft  12114  trireciplem  12124  geoserap  12131  geo2sum2  12139  fprodf1o  12212  prodssdc  12213  fprodssdc  12214  fprodmul  12215  fprodm1  12222  sinsub  12364  cossub  12365  p1modz1  12418  bitsinv1lem  12585  bitsinv1  12586  gcdaddm  12618  modgcd  12625  bezoutlemnewy  12630  absmulgcd  12651  gcdmultiplez  12655  eucalg  12694  lcmgcd  12713  lcmid  12715  numdensq  12837  dfphi2  12855  phiprm  12858  fermltl  12869  prmdiveq  12871  hashgcdlem  12873  odzdvds  12881  powm2modprm  12888  modprm0  12890  coprimeprodsq  12893  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem16  12915  pcaddlem  12975  sumhashdc  12983  fldivp1  12984  pcfac  12986  pockthlem  12992  4sqlem12  13038  4sqlem15  13041  ennnfonelem1  13091  ennnfonelemex  13098  topnpropgd  13399  qusaddvallemg  13479  grpinvalem  13531  grpinva  13532  grprida  13533  mnd12g  13574  resmhm  13633  grprcan  13683  grplcan  13708  grpasscan1  13709  grpinv11  13715  grpinvnz  13717  grplmulf1o  13720  grpinvpropdg  13721  grpinvadd  13724  grpsubsub4  13739  dfgrp3m  13745  imasgrp2  13760  mhmid  13765  mhmmnd  13766  mulgz  13800  mulgdirlem  13803  mulgdir  13804  mulgass  13809  mulgsubdir  13812  mulgpropdg  13814  isnsg3  13857  nmzsubg  13860  ssnmz  13861  eqger  13874  eqglact  13875  ghminv  13900  conjnmz  13929  ghmcmn  13977  gsumfzconst  13991  gsumfzmhm2  13994  rnglz  14022  rngrz  14023  isrngd  14030  ringcom  14108  crngpropd  14116  isringd  14118  ringlz  14120  ringrz  14121  ring1eq0  14125  ringmneg1  14130  mulgass3  14162  unitgrp  14194  rngidpropdg  14224  invrpropdg  14227  isrhm2d  14243  rhmunitinv  14256  subrngpropd  14294  subrginv  14315  subrgunit  14317  subrgpropd  14331  rhmpropd  14332  unitrrg  14346  lmodvs0  14401  lmodvneg1  14409  lmodcom  14412  lmodsubdi  14423  lss0v  14509  lidlrsppropdg  14574  mulgrhm2  14689  znidomb  14737  restin  14970  blpnfctr  15233  xmssym  15263  limcimolemlt  15458  dvmulxxbr  15496  dvrecap  15507  dvmptaddx  15513  dvmptmulx  15514  dvmptnegcn  15516  dvmptsubcn  15517  dvmptcjx  15518  dveflem  15520  plymullem1  15542  dvply1  15559  sin0pilem1  15575  ptolemy  15618  tangtx  15632  rpcxpneg  15701  rpcxpsub  15702  cxprec  15704  rpcxproot  15708  cxpcom  15732  rpabscxpbnd  15734  pellexlem2  15775  wilthlem1  15777  sgmppw  15789  1sgmprm  15791  1sgm2ppw  15792  perfectlem1  15796  perfectlem2  15797  lgsvalmod  15821  lgsneg  15826  lgsdilem  15829  lgsne0  15840  lgssq  15842  lgssq2  15843  gausslemma2dlem1f1o  15862  gausslemma2dlem6  15869  gausslemma2d  15871  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem4  15875  lgsquadlem1  15879  lgsquadlem3  15881  lgsquad3  15886  m1lgs  15887  p1evtxdeqfilem  16235  peano4nninf  16715  nninfalllem1  16717  nninfall  16718  nninfsellemqall  16724  qdencn  16738  qdiff  16764