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	|- ( 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 2264	. 2 |- ( ph -> B = C )
4		3eqtr3d.3	. 2 |- ( ph -> B = D )
5	3, 4	eqtr3d 2264	1 |- ( ph -> C = D )

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  5725  fvmptt  5726  fsnunfv  5840  f1ocnvfv1  5901  f1ocnvfv2  5902  fcof1  5907  caov12d  6187  caov13d  6189  caov411d  6191  caovimo  6199  tfrlem5  6460  tfrlemiubacc  6476  tfr1onlemubacc  6492  tfrcllemubacc  6505  nndir  6636  en2  6973  fopwdom  6997  updjud  7249  omp1eomlem  7261  addassnqg  7569  distrnqg  7574  enq0tr  7621  distrnq0  7646  distnq0r  7650  addnqprl  7716  addnqpru  7717  appdivnq  7750  ltmprr  7829  addcmpblnr  7926  mulcmpblnrlemg  7927  ltsrprg  7934  1idsr  7955  pn0sr  7958  mulgt0sr  7965  map2psrprg  7992  axmulass  8060  ax0id  8065  recriota  8077  mul12  8275  mul4  8278  readdcan  8286  add12  8304  cnegexlem2  8322  addcan  8326  ppncan  8388  addsub4  8389  subeqxfrd  8509  subaddeqd  8515  muladd  8530  mulcanapd  8808  receuap  8816  div13ap  8840  divdivdivap  8860  divcanap5  8861  divdivap1  8870  divdivap2  8871  halfaddsub  9345  fztp  10274  fseq1p1m1  10290  flqzadd  10518  flqdiv  10543  mulp1mod1  10587  modqnegd  10601  modqsub12d  10603  q2submod  10607  modsumfzodifsn  10618  seq3m1  10695  seq3caopr  10717  seqcaoprg  10718  iseqf1olemab  10724  iseqf1olemnanb  10725  seq3f1olemqsumk  10734  seqf1og  10743  exprecap  10802  expsubap  10809  zesq  10880  nn0opthlem1d  10942  facnn2  10956  faclbnd6  10966  zfz1isolemsplit  11060  seq3coll  11064  ccatopth  11248  shftval3  11338  crre  11368  resub  11381  imsub  11389  cjsub  11403  bdtrilem  11750  bdtri  11751  climshft2  11817  nnf1o  11887  fsumf1o  11901  isumss  11902  fisumss  11903  fsumadd  11917  isumclim3  11934  fsummulc2  11959  fsumsub  11963  telfsumo  11977  telfsumo2  11978  hashiun  11989  bcxmas  12000  isumshft  12001  trireciplem  12011  geoserap  12018  geo2sum2  12026  fprodf1o  12099  prodssdc  12100  fprodssdc  12101  fprodmul  12102  fprodm1  12109  sinsub  12251  cossub  12252  p1modz1  12305  bitsinv1lem  12472  bitsinv1  12473  gcdaddm  12505  modgcd  12512  bezoutlemnewy  12517  absmulgcd  12538  gcdmultiplez  12542  eucalg  12581  lcmgcd  12600  lcmid  12602  numdensq  12724  dfphi2  12742  phiprm  12745  fermltl  12756  prmdiveq  12758  hashgcdlem  12760  odzdvds  12768  powm2modprm  12775  modprm0  12777  coprimeprodsq  12780  pythagtriplem6  12793  pythagtriplem7  12794  pythagtriplem12  12798  pythagtriplem14  12800  pythagtriplem16  12802  pcaddlem  12862  sumhashdc  12870  fldivp1  12871  pcfac  12873  pockthlem  12879  4sqlem12  12925  4sqlem15  12928  ennnfonelem1  12978  ennnfonelemex  12985  topnpropgd  13286  qusaddvallemg  13366  grpinvalem  13418  grpinva  13419  grprida  13420  mnd12g  13461  resmhm  13520  grprcan  13570  grplcan  13595  grpasscan1  13596  grpinv11  13602  grpinvnz  13604  grplmulf1o  13607  grpinvpropdg  13608  grpinvadd  13611  grpsubsub4  13626  dfgrp3m  13632  imasgrp2  13647  mhmid  13652  mhmmnd  13653  mulgz  13687  mulgdirlem  13690  mulgdir  13691  mulgass  13696  mulgsubdir  13699  mulgpropdg  13701  isnsg3  13744  nmzsubg  13747  ssnmz  13748  eqger  13761  eqglact  13762  ghminv  13787  conjnmz  13816  ghmcmn  13864  gsumfzconst  13878  gsumfzmhm2  13881  rnglz  13908  rngrz  13909  isrngd  13916  ringcom  13994  crngpropd  14002  isringd  14004  ringlz  14006  ringrz  14007  ring1eq0  14011  ringmneg1  14016  mulgass3  14048  unitgrp  14080  rngidpropdg  14110  invrpropdg  14113  isrhm2d  14129  rhmunitinv  14142  subrngpropd  14180  subrginv  14201  subrgunit  14203  subrgpropd  14217  rhmpropd  14218  unitrrg  14231  lmodvs0  14286  lmodvneg1  14294  lmodcom  14297  lmodsubdi  14308  lss0v  14394  lidlrsppropdg  14459  mulgrhm2  14574  znidomb  14622  restin  14850  blpnfctr  15113  xmssym  15143  limcimolemlt  15338  dvmulxxbr  15376  dvrecap  15387  dvmptaddx  15393  dvmptmulx  15394  dvmptnegcn  15396  dvmptsubcn  15397  dvmptcjx  15398  dveflem  15400  plymullem1  15422  dvply1  15439  sin0pilem1  15455  ptolemy  15498  tangtx  15512  rpcxpneg  15581  rpcxpsub  15582  cxprec  15584  rpcxproot  15588  cxpcom  15612  rpabscxpbnd  15614  wilthlem1  15654  sgmppw  15666  1sgmprm  15668  1sgm2ppw  15669  perfectlem1  15673  perfectlem2  15674  lgsvalmod  15698  lgsneg  15703  lgsdilem  15706  lgsne0  15717  lgssq  15719  lgssq2  15720  gausslemma2dlem1f1o  15739  gausslemma2dlem6  15746  gausslemma2d  15748  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem4  15752  lgsquadlem1  15756  lgsquadlem3  15758  lgsquad3  15763  m1lgs  15764  peano4nninf  16372  nninfalllem1  16374  nninfall  16375  nninfsellemqall  16381  qdencn  16395