Theorem 3eqtr3d 2272

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  mpteqb  5737  fvmptt  5738  fsnunfv  5855  f1ocnvfv1  5918  f1ocnvfv2  5919  fcof1  5924  caov12d  6204  caov13d  6206  caov411d  6208  caovimo  6216  tfrlem5  6480  tfrlemiubacc  6496  tfr1onlemubacc  6512  tfrcllemubacc  6525  nndir  6658  en2  6998  fopwdom  7022  updjud  7281  omp1eomlem  7293  addassnqg  7602  distrnqg  7607  enq0tr  7654  distrnq0  7679  distnq0r  7683  addnqprl  7749  addnqpru  7750  appdivnq  7783  ltmprr  7862  addcmpblnr  7959  mulcmpblnrlemg  7960  ltsrprg  7967  1idsr  7988  pn0sr  7991  mulgt0sr  7998  map2psrprg  8025  axmulass  8093  ax0id  8098  recriota  8110  mul12  8308  mul4  8311  readdcan  8319  add12  8337  cnegexlem2  8355  addcan  8359  ppncan  8421  addsub4  8422  subeqxfrd  8542  subaddeqd  8548  muladd  8563  mulcanapd  8841  receuap  8849  div13ap  8873  divdivdivap  8893  divcanap5  8894  divdivap1  8903  divdivap2  8904  halfaddsub  9378  fztp  10313  fseq1p1m1  10329  flqzadd  10559  flqdiv  10584  mulp1mod1  10628  modqnegd  10642  modqsub12d  10644  q2submod  10648  modsumfzodifsn  10659  seq3m1  10736  seq3caopr  10758  seqcaoprg  10759  iseqf1olemab  10765  iseqf1olemnanb  10766  seq3f1olemqsumk  10775  seqf1og  10784  exprecap  10843  expsubap  10850  zesq  10921  nn0opthlem1d  10983  facnn2  10997  faclbnd6  11007  zfz1isolemsplit  11103  seq3coll  11107  ccatopth  11301  shftval3  11405  crre  11435  resub  11448  imsub  11456  cjsub  11470  bdtrilem  11817  bdtri  11818  climshft2  11884  nnf1o  11955  fsumf1o  11969  isumss  11970  fisumss  11971  fsumadd  11985  isumclim3  12002  fsummulc2  12027  fsumsub  12031  telfsumo  12045  telfsumo2  12046  hashiun  12057  bcxmas  12068  isumshft  12069  trireciplem  12079  geoserap  12086  geo2sum2  12094  fprodf1o  12167  prodssdc  12168  fprodssdc  12169  fprodmul  12170  fprodm1  12177  sinsub  12319  cossub  12320  p1modz1  12373  bitsinv1lem  12540  bitsinv1  12541  gcdaddm  12573  modgcd  12580  bezoutlemnewy  12585  absmulgcd  12606  gcdmultiplez  12610  eucalg  12649  lcmgcd  12668  lcmid  12670  numdensq  12792  dfphi2  12810  phiprm  12813  fermltl  12824  prmdiveq  12826  hashgcdlem  12828  odzdvds  12836  powm2modprm  12843  modprm0  12845  coprimeprodsq  12848  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem16  12870  pcaddlem  12930  sumhashdc  12938  fldivp1  12939  pcfac  12941  pockthlem  12947  4sqlem12  12993  4sqlem15  12996  ennnfonelem1  13046  ennnfonelemex  13053  topnpropgd  13354  qusaddvallemg  13434  grpinvalem  13486  grpinva  13487  grprida  13488  mnd12g  13529  resmhm  13588  grprcan  13638  grplcan  13663  grpasscan1  13664  grpinv11  13670  grpinvnz  13672  grplmulf1o  13675  grpinvpropdg  13676  grpinvadd  13679  grpsubsub4  13694  dfgrp3m  13700  imasgrp2  13715  mhmid  13720  mhmmnd  13721  mulgz  13755  mulgdirlem  13758  mulgdir  13759  mulgass  13764  mulgsubdir  13767  mulgpropdg  13769  isnsg3  13812  nmzsubg  13815  ssnmz  13816  eqger  13829  eqglact  13830  ghminv  13855  conjnmz  13884  ghmcmn  13932  gsumfzconst  13946  gsumfzmhm2  13949  rnglz  13977  rngrz  13978  isrngd  13985  ringcom  14063  crngpropd  14071  isringd  14073  ringlz  14075  ringrz  14076  ring1eq0  14080  ringmneg1  14085  mulgass3  14117  unitgrp  14149  rngidpropdg  14179  invrpropdg  14182  isrhm2d  14198  rhmunitinv  14211  subrngpropd  14249  subrginv  14270  subrgunit  14272  subrgpropd  14286  rhmpropd  14287  unitrrg  14300  lmodvs0  14355  lmodvneg1  14363  lmodcom  14366  lmodsubdi  14377  lss0v  14463  lidlrsppropdg  14528  mulgrhm2  14643  znidomb  14691  restin  14919  blpnfctr  15182  xmssym  15212  limcimolemlt  15407  dvmulxxbr  15445  dvrecap  15456  dvmptaddx  15462  dvmptmulx  15463  dvmptnegcn  15465  dvmptsubcn  15466  dvmptcjx  15467  dveflem  15469  plymullem1  15491  dvply1  15508  sin0pilem1  15524  ptolemy  15567  tangtx  15581  rpcxpneg  15650  rpcxpsub  15651  cxprec  15653  rpcxproot  15657  cxpcom  15681  rpabscxpbnd  15683  wilthlem1  15723  sgmppw  15735  1sgmprm  15737  1sgm2ppw  15738  perfectlem1  15742  perfectlem2  15743  lgsvalmod  15767  lgsneg  15772  lgsdilem  15775  lgsne0  15786  lgssq  15788  lgssq2  15789  gausslemma2dlem1f1o  15808  gausslemma2dlem6  15815  gausslemma2d  15817  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem4  15821  lgsquadlem1  15825  lgsquadlem3  15827  lgsquad3  15832  m1lgs  15833  p1evtxdeqfilem  16181  peano4nninf  16659  nninfalllem1  16661  nninfall  16662  nninfsellemqall  16668  qdencn  16682  qdiff  16704