Theorem 3eqtr3d 2273

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	|- ( ph -> A = B )
3eqtr3d.2	|- ( ph -> A = C )
3eqtr3d.3	|- ( ph -> B = D )

Assertion

Ref	Expression
3eqtr3d	|- ( ph -> C = D )

Proof of Theorem 3eqtr3d

Step	Hyp	Ref	Expression
1		3eqtr3d.1	. . 3 |- ( ph -> A = B )
2		3eqtr3d.2	. . 3 |- ( ph -> A = C )
3	1, 2	eqtr3d 2267	. 2 |- ( ph -> B = C )
4		3eqtr3d.3	. 2 |- ( ph -> B = D )
5	3, 4	eqtr3d 2267	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  mpteqb  5768  fvmptt  5769  fsnunfv  5885  f1ocnvfv1  5950  f1ocnvfv2  5951  fcof1  5956  caov12d  6236  caov13d  6238  caov411d  6240  caovimo  6248  tfrlem5  6545  tfrlemiubacc  6561  tfr1onlemubacc  6577  tfrcllemubacc  6590  nndir  6723  en2  7065  fopwdom  7089  updjud  7373  omp1eomlem  7385  addassnqg  7697  distrnqg  7702  enq0tr  7749  distrnq0  7774  distnq0r  7778  addnqprl  7844  addnqpru  7845  appdivnq  7878  ltmprr  7957  addcmpblnr  8054  mulcmpblnrlemg  8055  ltsrprg  8062  1idsr  8083  pn0sr  8086  mulgt0sr  8093  map2psrprg  8120  axmulass  8188  ax0id  8193  recriota  8205  mul12  8402  mul4  8405  readdcan  8413  add12  8431  cnegexlem2  8449  addcan  8453  ppncan  8515  addsub4  8516  subeqxfrd  8636  subaddeqd  8642  muladd  8657  mulcanapd  8935  receuap  8943  div13ap  8967  divdivdivap  8987  divcanap5  8988  divdivap1  8997  divdivap2  8998  halfaddsub  9472  lincmble  10337  fztp  10412  fseq1p1m1  10428  flqzadd  10658  flqdiv  10683  mulp1mod1  10727  modqnegd  10741  modqsub12d  10743  q2submod  10747  modsumfzodifsn  10758  seq3m1  10835  seq3caopr  10857  seqcaoprg  10858  iseqf1olemab  10864  iseqf1olemnanb  10865  seq3f1olemqsumk  10874  seqf1og  10883  exprecap  10942  expsubap  10949  zesq  11020  nn0opthlem1d  11082  facnn2  11096  faclbnd6  11106  bcm1n  11131  hashfibclem  11206  zfz1isolemsplit  11210  seq3coll  11214  ccatopth  11408  shftval3  11512  crre  11542  resub  11555  imsub  11563  cjsub  11577  bdtrilem  11924  bdtri  11925  climshft2  11991  nnf1o  12062  fsumf1o  12076  isumss  12077  fisumss  12078  fsumadd  12092  isumclim3  12109  fsummulc2  12134  fsumsub  12138  telfsumo  12152  telfsumo2  12153  hashiun  12164  bcxmas  12175  isumshft  12176  trireciplem  12186  geoserap  12193  geo2sum2  12201  fprodf1o  12274  prodssdc  12275  fprodssdc  12276  fprodmul  12277  fprodm1  12284  sinsub  12426  cossub  12427  p1modz1  12480  bitsinv1lem  12647  bitsinv1  12648  gcdaddm  12680  modgcd  12687  bezoutlemnewy  12692  absmulgcd  12713  gcdmultiplez  12717  eucalg  12756  lcmgcd  12775  lcmid  12777  numdensq  12899  dfphi2  12917  phiprm  12920  fermltl  12931  prmdiveq  12933  hashgcdlem  12935  odzdvds  12943  powm2modprm  12950  modprm0  12952  coprimeprodsq  12955  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem16  12977  pcaddlem  13037  sumhashdc  13045  fldivp1  13046  pcfac  13048  pockthlem  13054  4sqlem12  13100  4sqlem15  13103  ennnfonelem1  13158  ennnfonelemex  13165  topnpropgd  13466  qusaddvallemg  13546  grpinvalem  13598  grpinva  13599  grprida  13600  mnd12g  13641  resmhm  13700  grprcan  13750  grplcan  13775  grpasscan1  13776  grpinv11  13782  grpinvnz  13784  grplmulf1o  13787  grpinvpropdg  13788  grpinvadd  13791  grpsubsub4  13806  dfgrp3m  13812  imasgrp2  13827  mhmid  13832  mhmmnd  13833  mulgz  13867  mulgdirlem  13870  mulgdir  13871  mulgass  13876  mulgsubdir  13879  mulgpropdg  13881  isnsg3  13924  nmzsubg  13927  ssnmz  13928  eqger  13941  eqglact  13942  ghminv  13967  conjnmz  13996  ghmcmn  14044  gsumfzconst  14058  gsumfzmhm2  14061  rnglz  14089  rngrz  14090  isrngd  14097  ringcom  14175  crngpropd  14183  isringd  14185  ringlz  14187  ringrz  14188  ring1eq0  14192  ringmneg1  14197  mulgass3  14229  unitgrp  14261  rngidpropdg  14291  invrpropdg  14294  isrhm2d  14310  rhmunitinv  14323  subrngpropd  14361  subrginv  14382  subrgunit  14384  subrgpropd  14398  rhmpropd  14399  unitrrg  14413  aprlring  14434  lmodvs0  14470  lmodvneg1  14478  lmodcom  14481  lmodsubdi  14492  lss0v  14578  lidlrsppropdg  14643  mulgrhm2  14758  znidomb  14806  restin  15041  blpnfctr  15304  xmssym  15334  limcimolemlt  15529  dvmulxxbr  15567  dvrecap  15578  dvmptaddx  15584  dvmptmulx  15585  dvmptnegcn  15587  dvmptsubcn  15588  dvmptcjx  15589  dveflem  15591  plymullem1  15613  dvply1  15630  sin0pilem1  15646  ptolemy  15689  tangtx  15703  rpcxpneg  15772  rpcxpsub  15773  cxprec  15775  rpcxproot  15779  cxpcom  15803  rpabscxpbnd  15805  pellexlem2  15846  wilthlem1  15848  sgmppw  15860  1sgmprm  15862  1sgm2ppw  15863  perfectlem1  15867  perfectlem2  15868  lgsvalmod  15892  lgsneg  15897  lgsdilem  15900  lgsne0  15911  lgssq  15913  lgssq2  15914  gausslemma2dlem1f1o  15933  gausslemma2dlem6  15940  gausslemma2d  15942  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem4  15946  lgsquadlem1  15950  lgsquadlem3  15952  lgsquad3  15957  m1lgs  15958  p1evtxdeqfilem  16306  peano4nninf  16784  nninfalllem1  16786  nninfall  16787  nninfsellemqall  16793  qdencn  16807  qdiff  16833