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  5727  fvmptt  5728  fsnunfv  5844  f1ocnvfv1  5907  f1ocnvfv2  5908  fcof1  5913  caov12d  6193  caov13d  6195  caov411d  6197  caovimo  6205  tfrlem5  6466  tfrlemiubacc  6482  tfr1onlemubacc  6498  tfrcllemubacc  6511  nndir  6644  en2  6981  fopwdom  7005  updjud  7257  omp1eomlem  7269  addassnqg  7577  distrnqg  7582  enq0tr  7629  distrnq0  7654  distnq0r  7658  addnqprl  7724  addnqpru  7725  appdivnq  7758  ltmprr  7837  addcmpblnr  7934  mulcmpblnrlemg  7935  ltsrprg  7942  1idsr  7963  pn0sr  7966  mulgt0sr  7973  map2psrprg  8000  axmulass  8068  ax0id  8073  recriota  8085  mul12  8283  mul4  8286  readdcan  8294  add12  8312  cnegexlem2  8330  addcan  8334  ppncan  8396  addsub4  8397  subeqxfrd  8517  subaddeqd  8523  muladd  8538  mulcanapd  8816  receuap  8824  div13ap  8848  divdivdivap  8868  divcanap5  8869  divdivap1  8878  divdivap2  8879  halfaddsub  9353  fztp  10282  fseq1p1m1  10298  flqzadd  10526  flqdiv  10551  mulp1mod1  10595  modqnegd  10609  modqsub12d  10611  q2submod  10615  modsumfzodifsn  10626  seq3m1  10703  seq3caopr  10725  seqcaoprg  10726  iseqf1olemab  10732  iseqf1olemnanb  10733  seq3f1olemqsumk  10742  seqf1og  10751  exprecap  10810  expsubap  10817  zesq  10888  nn0opthlem1d  10950  facnn2  10964  faclbnd6  10974  zfz1isolemsplit  11068  seq3coll  11072  ccatopth  11256  shftval3  11346  crre  11376  resub  11389  imsub  11397  cjsub  11411  bdtrilem  11758  bdtri  11759  climshft2  11825  nnf1o  11895  fsumf1o  11909  isumss  11910  fisumss  11911  fsumadd  11925  isumclim3  11942  fsummulc2  11967  fsumsub  11971  telfsumo  11985  telfsumo2  11986  hashiun  11997  bcxmas  12008  isumshft  12009  trireciplem  12019  geoserap  12026  geo2sum2  12034  fprodf1o  12107  prodssdc  12108  fprodssdc  12109  fprodmul  12110  fprodm1  12117  sinsub  12259  cossub  12260  p1modz1  12313  bitsinv1lem  12480  bitsinv1  12481  gcdaddm  12513  modgcd  12520  bezoutlemnewy  12525  absmulgcd  12546  gcdmultiplez  12550  eucalg  12589  lcmgcd  12608  lcmid  12610  numdensq  12732  dfphi2  12750  phiprm  12753  fermltl  12764  prmdiveq  12766  hashgcdlem  12768  odzdvds  12776  powm2modprm  12783  modprm0  12785  coprimeprodsq  12788  pythagtriplem6  12801  pythagtriplem7  12802  pythagtriplem12  12806  pythagtriplem14  12808  pythagtriplem16  12810  pcaddlem  12870  sumhashdc  12878  fldivp1  12879  pcfac  12881  pockthlem  12887  4sqlem12  12933  4sqlem15  12936  ennnfonelem1  12986  ennnfonelemex  12993  topnpropgd  13294  qusaddvallemg  13374  grpinvalem  13426  grpinva  13427  grprida  13428  mnd12g  13469  resmhm  13528  grprcan  13578  grplcan  13603  grpasscan1  13604  grpinv11  13610  grpinvnz  13612  grplmulf1o  13615  grpinvpropdg  13616  grpinvadd  13619  grpsubsub4  13634  dfgrp3m  13640  imasgrp2  13655  mhmid  13660  mhmmnd  13661  mulgz  13695  mulgdirlem  13698  mulgdir  13699  mulgass  13704  mulgsubdir  13707  mulgpropdg  13709  isnsg3  13752  nmzsubg  13755  ssnmz  13756  eqger  13769  eqglact  13770  ghminv  13795  conjnmz  13824  ghmcmn  13872  gsumfzconst  13886  gsumfzmhm2  13889  rnglz  13916  rngrz  13917  isrngd  13924  ringcom  14002  crngpropd  14010  isringd  14012  ringlz  14014  ringrz  14015  ring1eq0  14019  ringmneg1  14024  mulgass3  14056  unitgrp  14088  rngidpropdg  14118  invrpropdg  14121  isrhm2d  14137  rhmunitinv  14150  subrngpropd  14188  subrginv  14209  subrgunit  14211  subrgpropd  14225  rhmpropd  14226  unitrrg  14239  lmodvs0  14294  lmodvneg1  14302  lmodcom  14305  lmodsubdi  14316  lss0v  14402  lidlrsppropdg  14467  mulgrhm2  14582  znidomb  14630  restin  14858  blpnfctr  15121  xmssym  15151  limcimolemlt  15346  dvmulxxbr  15384  dvrecap  15395  dvmptaddx  15401  dvmptmulx  15402  dvmptnegcn  15404  dvmptsubcn  15405  dvmptcjx  15406  dveflem  15408  plymullem1  15430  dvply1  15447  sin0pilem1  15463  ptolemy  15506  tangtx  15520  rpcxpneg  15589  rpcxpsub  15590  cxprec  15592  rpcxproot  15596  cxpcom  15620  rpabscxpbnd  15622  wilthlem1  15662  sgmppw  15674  1sgmprm  15676  1sgm2ppw  15677  perfectlem1  15681  perfectlem2  15682  lgsvalmod  15706  lgsneg  15711  lgsdilem  15714  lgsne0  15725  lgssq  15727  lgssq2  15728  gausslemma2dlem1f1o  15747  gausslemma2dlem6  15754  gausslemma2d  15756  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem4  15760  lgsquadlem1  15764  lgsquadlem3  15766  lgsquad3  15771  m1lgs  15772  peano4nninf  16399  nninfalllem1  16401  nninfall  16402  nninfsellemqall  16408  qdencn  16422