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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  mpteqb  5737  fvmptt  5738  fsnunfv  5854  f1ocnvfv1  5917  f1ocnvfv2  5918  fcof1  5923  caov12d  6203  caov13d  6205  caov411d  6207  caovimo  6215  tfrlem5  6479  tfrlemiubacc  6495  tfr1onlemubacc  6511  tfrcllemubacc  6524  nndir  6657  en2  6997  fopwdom  7021  updjud  7280  omp1eomlem  7292  addassnqg  7601  distrnqg  7606  enq0tr  7653  distrnq0  7678  distnq0r  7682  addnqprl  7748  addnqpru  7749  appdivnq  7782  ltmprr  7861  addcmpblnr  7958  mulcmpblnrlemg  7959  ltsrprg  7966  1idsr  7987  pn0sr  7990  mulgt0sr  7997  map2psrprg  8024  axmulass  8092  ax0id  8097  recriota  8109  mul12  8307  mul4  8310  readdcan  8318  add12  8336  cnegexlem2  8354  addcan  8358  ppncan  8420  addsub4  8421  subeqxfrd  8541  subaddeqd  8547  muladd  8562  mulcanapd  8840  receuap  8848  div13ap  8872  divdivdivap  8892  divcanap5  8893  divdivap1  8902  divdivap2  8903  halfaddsub  9377  fztp  10312  fseq1p1m1  10328  flqzadd  10557  flqdiv  10582  mulp1mod1  10626  modqnegd  10640  modqsub12d  10642  q2submod  10646  modsumfzodifsn  10657  seq3m1  10734  seq3caopr  10756  seqcaoprg  10757  iseqf1olemab  10763  iseqf1olemnanb  10764  seq3f1olemqsumk  10773  seqf1og  10782  exprecap  10841  expsubap  10848  zesq  10919  nn0opthlem1d  10981  facnn2  10995  faclbnd6  11005  zfz1isolemsplit  11101  seq3coll  11105  ccatopth  11296  shftval3  11387  crre  11417  resub  11430  imsub  11438  cjsub  11452  bdtrilem  11799  bdtri  11800  climshft2  11866  nnf1o  11936  fsumf1o  11950  isumss  11951  fisumss  11952  fsumadd  11966  isumclim3  11983  fsummulc2  12008  fsumsub  12012  telfsumo  12026  telfsumo2  12027  hashiun  12038  bcxmas  12049  isumshft  12050  trireciplem  12060  geoserap  12067  geo2sum2  12075  fprodf1o  12148  prodssdc  12149  fprodssdc  12150  fprodmul  12151  fprodm1  12158  sinsub  12300  cossub  12301  p1modz1  12354  bitsinv1lem  12521  bitsinv1  12522  gcdaddm  12554  modgcd  12561  bezoutlemnewy  12566  absmulgcd  12587  gcdmultiplez  12591  eucalg  12630  lcmgcd  12649  lcmid  12651  numdensq  12773  dfphi2  12791  phiprm  12794  fermltl  12805  prmdiveq  12807  hashgcdlem  12809  odzdvds  12817  powm2modprm  12824  modprm0  12826  coprimeprodsq  12829  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem16  12851  pcaddlem  12911  sumhashdc  12919  fldivp1  12920  pcfac  12922  pockthlem  12928  4sqlem12  12974  4sqlem15  12977  ennnfonelem1  13027  ennnfonelemex  13034  topnpropgd  13335  qusaddvallemg  13415  grpinvalem  13467  grpinva  13468  grprida  13469  mnd12g  13510  resmhm  13569  grprcan  13619  grplcan  13644  grpasscan1  13645  grpinv11  13651  grpinvnz  13653  grplmulf1o  13656  grpinvpropdg  13657  grpinvadd  13660  grpsubsub4  13675  dfgrp3m  13681  imasgrp2  13696  mhmid  13701  mhmmnd  13702  mulgz  13736  mulgdirlem  13739  mulgdir  13740  mulgass  13745  mulgsubdir  13748  mulgpropdg  13750  isnsg3  13793  nmzsubg  13796  ssnmz  13797  eqger  13810  eqglact  13811  ghminv  13836  conjnmz  13865  ghmcmn  13913  gsumfzconst  13927  gsumfzmhm2  13930  rnglz  13957  rngrz  13958  isrngd  13965  ringcom  14043  crngpropd  14051  isringd  14053  ringlz  14055  ringrz  14056  ring1eq0  14060  ringmneg1  14065  mulgass3  14097  unitgrp  14129  rngidpropdg  14159  invrpropdg  14162  isrhm2d  14178  rhmunitinv  14191  subrngpropd  14229  subrginv  14250  subrgunit  14252  subrgpropd  14266  rhmpropd  14267  unitrrg  14280  lmodvs0  14335  lmodvneg1  14343  lmodcom  14346  lmodsubdi  14357  lss0v  14443  lidlrsppropdg  14508  mulgrhm2  14623  znidomb  14671  restin  14899  blpnfctr  15162  xmssym  15192  limcimolemlt  15387  dvmulxxbr  15425  dvrecap  15436  dvmptaddx  15442  dvmptmulx  15443  dvmptnegcn  15445  dvmptsubcn  15446  dvmptcjx  15447  dveflem  15449  plymullem1  15471  dvply1  15488  sin0pilem1  15504  ptolemy  15547  tangtx  15561  rpcxpneg  15630  rpcxpsub  15631  cxprec  15633  rpcxproot  15637  cxpcom  15661  rpabscxpbnd  15663  wilthlem1  15703  sgmppw  15715  1sgmprm  15717  1sgm2ppw  15718  perfectlem1  15722  perfectlem2  15723  lgsvalmod  15747  lgsneg  15752  lgsdilem  15755  lgsne0  15766  lgssq  15768  lgssq2  15769  gausslemma2dlem1f1o  15788  gausslemma2dlem6  15795  gausslemma2d  15797  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem4  15801  lgsquadlem1  15805  lgsquadlem3  15807  lgsquad3  15812  m1lgs  15813  p1evtxdeqfilem  16161  peano4nninf  16608  nninfalllem1  16610  nninfall  16611  nninfsellemqall  16617  qdencn  16631