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 )

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  tpeq123d  3799  diftpsn3  3851  oteq123d  3914  resiima  5140  fvun1  5763  fvmptd  5780  fmptpr  5898  caovlem2d  6272  offval  6300  ofvalg  6302  cnvf1olem  6450  supp0  6468  suppsnopdc  6480  suppofss1dcl  6494  suppofss2dcl  6495  suppcofn  6496  nnm1  6788  updjudhcoinlf  7410  updjudhcoinrg  7411  caseinl  7421  caseinr  7422  omp1eomlem  7424  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  ltexnqq  7765  prarloclemarch  7775  ltrnqg  7777  nq02m  7822  prarloclemcalc  7859  mulnqprl  7925  mulnqpru  7926  ltexprlemloc  7964  addcanprleml  7971  recexprlem1ssu  7991  cauappcvgprlem1  8016  caucvgsrlemfv  8148  caucvgsrlemoffval  8153  recidpirqlemcalc  8214  axmulass  8230  axrnegex  8236  muladd11r  8472  addcan2  8497  addsub  8527  subsub2  8544  negsubdi2  8575  muladd  8701  mulsub  8718  cru  8920  mulreim  8922  recextlem1  8969  mulap0  8972  muleqadd  8988  divrecap  9008  div23ap  9011  div12ap  9014  divmulasscomap  9016  divcanap7  9041  conjmulap  9049  apmul1  9108  nndivtr  9325  subhalfhalf  9519  xp1d2m1eqxm1d2  9537  div4p1lem1div2  9538  qapne  10018  xnegneg  10214  rexsub  10234  xnegid  10240  fseq1p1m1  10479  nn0split  10521  nnsplit  10522  fzosplitsnm1  10605  fzosplitpr  10630  fzosplitprm1  10631  ceilid  10730  flqdiv  10736  zmod10  10755  modqcyc  10774  modqaddabs  10777  mulqaddmodid  10779  modqadd2mod  10789  modqm1p1mod0  10790  modqmul12d  10793  modqadd12d  10795  modqmulmodr  10805  modqaddmulmod  10806  frecuzrdgsuc  10829  seqeq123d  10871  seqvalcd  10876  seq3f1olemqsumkj  10926  seq3f1oleml  10931  seqf1oglem2  10935  seq3id3  10939  seq3id  10940  seq3homo  10942  seq3z  10943  seqhomog  10945  exp1  10960  expnegap0  10962  expmulzap  11000  m1expeven  11001  expdivap  11005  binom3  11072  sqoddm1div8  11109  mulsubdivbinom2ap  11127  bcn1  11174  bcnp1n  11175  bcval5  11179  bcn2m1  11186  bcn2p1  11187  hashdifpr  11239  hashmap  11246  hashfibclem  11260  hashf1lem2  11264  ccatlen  11341  ccatalpha  11359  ccatw2s1leng  11384  ccats1val2  11386  lswccats1  11389  swrdlend  11408  ccatswrd  11420  pfxmpt  11430  pfxfv  11434  pfxfvlsw  11445  ccatpfx  11451  pfx1  11453  pfxswrd  11456  swrdpfx  11457  pfxpfx  11458  lenrevpfxcctswrd  11462  wrdind  11472  wrd2ind  11473  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatpfx2  11487  pfxccatid  11491  cats1fvnd  11515  crim  11601  remullem  11614  remul2  11616  immul2  11623  ipcnval  11629  cjreim  11647  recvguniqlem  11738  resqrexlemover  11754  resqrexlemcalc1  11758  absid  11815  amgm2  11862  max0addsup  11963  minabs  11980  xrmaxrecl  11999  xrminadd  12019  fsumsplitf  12153  sumsnf  12154  fsump1i  12178  fsum2dlemstep  12179  fsumshftm  12190  fsummulc2  12193  modfsummodlemstep  12202  telfsumo  12211  fsumrelem  12216  hash2iun1dif1  12225  binomlem  12228  binom1dif  12232  arisum  12243  geo2sum  12259  geo2sum2  12260  cvgratz  12277  mertenslemi1  12280  clim2prod  12284  fprodeq0  12362  fprod2dlemstep  12367  fproddivap  12375  fproddivapf  12376  fprodmodd  12386  ef0lem  12405  eftlub  12435  efsep  12436  effsumlt  12437  tanval2ap  12458  efi4p  12462  resin4p  12463  recos4p  12464  efeul  12479  sinadd  12481  cosadd  12482  sinmul  12489  ef01bndlem  12501  cos12dec  12513  absef  12515  demoivreALT  12519  dvds2ln  12569  dvdseq  12593  opeo  12642  bezoutlemnewy  12751  nninfctlemfo  12795  eucalginv  12812  eucalglt  12813  eucalg  12815  lcmgcdlem  12833  lcm1  12837  divgcdcoprmex  12858  2sqpwodd  12932  zgcdsq  12957  qden1elz  12961  phiprmpw  12978  eulerthlem1  12983  eulerthlemrprm  12985  prmdiv  12991  hashgcdlem  12994  odzdvds  13002  vfermltl  13008  modprm0  13011  pythagtriplem12  13032  pcqmul  13060  pcaddlem  13096  pcadd  13097  pcadd2  13098  pcmpt  13100  pcmpt2  13101  mul4sqlem  13150  4sqlem11  13158  4sqlem17  13164  ballotfilemfp1  13209  ballotfilemfmpn  13212  ballotfilemsi  13236  nninfdclemp1  13319  ressressg  13406  gzsumsplit1r  13692  mndinvmod  13735  mhmco  13774  grpinvid2  13835  grpasscan2  13846  grpinvssd  13859  grpinvadd  13860  grpsubid1  13867  grpsubadd  13870  grppncan  13873  mulg1  13909  mulgaddcomlem  13925  mulgdirlem  13933  mulgneg2  13936  mulgmodid  13941  nmzsubg  13990  qusinv  14016  qussub  14017  conjnmz  14059  ablsub2inv  14092  abladdsub4  14095  abladdsub  14096  ablpncan2  14097  ablpnpcan  14101  ablnncan  14102  invghm  14110  gzsumconst  14120  gzsumsnfd  14124  gsumvalfi  14129  gsumsncmn  14133  gsumzfi  14135  gsumf1ofi  14137  rngm2neg  14223  srgpcompp  14269  srgpcomppsc  14270  ringinvnzdiv  14328  ringm2neg  14333  dvr1  14418  dvrcan1  14420  dvrcan3  14421  rdivmuldivd  14424  lmodfopne  14635  sralemg  14747  mplsubgfilemcl  15013  mplsubgfileminv  15014  xmetxpbl  15532  ivthinclemuopn  15662  limcimolemlt  15688  cnplimcim  15691  limccnpcntop  15699  limccnp2lem  15700  dvexp  15735  dvmptcmulcn  15745  dvply1  15789  ef2kpi  15830  sinhalfpip  15844  sinhalfpim  15845  coshalfpim  15847  ptolemy  15848  tangtx  15862  rpabscxpbnd  15965  relogbexpap  15983  rplogbcxp  15988  rpcxplogb  15989  binom4  16004  pellexlem2  16006  wilthlem1  16008  0sgm  16013  mpodvdsmulf1o  16018  fsumdvdsmul  16019  sgmppw  16020  0sgmppw  16021  1sgm2ppw  16023  perfectlem1  16027  perfectlem2  16028  perfect  16029  lgsval2lem  16043  lgsval4  16053  lgsval4a  16055  lgsneg  16057  lgsneg1  16058  lgsdirprm  16067  lgsdir  16068  lgsne0  16071  lgsmulsqcoprm  16079  gausslemma2dlem1a  16091  gausslemma2dlem6  16100  gausslemma2d  16102  lgseisenlem3  16105  lgseisenlem4  16106  lgseisen  16107  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem1  16114  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2lgslem3d1  16133  2sqlem3  16150  structiedg0val  16195  uhgr2edg  16361  usgr1e  16396  vtxdgfifival  16446  vtxdfifiun  16452  vtxdumgrfival  16453  vtxduspgrfvedgfi  16456  1loopgredg  16459  1loopgrvd2fi  16460  1hevtxdg1en  16463  p1evtxdeqfi  16467  edginwlkd  16510  clwwlknonex2lem1  16592  eupthvdres  16630  peano4nninf  16954  repiecele0  16980  repiecege0  16981  trilpolemclim  16990  trilpolemeq1  16994  apdifflemf  17000