Theorem 3eqtr3d 2234

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  mpteqb  5649  fvmptt  5650  fsnunfv  5760  f1ocnvfv1  5821  f1ocnvfv2  5822  fcof1  5827  caov12d  6102  caov13d  6104  caov411d  6106  caovimo  6114  tfrlem5  6369  tfrlemiubacc  6385  tfr1onlemubacc  6401  tfrcllemubacc  6414  nndir  6545  fopwdom  6894  updjud  7143  omp1eomlem  7155  addassnqg  7444  distrnqg  7449  enq0tr  7496  distrnq0  7521  distnq0r  7525  addnqprl  7591  addnqpru  7592  appdivnq  7625  ltmprr  7704  addcmpblnr  7801  mulcmpblnrlemg  7802  ltsrprg  7809  1idsr  7830  pn0sr  7833  mulgt0sr  7840  map2psrprg  7867  axmulass  7935  ax0id  7940  recriota  7952  mul12  8150  mul4  8153  readdcan  8161  add12  8179  cnegexlem2  8197  addcan  8201  ppncan  8263  addsub4  8264  subeqxfrd  8384  subaddeqd  8390  muladd  8405  mulcanapd  8682  receuap  8690  div13ap  8714  divdivdivap  8734  divcanap5  8735  divdivap1  8744  divdivap2  8745  halfaddsub  9219  fztp  10147  fseq1p1m1  10163  flqzadd  10370  flqdiv  10395  mulp1mod1  10439  modqnegd  10453  modqsub12d  10455  q2submod  10459  modsumfzodifsn  10470  seq3m1  10547  seq3caopr  10569  seqcaoprg  10570  iseqf1olemab  10576  iseqf1olemnanb  10577  seq3f1olemqsumk  10586  seqf1og  10595  exprecap  10654  expsubap  10661  zesq  10732  nn0opthlem1d  10794  facnn2  10808  faclbnd6  10818  zfz1isolemsplit  10912  seq3coll  10916  shftval3  10974  crre  11004  resub  11017  imsub  11025  cjsub  11039  bdtrilem  11385  bdtri  11386  climshft2  11452  nnf1o  11522  fsumf1o  11536  isumss  11537  fisumss  11538  fsumadd  11552  isumclim3  11569  fsummulc2  11594  fsumsub  11598  telfsumo  11612  telfsumo2  11613  hashiun  11624  bcxmas  11635  isumshft  11636  trireciplem  11646  geoserap  11653  geo2sum2  11661  fprodf1o  11734  prodssdc  11735  fprodssdc  11736  fprodmul  11737  fprodm1  11744  sinsub  11886  cossub  11887  p1modz1  11940  gcdaddm  12124  modgcd  12131  bezoutlemnewy  12136  absmulgcd  12157  gcdmultiplez  12161  eucalg  12200  lcmgcd  12219  lcmid  12221  numdensq  12343  dfphi2  12361  phiprm  12364  fermltl  12375  prmdiveq  12377  hashgcdlem  12379  odzdvds  12386  powm2modprm  12393  modprm0  12395  coprimeprodsq  12398  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem16  12420  pcaddlem  12480  sumhashdc  12488  fldivp1  12489  pcfac  12491  pockthlem  12497  4sqlem12  12543  4sqlem15  12546  ennnfonelem1  12567  ennnfonelemex  12574  topnpropgd  12867  qusaddvallemg  12919  grpinvalem  12971  grpinva  12972  grprida  12973  mnd12g  13012  resmhm  13062  grprcan  13112  grplcan  13137  grpasscan1  13138  grpinv11  13144  grpinvnz  13146  grplmulf1o  13149  grpinvpropdg  13150  grpinvadd  13153  grpsubsub4  13168  dfgrp3m  13174  imasgrp2  13183  mhmid  13188  mhmmnd  13189  mulgz  13223  mulgdirlem  13226  mulgdir  13227  mulgass  13232  mulgsubdir  13235  mulgpropdg  13237  isnsg3  13280  nmzsubg  13283  ssnmz  13284  eqger  13297  eqglact  13298  ghminv  13323  conjnmz  13352  ghmcmn  13400  gsumfzconst  13414  gsumfzmhm2  13417  rnglz  13444  rngrz  13445  isrngd  13452  ringcom  13530  crngpropd  13538  isringd  13540  ringlz  13542  ringrz  13543  ring1eq0  13547  ringmneg1  13552  mulgass3  13584  unitgrp  13615  rngidpropdg  13645  invrpropdg  13648  isrhm2d  13664  rhmunitinv  13677  subrngpropd  13715  subrginv  13736  subrgunit  13738  subrgpropd  13752  rhmpropd  13753  unitrrg  13766  lmodvs0  13821  lmodvneg1  13829  lmodcom  13832  lmodsubdi  13843  lss0v  13929  lidlrsppropdg  13994  mulgrhm2  14109  znidomb  14157  restin  14355  blpnfctr  14618  xmssym  14648  limcimolemlt  14843  dvmulxxbr  14881  dvrecap  14892  dvmptaddx  14898  dvmptmulx  14899  dvmptnegcn  14901  dvmptsubcn  14902  dvmptcjx  14903  dveflem  14905  plymullem1  14927  dvply1  14943  sin0pilem1  14957  ptolemy  15000  tangtx  15014  rpcxpneg  15083  rpcxpsub  15084  cxprec  15086  rpcxproot  15089  cxpcom  15112  rpabscxpbnd  15114  wilthlem1  15153  lgsvalmod  15176  lgsneg  15181  lgsdilem  15184  lgsne0  15195  lgssq  15197  lgssq2  15198  gausslemma2dlem1f1o  15217  gausslemma2dlem6  15224  gausslemma2d  15226  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem4  15230  lgsquadlem1  15234  lgsquadlem3  15236  lgsquad3  15241  m1lgs  15242  peano4nninf  15566  nninfalllem1  15568  nninfall  15569  nninfsellemqall  15575  qdencn  15587