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  5648  fvmptt  5649  fsnunfv  5759  f1ocnvfv1  5820  f1ocnvfv2  5821  fcof1  5826  caov12d  6100  caov13d  6102  caov411d  6104  caovimo  6112  tfrlem5  6367  tfrlemiubacc  6383  tfr1onlemubacc  6399  tfrcllemubacc  6412  nndir  6543  fopwdom  6892  updjud  7141  omp1eomlem  7153  addassnqg  7442  distrnqg  7447  enq0tr  7494  distrnq0  7519  distnq0r  7523  addnqprl  7589  addnqpru  7590  appdivnq  7623  ltmprr  7702  addcmpblnr  7799  mulcmpblnrlemg  7800  ltsrprg  7807  1idsr  7828  pn0sr  7831  mulgt0sr  7838  map2psrprg  7865  axmulass  7933  ax0id  7938  recriota  7950  mul12  8148  mul4  8151  readdcan  8159  add12  8177  cnegexlem2  8195  addcan  8199  ppncan  8261  addsub4  8262  subeqxfrd  8382  subaddeqd  8388  muladd  8403  mulcanapd  8680  receuap  8688  div13ap  8712  divdivdivap  8732  divcanap5  8733  divdivap1  8742  divdivap2  8743  halfaddsub  9216  fztp  10144  fseq1p1m1  10160  flqzadd  10367  flqdiv  10392  mulp1mod1  10436  modqnegd  10450  modqsub12d  10452  q2submod  10456  modsumfzodifsn  10467  seq3m1  10544  seq3caopr  10566  seqcaoprg  10567  iseqf1olemab  10573  iseqf1olemnanb  10574  seq3f1olemqsumk  10583  seqf1og  10592  exprecap  10651  expsubap  10658  zesq  10729  nn0opthlem1d  10791  facnn2  10805  faclbnd6  10815  zfz1isolemsplit  10909  seq3coll  10913  shftval3  10971  crre  11001  resub  11014  imsub  11022  cjsub  11036  bdtrilem  11382  bdtri  11383  climshft2  11449  nnf1o  11519  fsumf1o  11533  isumss  11534  fisumss  11535  fsumadd  11549  isumclim3  11566  fsummulc2  11591  fsumsub  11595  telfsumo  11609  telfsumo2  11610  hashiun  11621  bcxmas  11632  isumshft  11633  trireciplem  11643  geoserap  11650  geo2sum2  11658  fprodf1o  11731  prodssdc  11732  fprodssdc  11733  fprodmul  11734  fprodm1  11741  sinsub  11883  cossub  11884  p1modz1  11937  gcdaddm  12121  modgcd  12128  bezoutlemnewy  12133  absmulgcd  12154  gcdmultiplez  12158  eucalg  12197  lcmgcd  12216  lcmid  12218  numdensq  12340  dfphi2  12358  phiprm  12361  fermltl  12372  prmdiveq  12374  hashgcdlem  12376  odzdvds  12383  powm2modprm  12390  modprm0  12392  coprimeprodsq  12395  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem16  12417  pcaddlem  12477  sumhashdc  12485  fldivp1  12486  pcfac  12488  pockthlem  12494  4sqlem12  12540  4sqlem15  12543  ennnfonelem1  12564  ennnfonelemex  12571  topnpropgd  12864  qusaddvallemg  12916  grpinvalem  12968  grpinva  12969  grprida  12970  mnd12g  13009  resmhm  13059  grprcan  13109  grplcan  13134  grpasscan1  13135  grpinv11  13141  grpinvnz  13143  grplmulf1o  13146  grpinvpropdg  13147  grpinvadd  13150  grpsubsub4  13165  dfgrp3m  13171  imasgrp2  13180  mhmid  13185  mhmmnd  13186  mulgz  13220  mulgdirlem  13223  mulgdir  13224  mulgass  13229  mulgsubdir  13232  mulgpropdg  13234  isnsg3  13277  nmzsubg  13280  ssnmz  13281  eqger  13294  eqglact  13295  ghminv  13320  conjnmz  13349  ghmcmn  13397  gsumfzconst  13411  gsumfzmhm2  13414  rnglz  13441  rngrz  13442  isrngd  13449  ringcom  13527  crngpropd  13535  isringd  13537  ringlz  13539  ringrz  13540  ring1eq0  13544  ringmneg1  13549  mulgass3  13581  unitgrp  13612  rngidpropdg  13642  invrpropdg  13645  isrhm2d  13661  rhmunitinv  13674  subrngpropd  13712  subrginv  13733  subrgunit  13735  subrgpropd  13749  rhmpropd  13750  unitrrg  13763  lmodvs0  13818  lmodvneg1  13826  lmodcom  13829  lmodsubdi  13840  lss0v  13926  lidlrsppropdg  13991  mulgrhm2  14098  znidomb  14146  restin  14344  blpnfctr  14607  xmssym  14637  limcimolemlt  14818  dvmulxxbr  14851  dvrecap  14862  dvmptaddx  14866  dvmptmulx  14867  dvmptnegcn  14869  dvmptsubcn  14870  dvmptcjx  14871  dveflem  14872  plymullem1  14894  sin0pilem1  14916  ptolemy  14959  tangtx  14973  rpcxpneg  15042  rpcxpsub  15043  cxprec  15045  rpcxproot  15048  cxpcom  15071  rpabscxpbnd  15073  wilthlem1  15112  lgsvalmod  15135  lgsneg  15140  lgsdilem  15143  lgsne0  15154  lgssq  15156  lgssq2  15157  gausslemma2dlem1f1o  15176  gausslemma2dlem6  15183  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem4  15189  lgsquadlem1  15191  m1lgs  15192  peano4nninf  15496  nninfalllem1  15498  nninfall  15499  nninfsellemqall  15505  qdencn  15517