Theorem 3eqtr3d 2279

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  mpteqb  5796  fvmptt  5797  fsnunfv  5916  f1ocnvfv1  5983  f1ocnvfv2  5984  fcof1  5989  caov12d  6271  caov13d  6273  caov411d  6275  caovimo  6283  tfrlem5  6585  tfrlemiubacc  6601  tfr1onlemubacc  6617  tfrcllemubacc  6630  nndir  6763  en2  7112  fopwdom  7136  updjud  7423  omp1eomlem  7435  addassnqg  7750  distrnqg  7755  enq0tr  7802  distrnq0  7827  distnq0r  7831  addnqprl  7897  addnqpru  7898  appdivnq  7931  ltmprr  8010  addcmpblnr  8107  mulcmpblnrlemg  8108  ltsrprg  8115  1idsr  8136  pn0sr  8139  mulgt0sr  8146  map2psrprg  8173  axmulass  8241  ax0id  8246  recriota  8258  mul12  8457  mul4  8460  readdcan  8468  add12  8486  cnegexlem2  8504  addcan  8508  ppncan  8570  addsub4  8571  subeqxfrd  8691  subaddeqd  8697  muladd  8713  mulcanapd  8992  receuap  9002  div13ap  9026  divdivdivap  9046  divcanap5  9047  divdivap1  9056  divdivap2  9057  halfaddsub  9544  lincmble  10417  fztp  10496  fseq1p1m1  10512  flqzadd  10748  flqdiv  10773  mulp1mod1  10817  modqnegd  10831  modqsub12d  10833  q2submod  10837  modsumfzodifsn  10848  seq3m1  10925  seq3caopr  10947  seqcaoprg  10948  iseqf1olemab  10954  iseqf1olemnanb  10955  seq3f1olemqsumk  10964  seqf1og  10973  exprecap  11032  expsubap  11039  zesq  11111  nn0opthlem1d  11174  facnn2  11188  faclbnd6  11198  bcm1n  11223  hashfibclem  11298  hashfac  11304  zfz1isolemsplit  11306  seq3coll  11310  ccatopth  11504  shftval3  11608  crre  11638  resub  11651  imsub  11659  cjsub  11673  sq01  11676  bdtrilem  12024  bdtri  12025  climshft2  12091  nnf1o  12162  fsumf1o  12176  isumss  12177  fisumss  12178  fsumadd  12192  isumclim3  12209  fsummulc2  12234  fsumsub  12238  telfsumo  12252  telfsumo2  12253  hashiun  12264  bcxmas  12275  isumshft  12276  trireciplem  12286  geoserap  12293  geo2sum2  12301  fprodf1o  12374  prodssdc  12375  fprodssdc  12376  fprodmul  12377  fprodm1  12384  sinsub  12526  cossub  12527  p1modz1  12580  bitsinv1lem  12747  bitsinv1  12748  gcdaddm  12780  modgcd  12787  bezoutlemnewy  12792  absmulgcd  12813  gcdmultiplez  12817  eucalg  12856  lcmgcd  12875  lcmid  12877  numdensq  13001  dfphi2  13021  phiprm  13024  fermltl  13035  prmdiveq  13037  hashgcdlem  13039  odzdvds  13047  powm2modprm  13054  modprm0  13056  coprimeprodsq  13059  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem16  13081  pcaddlem  13141  sumhashdc  13149  fldivp1  13150  pcfac  13152  pockthlem  13158  4sqlem12  13204  4sqlem15  13207  ennnfonelem1  13350  ennnfonelemex  13357  topnpropgd  13660  qusaddvallemg  13707  grpinvalem  13758  grpinva  13759  grprida  13760  mnd12g  13794  resmhm  13847  grprcan  13895  grplcan  13920  grpasscan1  13921  grpinv11  13927  grpinvnz  13929  grplmulf1o  13932  grpinvpropdg  13933  grpinvadd  13936  grpsubsub4  13951  dfgrp3m  13957  imasgrp2  13966  mhmid  13971  mhmmnd  13972  mulgz  14006  mulgdirlem  14009  mulgdir  14010  mulgass  14015  mulgsubdir  14018  mulgpropdg  14020  isnsg3  14063  nmzsubg  14066  ssnmz  14067  eqger  14080  eqglact  14081  ghminv  14106  conjnmz  14135  cntzsubg  14165  cntzmhm  14167  ghmcmn  14215  gzsumconst  14227  gzsummhm2  14230  gsummhm2fi  14249  rnglz  14328  rngrz  14329  isrngd  14336  ringcom  14420  crngpropd  14428  isringd  14430  ringlz  14432  ringrz  14433  ring1eq0  14437  ringmneg1  14442  mulgass3  14475  unitgrp  14507  rngidpropdg  14537  invrpropdg  14540  isrhm2d  14556  rhmunitinv  14569  subrngpropd  14608  subrginv  14629  subrgunit  14631  subrgpropd  14645  rhmpropd  14646  unitrrg  14660  aprlring  14684  lmodvs0  14743  lmodvneg1  14751  lmodcom  14754  lmodsubdi  14765  lss0v  14851  lidlrsppropdg  14916  mulgrhm2  15029  znidomb  15077  asclpropd  15124  restin  15368  blpnfctr  15631  xmssym  15661  limcimolemlt  15856  dvmulxxbr  15894  dvrecap  15905  dvmptaddx  15911  dvmptmulx  15912  dvmptnegcn  15914  dvmptsubcn  15915  dvmptcjx  15916  dveflem  15918  plymullem1  15940  dvply1  15957  sin0pilem1  15974  ptolemy  16017  tangtx  16031  rpcxpneg  16104  rpcxpsub  16105  cxprec  16107  rpcxproot  16111  cxpcom  16135  rpabscxpbnd  16137  zprmlogbaplem3  16178  pellexlem2  16191  wilthlem1  16193  sgmppw  16247  1sgmprm  16249  1sgm2ppw  16250  ppiqub  16254  perfectlem1  16260  perfectlem2  16261  bposlem6  16277  bposlem9  16280  lgsvalmod  16304  lgsneg  16309  lgsdilem  16312  lgsne0  16323  lgssq  16325  lgssq2  16326  gausslemma2dlem1f1o  16345  gausslemma2dlem6  16352  gausslemma2d  16354  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem4  16358  lgsquadlem1  16362  lgsquadlem3  16364  lgsquad3  16369  m1lgs  16370  p1evtxdeqfilem  16718  peano4nninf  17215  nninfalllem1  17217  nninfall  17218  nninfsellemqall  17224  qdencn  17238  qdiff  17265