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  7421  updjudhcoinrg  7422  caseinl  7432  caseinr  7433  omp1eomlem  7435  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  ltexnqq  7776  prarloclemarch  7786  ltrnqg  7788  nq02m  7833  prarloclemcalc  7870  mulnqprl  7936  mulnqpru  7937  ltexprlemloc  7975  addcanprleml  7982  recexprlem1ssu  8002  cauappcvgprlem1  8027  caucvgsrlemfv  8159  caucvgsrlemoffval  8164  recidpirqlemcalc  8225  axmulass  8241  axrnegex  8247  muladd11r  8484  addcan2  8509  addsub  8539  subsub2  8556  negsubdi2  8587  muladd  8713  mulsub  8730  cru  8933  mulreim  8935  recextlem1  8982  mulap0  8985  muleqadd  9001  divrecap  9021  div23ap  9024  div12ap  9027  divmulasscomap  9029  divcanap7  9054  conjmulap  9062  apmul1  9121  nndivtr  9349  subhalfhalf  9545  xp1d2m1eqxm1d2  9563  div4p1lem1div2  9564  qapne  10049  xnegneg  10246  rexsub  10266  xnegid  10272  fseq1p1m1  10512  nn0split  10554  nnsplit  10555  fzosplitsnm1  10638  fzosplitpr  10663  fzosplitprm1  10664  ceilid  10767  flqdiv  10773  zmod10  10792  modqcyc  10811  modqaddabs  10814  mulqaddmodid  10816  modqadd2mod  10826  modqm1p1mod0  10827  modqmul12d  10830  modqadd12d  10832  modqmulmodr  10842  modqaddmulmod  10843  frecuzrdgsuc  10866  seqeq123d  10908  seqvalcd  10913  seq3f1olemqsumkj  10963  seq3f1oleml  10968  seqf1oglem2  10972  seq3id3  10976  seq3id  10977  seq3homo  10979  seq3z  10980  seqhomog  10982  exp1  10997  expnegap0  10999  expmulzap  11037  m1expeven  11038  expdivap  11042  binom3  11109  sqoddm1div8  11146  mulsubdivbinom2ap  11165  bcn1  11212  bcnp1n  11213  bcval5  11217  bcn2m1  11224  bcn2p1  11225  hashdifpr  11277  hashmap  11284  hashfibclem  11298  hashf1lem2  11302  ccatlen  11379  ccatalpha  11397  ccatw2s1leng  11422  ccats1val2  11424  lswccats1  11427  swrdlend  11446  ccatswrd  11458  pfxmpt  11468  pfxfv  11472  pfxfvlsw  11483  ccatpfx  11489  pfx1  11491  pfxswrd  11494  swrdpfx  11495  pfxpfx  11496  lenrevpfxcctswrd  11500  wrdind  11510  wrd2ind  11511  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatpfx2  11525  pfxccatid  11529  cats1fvnd  11553  crim  11639  remullem  11652  remul2  11654  immul2  11661  ipcnval  11667  cjreim  11685  recvguniqlem  11776  resqrexlemover  11792  resqrexlemcalc1  11796  absid  11853  amgm2  11901  max0addsup  12002  minabs  12020  xrmaxrecl  12040  xrminadd  12060  fsumsplitf  12194  sumsnf  12195  fsump1i  12219  fsum2dlemstep  12220  fsumshftm  12231  fsummulc2  12234  modfsummodlemstep  12243  telfsumo  12252  fsumrelem  12257  hash2iun1dif1  12266  binomlem  12269  binom1dif  12273  arisum  12284  geo2sum  12300  geo2sum2  12301  cvgratz  12318  mertenslemi1  12321  clim2prod  12325  fprodeq0  12403  fprod2dlemstep  12408  fproddivap  12416  fproddivapf  12417  fprodmodd  12427  ef0lem  12446  eftlub  12476  efsep  12477  effsumlt  12478  tanval2ap  12499  efi4p  12503  resin4p  12504  recos4p  12505  efeul  12520  sinadd  12522  cosadd  12523  sinmul  12530  ef01bndlem  12542  cos12dec  12554  absef  12556  demoivreALT  12560  dvds2ln  12610  dvdseq  12634  opeo  12683  bezoutlemnewy  12792  nninfctlemfo  12836  eucalginv  12853  eucalglt  12854  eucalg  12856  lcmgcdlem  12874  lcm1  12878  divgcdcoprmex  12899  2sqpwodd  12975  zgcdsq  13000  qden1elz  13004  phiprmpw  13023  eulerthlem1  13028  eulerthlemrprm  13030  prmdiv  13036  hashgcdlem  13039  odzdvds  13047  vfermltl  13053  modprm0  13056  pythagtriplem12  13077  pcqmul  13105  pcaddlem  13141  pcadd  13142  pcadd2  13143  pcmpt  13145  pcmpt2  13146  mul4sqlem  13195  4sqlem11  13203  4sqlem17  13209  ballotfilemfp1  13283  ballotfilemfmpn  13286  ballotfilemsi  13310  nninfdclemp1  13393  ressressg  13482  gzsumsplit1r  13768  mndinvmod  13811  mhmco  13850  grpinvid2  13911  grpasscan2  13922  grpinvssd  13935  grpinvadd  13936  grpsubid1  13943  grpsubadd  13946  grppncan  13949  mulg1  13985  mulgaddcomlem  14001  mulgdirlem  14009  mulgneg2  14012  mulgmodid  14017  nmzsubg  14066  qusinv  14092  qussub  14093  conjnmz  14135  cntzsgrpcl  14161  cntzsubm  14164  ablsub2inv  14199  abladdsub4  14202  abladdsub  14203  ablpncan2  14204  ablpnpcan  14208  ablnncan  14209  invghm  14217  gzsumconst  14227  gzsumsnfd  14231  gsumvalfi  14236  gsumsncmn  14240  gsumzfi  14242  gsumf1ofi  14244  rngm2neg  14332  srgpcompp  14379  srgpcomppsc  14380  ringinvnzdiv  14439  ringm2neg  14444  dvr1  14529  dvrcan1  14531  dvrcan3  14532  rdivmuldivd  14535  lmodfopne  14747  sralemg  14859  assa2ass  15093  assa2ass2  15094  asclmul1  15113  asclmul2  15114  assamulgscmlem2  15126  mplsubgfilemcl  15181  mplsubgfileminv  15182  xmetxpbl  15700  ivthinclemuopn  15830  limcimolemlt  15856  cnplimcim  15859  limccnpcntop  15867  limccnp2lem  15868  dvexp  15903  dvmptcmulcn  15913  dvply1  15957  ef2kpi  15999  sinhalfpip  16013  sinhalfpim  16014  coshalfpim  16016  ptolemy  16017  tangtx  16031  rpabscxpbnd  16137  relogbexpap  16155  rplogbcxp  16160  rpcxplogb  16161  zprmlogbaplem2  16177  binom4  16180  log2tlbndlog2  16181  birthdaylem2  16187  pellexlem2  16191  wilthlem1  16193  0sgm  16215  chtprm  16222  ppidif  16230  mpodvdsmulf1o  16245  fsumdvdsmul  16246  sgmppw  16247  0sgmppw  16248  1sgm2ppw  16250  chtublem  16256  chtqub  16257  perfectlem1  16260  perfectlem2  16261  perfect  16262  bposlem5  16276  bposlem9  16280  lgsval2lem  16295  lgsval4  16305  lgsval4a  16307  lgsneg  16309  lgsneg1  16310  lgsdirprm  16319  lgsdir  16320  lgsne0  16323  lgsmulsqcoprm  16331  gausslemma2dlem1a  16343  gausslemma2dlem6  16352  gausslemma2d  16354  lgseisenlem3  16357  lgseisenlem4  16358  lgseisen  16359  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem1  16366  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2lgslem3d1  16385  2sqlem3  16402  structiedg0val  16447  uhgr2edg  16613  usgr1e  16648  vtxdgfifival  16698  vtxdfifiun  16704  vtxdumgrfival  16705  vtxduspgrfvedgfi  16708  1loopgredg  16711  1loopgrvd2fi  16712  1hevtxdg1en  16715  p1evtxdeqfi  16719  edginwlkd  16762  clwwlknonex2lem1  16844  eupthvdres  16882  peano4nninf  17215  repiecele0  17241  repiecege0  17242  trilpolemclim  17252  trilpolemeq1  17256  apdifflemf  17262