Theorem 3eqtrd 2275

Description: A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)

Hypotheses

Ref	Expression
3eqtrd.1	|- ( ph -> A = B )
3eqtrd.2	|- ( ph -> B = C )
3eqtrd.3	|- ( ph -> C = D )

Assertion

Ref	Expression
3eqtrd	|- ( ph -> A = D )

Proof of Theorem 3eqtrd

Step	Hyp	Ref	Expression
1		3eqtrd.1	. 2 |- ( ph -> A = B )
2		3eqtrd.2	. . 3 |- ( ph -> B = C )
3		3eqtrd.3	. . 3 |- ( ph -> C = D )
4	2, 3	eqtrd 2271	. 2 |- ( ph -> B = D )
5	1, 4	eqtrd 2271	1 |- ( ph -> A = 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:  tpeq123d  3803  diftpsn3  3856  oteq123d  3919  resiima  5145  fvun1  5769  fvmptd  5786  fmptpr  5907  caovlem2d  6282  offval  6310  ofvalg  6312  cnvf1olem  6460  supp0  6478  suppsnopdc  6490  suppofss1dcl  6504  suppofss2dcl  6505  suppcofn  6506  nnm1  6798  updjudhcoinlf  7420  updjudhcoinrg  7421  caseinl  7431  caseinr  7432  omp1eomlem  7434  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  ltexnqq  7775  prarloclemarch  7785  ltrnqg  7787  nq02m  7832  prarloclemcalc  7869  mulnqprl  7935  mulnqpru  7936  ltexprlemloc  7974  addcanprleml  7981  recexprlem1ssu  8001  cauappcvgprlem1  8026  caucvgsrlemfv  8158  caucvgsrlemoffval  8163  recidpirqlemcalc  8224  axmulass  8240  axrnegex  8246  muladd11r  8482  addcan2  8507  addsub  8537  subsub2  8554  negsubdi2  8585  muladd  8711  mulsub  8728  cru  8930  mulreim  8932  recextlem1  8979  mulap0  8982  muleqadd  8998  divrecap  9018  div23ap  9021  div12ap  9024  divmulasscomap  9026  divcanap7  9051  conjmulap  9059  apmul1  9118  nndivtr  9346  subhalfhalf  9540  xp1d2m1eqxm1d2  9558  div4p1lem1div2  9559  qapne  10039  xnegneg  10235  rexsub  10255  xnegid  10261  fseq1p1m1  10501  nn0split  10543  nnsplit  10544  fzosplitsnm1  10627  fzosplitpr  10652  fzosplitprm1  10653  ceilid  10752  flqdiv  10758  zmod10  10777  modqcyc  10796  modqaddabs  10799  mulqaddmodid  10801  modqadd2mod  10811  modqm1p1mod0  10812  modqmul12d  10815  modqadd12d  10817  modqmulmodr  10827  modqaddmulmod  10828  frecuzrdgsuc  10851  seqeq123d  10893  seqvalcd  10898  seq3f1olemqsumkj  10948  seq3f1oleml  10953  seqf1oglem2  10957  seq3id3  10961  seq3id  10962  seq3homo  10964  seq3z  10965  seqhomog  10967  exp1  10982  expnegap0  10984  expmulzap  11022  m1expeven  11023  expdivap  11027  binom3  11094  sqoddm1div8  11131  mulsubdivbinom2ap  11149  bcn1  11196  bcnp1n  11197  bcval5  11201  bcn2m1  11208  bcn2p1  11209  hashdifpr  11261  hashmap  11268  hashfibclem  11282  hashf1lem2  11286  ccatlen  11363  ccatalpha  11381  ccatw2s1leng  11406  ccats1val2  11408  lswccats1  11411  swrdlend  11430  ccatswrd  11442  pfxmpt  11452  pfxfv  11456  pfxfvlsw  11467  ccatpfx  11473  pfx1  11475  pfxswrd  11478  swrdpfx  11479  pfxpfx  11480  lenrevpfxcctswrd  11484  wrdind  11494  wrd2ind  11495  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatpfx2  11509  pfxccatid  11513  cats1fvnd  11537  crim  11623  remullem  11636  remul2  11638  immul2  11645  ipcnval  11651  cjreim  11669  recvguniqlem  11760  resqrexlemover  11776  resqrexlemcalc1  11780  absid  11837  amgm2  11884  max0addsup  11985  minabs  12002  xrmaxrecl  12021  xrminadd  12041  fsumsplitf  12175  sumsnf  12176  fsump1i  12200  fsum2dlemstep  12201  fsumshftm  12212  fsummulc2  12215  modfsummodlemstep  12224  telfsumo  12233  fsumrelem  12238  hash2iun1dif1  12247  binomlem  12250  binom1dif  12254  arisum  12265  geo2sum  12281  geo2sum2  12282  cvgratz  12299  mertenslemi1  12302  clim2prod  12306  fprodeq0  12384  fprod2dlemstep  12389  fproddivap  12397  fproddivapf  12398  fprodmodd  12408  ef0lem  12427  eftlub  12457  efsep  12458  effsumlt  12459  tanval2ap  12480  efi4p  12484  resin4p  12485  recos4p  12486  efeul  12501  sinadd  12503  cosadd  12504  sinmul  12511  ef01bndlem  12523  cos12dec  12535  absef  12537  demoivreALT  12541  dvds2ln  12591  dvdseq  12615  opeo  12664  bezoutlemnewy  12773  nninfctlemfo  12817  eucalginv  12834  eucalglt  12835  eucalg  12837  lcmgcdlem  12855  lcm1  12859  divgcdcoprmex  12880  2sqpwodd  12954  zgcdsq  12979  qden1elz  12983  phiprmpw  13000  eulerthlem1  13005  eulerthlemrprm  13007  prmdiv  13013  hashgcdlem  13016  odzdvds  13024  vfermltl  13030  modprm0  13033  pythagtriplem12  13054  pcqmul  13082  pcaddlem  13118  pcadd  13119  pcadd2  13120  pcmpt  13122  pcmpt2  13123  mul4sqlem  13172  4sqlem11  13180  4sqlem17  13186  ballotfilemfp1  13231  ballotfilemfmpn  13234  ballotfilemsi  13258  nninfdclemp1  13341  ressressg  13429  gzsumsplit1r  13715  mndinvmod  13758  mhmco  13797  grpinvid2  13858  grpasscan2  13869  grpinvssd  13882  grpinvadd  13883  grpsubid1  13890  grpsubadd  13893  grppncan  13896  mulg1  13932  mulgaddcomlem  13948  mulgdirlem  13956  mulgneg2  13959  mulgmodid  13964  nmzsubg  14013  qusinv  14039  qussub  14040  conjnmz  14082  ablsub2inv  14115  abladdsub4  14118  abladdsub  14119  ablpncan2  14120  ablpnpcan  14124  ablnncan  14125  invghm  14133  gzsumconst  14143  gzsumsnfd  14147  gsumvalfi  14152  gsumsncmn  14156  gsumzfi  14158  gsumf1ofi  14160  rngm2neg  14248  srgpcompp  14295  srgpcomppsc  14296  ringinvnzdiv  14355  ringm2neg  14360  dvr1  14445  dvrcan1  14447  dvrcan3  14448  rdivmuldivd  14451  lmodfopne  14663  sralemg  14775  assa2ass  15009  assa2ass2  15010  asclmul1  15029  asclmul2  15030  assamulgscmlem2  15042  mplsubgfilemcl  15090  mplsubgfileminv  15091  xmetxpbl  15609  ivthinclemuopn  15739  limcimolemlt  15765  cnplimcim  15768  limccnpcntop  15776  limccnp2lem  15777  dvexp  15812  dvmptcmulcn  15822  dvply1  15866  ef2kpi  15907  sinhalfpip  15921  sinhalfpim  15922  coshalfpim  15924  ptolemy  15925  tangtx  15939  rpabscxpbnd  16042  relogbexpap  16060  rplogbcxp  16065  rpcxplogb  16066  binom4  16081  log2tlbndlog2  16082  birthdaylem2  16088  pellexlem2  16092  wilthlem1  16094  0sgm  16099  mpodvdsmulf1o  16104  fsumdvdsmul  16105  sgmppw  16106  0sgmppw  16107  1sgm2ppw  16109  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgsval2lem  16129  lgsval4  16139  lgsval4a  16141  lgsneg  16143  lgsneg1  16144  lgsdirprm  16153  lgsdir  16154  lgsne0  16157  lgsmulsqcoprm  16165  gausslemma2dlem1a  16177  gausslemma2dlem6  16186  gausslemma2d  16188  lgseisenlem3  16191  lgseisenlem4  16192  lgseisen  16193  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem1  16200  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgslem3d1  16219  2sqlem3  16236  structiedg0val  16281  uhgr2edg  16447  usgr1e  16482  vtxdgfifival  16532  vtxdfifiun  16538  vtxdumgrfival  16539  vtxduspgrfvedgfi  16542  1loopgredg  16545  1loopgrvd2fi  16546  1hevtxdg1en  16549  p1evtxdeqfi  16553  edginwlkd  16596  clwwlknonex2lem1  16678  eupthvdres  16716  peano4nninf  17049  repiecele0  17075  repiecege0  17076  trilpolemclim  17085  trilpolemeq1  17089  apdifflemf  17095