Theorem 3eqtr3d 2270

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  mpteqb  5724  fvmptt  5725  fsnunfv  5839  f1ocnvfv1  5900  f1ocnvfv2  5901  fcof1  5906  caov12d  6186  caov13d  6188  caov411d  6190  caovimo  6198  tfrlem5  6458  tfrlemiubacc  6474  tfr1onlemubacc  6490  tfrcllemubacc  6503  nndir  6634  en2  6971  fopwdom  6993  updjud  7245  omp1eomlem  7257  addassnqg  7565  distrnqg  7570  enq0tr  7617  distrnq0  7642  distnq0r  7646  addnqprl  7712  addnqpru  7713  appdivnq  7746  ltmprr  7825  addcmpblnr  7922  mulcmpblnrlemg  7923  ltsrprg  7930  1idsr  7951  pn0sr  7954  mulgt0sr  7961  map2psrprg  7988  axmulass  8056  ax0id  8061  recriota  8073  mul12  8271  mul4  8274  readdcan  8282  add12  8300  cnegexlem2  8318  addcan  8322  ppncan  8384  addsub4  8385  subeqxfrd  8505  subaddeqd  8511  muladd  8526  mulcanapd  8804  receuap  8812  div13ap  8836  divdivdivap  8856  divcanap5  8857  divdivap1  8866  divdivap2  8867  halfaddsub  9341  fztp  10270  fseq1p1m1  10286  flqzadd  10513  flqdiv  10538  mulp1mod1  10582  modqnegd  10596  modqsub12d  10598  q2submod  10602  modsumfzodifsn  10613  seq3m1  10690  seq3caopr  10712  seqcaoprg  10713  iseqf1olemab  10719  iseqf1olemnanb  10720  seq3f1olemqsumk  10729  seqf1og  10738  exprecap  10797  expsubap  10804  zesq  10875  nn0opthlem1d  10937  facnn2  10951  faclbnd6  10961  zfz1isolemsplit  11055  seq3coll  11059  ccatopth  11243  shftval3  11333  crre  11363  resub  11376  imsub  11384  cjsub  11398  bdtrilem  11745  bdtri  11746  climshft2  11812  nnf1o  11882  fsumf1o  11896  isumss  11897  fisumss  11898  fsumadd  11912  isumclim3  11929  fsummulc2  11954  fsumsub  11958  telfsumo  11972  telfsumo2  11973  hashiun  11984  bcxmas  11995  isumshft  11996  trireciplem  12006  geoserap  12013  geo2sum2  12021  fprodf1o  12094  prodssdc  12095  fprodssdc  12096  fprodmul  12097  fprodm1  12104  sinsub  12246  cossub  12247  p1modz1  12300  bitsinv1lem  12467  bitsinv1  12468  gcdaddm  12500  modgcd  12507  bezoutlemnewy  12512  absmulgcd  12533  gcdmultiplez  12537  eucalg  12576  lcmgcd  12595  lcmid  12597  numdensq  12719  dfphi2  12737  phiprm  12740  fermltl  12751  prmdiveq  12753  hashgcdlem  12755  odzdvds  12763  powm2modprm  12770  modprm0  12772  coprimeprodsq  12775  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem16  12797  pcaddlem  12857  sumhashdc  12865  fldivp1  12866  pcfac  12868  pockthlem  12874  4sqlem12  12920  4sqlem15  12923  ennnfonelem1  12973  ennnfonelemex  12980  topnpropgd  13281  qusaddvallemg  13361  grpinvalem  13413  grpinva  13414  grprida  13415  mnd12g  13456  resmhm  13515  grprcan  13565  grplcan  13590  grpasscan1  13591  grpinv11  13597  grpinvnz  13599  grplmulf1o  13602  grpinvpropdg  13603  grpinvadd  13606  grpsubsub4  13621  dfgrp3m  13627  imasgrp2  13642  mhmid  13647  mhmmnd  13648  mulgz  13682  mulgdirlem  13685  mulgdir  13686  mulgass  13691  mulgsubdir  13694  mulgpropdg  13696  isnsg3  13739  nmzsubg  13742  ssnmz  13743  eqger  13756  eqglact  13757  ghminv  13782  conjnmz  13811  ghmcmn  13859  gsumfzconst  13873  gsumfzmhm2  13876  rnglz  13903  rngrz  13904  isrngd  13911  ringcom  13989  crngpropd  13997  isringd  13999  ringlz  14001  ringrz  14002  ring1eq0  14006  ringmneg1  14011  mulgass3  14043  unitgrp  14074  rngidpropdg  14104  invrpropdg  14107  isrhm2d  14123  rhmunitinv  14136  subrngpropd  14174  subrginv  14195  subrgunit  14197  subrgpropd  14211  rhmpropd  14212  unitrrg  14225  lmodvs0  14280  lmodvneg1  14288  lmodcom  14291  lmodsubdi  14302  lss0v  14388  lidlrsppropdg  14453  mulgrhm2  14568  znidomb  14616  restin  14844  blpnfctr  15107  xmssym  15137  limcimolemlt  15332  dvmulxxbr  15370  dvrecap  15381  dvmptaddx  15387  dvmptmulx  15388  dvmptnegcn  15390  dvmptsubcn  15391  dvmptcjx  15392  dveflem  15394  plymullem1  15416  dvply1  15433  sin0pilem1  15449  ptolemy  15492  tangtx  15506  rpcxpneg  15575  rpcxpsub  15576  cxprec  15578  rpcxproot  15582  cxpcom  15606  rpabscxpbnd  15608  wilthlem1  15648  sgmppw  15660  1sgmprm  15662  1sgm2ppw  15663  perfectlem1  15667  perfectlem2  15668  lgsvalmod  15692  lgsneg  15697  lgsdilem  15700  lgsne0  15711  lgssq  15713  lgssq2  15714  gausslemma2dlem1f1o  15733  gausslemma2dlem6  15740  gausslemma2d  15742  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem4  15746  lgsquadlem1  15750  lgsquadlem3  15752  lgsquad3  15757  m1lgs  15758  peano4nninf  16331  nninfalllem1  16333  nninfall  16334  nninfsellemqall  16340  qdencn  16354