Theorem 3eqtr3d 2247

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  mpteqb  5682  fvmptt  5683  fsnunfv  5797  f1ocnvfv1  5858  f1ocnvfv2  5859  fcof1  5864  caov12d  6140  caov13d  6142  caov411d  6144  caovimo  6152  tfrlem5  6412  tfrlemiubacc  6428  tfr1onlemubacc  6444  tfrcllemubacc  6457  nndir  6588  en2  6925  fopwdom  6947  updjud  7198  omp1eomlem  7210  addassnqg  7510  distrnqg  7515  enq0tr  7562  distrnq0  7587  distnq0r  7591  addnqprl  7657  addnqpru  7658  appdivnq  7691  ltmprr  7770  addcmpblnr  7867  mulcmpblnrlemg  7868  ltsrprg  7875  1idsr  7896  pn0sr  7899  mulgt0sr  7906  map2psrprg  7933  axmulass  8001  ax0id  8006  recriota  8018  mul12  8216  mul4  8219  readdcan  8227  add12  8245  cnegexlem2  8263  addcan  8267  ppncan  8329  addsub4  8330  subeqxfrd  8450  subaddeqd  8456  muladd  8471  mulcanapd  8749  receuap  8757  div13ap  8781  divdivdivap  8801  divcanap5  8802  divdivap1  8811  divdivap2  8812  halfaddsub  9286  fztp  10215  fseq1p1m1  10231  flqzadd  10458  flqdiv  10483  mulp1mod1  10527  modqnegd  10541  modqsub12d  10543  q2submod  10547  modsumfzodifsn  10558  seq3m1  10635  seq3caopr  10657  seqcaoprg  10658  iseqf1olemab  10664  iseqf1olemnanb  10665  seq3f1olemqsumk  10674  seqf1og  10683  exprecap  10742  expsubap  10749  zesq  10820  nn0opthlem1d  10882  facnn2  10896  faclbnd6  10906  zfz1isolemsplit  11000  seq3coll  11004  ccatopth  11187  shftval3  11208  crre  11238  resub  11251  imsub  11259  cjsub  11273  bdtrilem  11620  bdtri  11621  climshft2  11687  nnf1o  11757  fsumf1o  11771  isumss  11772  fisumss  11773  fsumadd  11787  isumclim3  11804  fsummulc2  11829  fsumsub  11833  telfsumo  11847  telfsumo2  11848  hashiun  11859  bcxmas  11870  isumshft  11871  trireciplem  11881  geoserap  11888  geo2sum2  11896  fprodf1o  11969  prodssdc  11970  fprodssdc  11971  fprodmul  11972  fprodm1  11979  sinsub  12121  cossub  12122  p1modz1  12175  bitsinv1lem  12342  bitsinv1  12343  gcdaddm  12375  modgcd  12382  bezoutlemnewy  12387  absmulgcd  12408  gcdmultiplez  12412  eucalg  12451  lcmgcd  12470  lcmid  12472  numdensq  12594  dfphi2  12612  phiprm  12615  fermltl  12626  prmdiveq  12628  hashgcdlem  12630  odzdvds  12638  powm2modprm  12645  modprm0  12647  coprimeprodsq  12650  pythagtriplem6  12663  pythagtriplem7  12664  pythagtriplem12  12668  pythagtriplem14  12670  pythagtriplem16  12672  pcaddlem  12732  sumhashdc  12740  fldivp1  12741  pcfac  12743  pockthlem  12749  4sqlem12  12795  4sqlem15  12798  ennnfonelem1  12848  ennnfonelemex  12855  topnpropgd  13155  qusaddvallemg  13235  grpinvalem  13287  grpinva  13288  grprida  13289  mnd12g  13330  resmhm  13389  grprcan  13439  grplcan  13464  grpasscan1  13465  grpinv11  13471  grpinvnz  13473  grplmulf1o  13476  grpinvpropdg  13477  grpinvadd  13480  grpsubsub4  13495  dfgrp3m  13501  imasgrp2  13516  mhmid  13521  mhmmnd  13522  mulgz  13556  mulgdirlem  13559  mulgdir  13560  mulgass  13565  mulgsubdir  13568  mulgpropdg  13570  isnsg3  13613  nmzsubg  13616  ssnmz  13617  eqger  13630  eqglact  13631  ghminv  13656  conjnmz  13685  ghmcmn  13733  gsumfzconst  13747  gsumfzmhm2  13750  rnglz  13777  rngrz  13778  isrngd  13785  ringcom  13863  crngpropd  13871  isringd  13873  ringlz  13875  ringrz  13876  ring1eq0  13880  ringmneg1  13885  mulgass3  13917  unitgrp  13948  rngidpropdg  13978  invrpropdg  13981  isrhm2d  13997  rhmunitinv  14010  subrngpropd  14048  subrginv  14069  subrgunit  14071  subrgpropd  14085  rhmpropd  14086  unitrrg  14099  lmodvs0  14154  lmodvneg1  14162  lmodcom  14165  lmodsubdi  14176  lss0v  14262  lidlrsppropdg  14327  mulgrhm2  14442  znidomb  14490  restin  14718  blpnfctr  14981  xmssym  15011  limcimolemlt  15206  dvmulxxbr  15244  dvrecap  15255  dvmptaddx  15261  dvmptmulx  15262  dvmptnegcn  15264  dvmptsubcn  15265  dvmptcjx  15266  dveflem  15268  plymullem1  15290  dvply1  15307  sin0pilem1  15323  ptolemy  15366  tangtx  15380  rpcxpneg  15449  rpcxpsub  15450  cxprec  15452  rpcxproot  15456  cxpcom  15480  rpabscxpbnd  15482  wilthlem1  15522  sgmppw  15534  1sgmprm  15536  1sgm2ppw  15537  perfectlem1  15541  perfectlem2  15542  lgsvalmod  15566  lgsneg  15571  lgsdilem  15574  lgsne0  15585  lgssq  15587  lgssq2  15588  gausslemma2dlem1f1o  15607  gausslemma2dlem6  15614  gausslemma2d  15616  lgseisenlem1  15617  lgseisenlem2  15618  lgseisenlem4  15620  lgsquadlem1  15624  lgsquadlem3  15626  lgsquad3  15631  m1lgs  15632  peano4nninf  16078  nninfalllem1  16080  nninfall  16081  nninfsellemqall  16087  qdencn  16101