Theorem 3eqtrd 2268

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  tpeq123d  3767  diftpsn3  3819  oteq123d  3882  resiima  5101  fvun1  5721  fvmptd  5736  fmptpr  5854  caovlem2d  6225  offval  6252  ofvalg  6254  cnvf1olem  6398  supp0  6416  suppsnopdc  6428  suppofss1dcl  6442  suppofss2dcl  6443  suppcofn  6444  nnm1  6736  updjudhcoinlf  7339  updjudhcoinrg  7340  caseinl  7350  caseinr  7351  omp1eomlem  7353  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  ltexnqq  7688  prarloclemarch  7698  ltrnqg  7700  nq02m  7745  prarloclemcalc  7782  mulnqprl  7848  mulnqpru  7849  ltexprlemloc  7887  addcanprleml  7894  recexprlem1ssu  7914  cauappcvgprlem1  7939  caucvgsrlemfv  8071  caucvgsrlemoffval  8076  recidpirqlemcalc  8137  axmulass  8153  axrnegex  8159  muladd11r  8394  addcan2  8419  addsub  8449  subsub2  8466  negsubdi2  8497  muladd  8622  mulsub  8639  cru  8841  mulreim  8843  recextlem1  8890  mulap0  8893  muleqadd  8907  divrecap  8927  div23ap  8930  div12ap  8933  divmulasscomap  8935  divcanap7  8960  conjmulap  8968  apmul1  9027  nndivtr  9244  subhalfhalf  9438  xp1d2m1eqxm1d2  9456  div4p1lem1div2  9457  qapne  9934  xnegneg  10129  rexsub  10149  xnegid  10155  fseq1p1m1  10391  nn0split  10433  nnsplit  10434  fzosplitsnm1  10517  fzosplitpr  10542  fzosplitprm1  10543  ceilid  10640  flqdiv  10646  zmod10  10665  modqcyc  10684  modqaddabs  10687  mulqaddmodid  10689  modqadd2mod  10699  modqm1p1mod0  10700  modqmul12d  10703  modqadd12d  10705  modqmulmodr  10715  modqaddmulmod  10716  frecuzrdgsuc  10739  seqeq123d  10781  seqvalcd  10786  seq3f1olemqsumkj  10836  seq3f1oleml  10841  seqf1oglem2  10845  seq3id3  10849  seq3id  10850  seq3homo  10852  seq3z  10853  seqhomog  10855  exp1  10870  expnegap0  10872  expmulzap  10910  m1expeven  10911  expdivap  10915  binom3  10982  sqoddm1div8  11018  mulsubdivbinom2ap  11036  bcn1  11083  bcnp1n  11084  bcval5  11088  bcn2m1  11094  bcn2p1  11095  hashdifpr  11147  ccatlen  11238  ccatalpha  11256  ccatw2s1leng  11281  ccats1val2  11283  lswccats1  11286  swrdlend  11305  ccatswrd  11317  pfxmpt  11327  pfxfv  11331  pfxfvlsw  11342  ccatpfx  11348  pfx1  11350  pfxswrd  11353  swrdpfx  11354  pfxpfx  11355  lenrevpfxcctswrd  11359  wrdind  11369  wrd2ind  11370  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatpfx2  11384  pfxccatid  11388  cats1fvnd  11412  crim  11498  remullem  11511  remul2  11513  immul2  11520  ipcnval  11526  cjreim  11543  recvguniqlem  11634  resqrexlemover  11650  resqrexlemcalc1  11654  absid  11711  amgm2  11758  max0addsup  11859  minabs  11876  xrmaxrecl  11895  xrminadd  11915  fsumsplitf  12049  sumsnf  12050  fsump1i  12074  fsum2dlemstep  12075  fsumshftm  12086  fsummulc2  12089  modfsummodlemstep  12098  telfsumo  12107  fsumrelem  12112  hash2iun1dif1  12121  binomlem  12124  binom1dif  12128  arisum  12139  geo2sum  12155  geo2sum2  12156  cvgratz  12173  mertenslemi1  12176  clim2prod  12180  fprodeq0  12258  fprod2dlemstep  12263  fproddivap  12271  fproddivapf  12272  fprodmodd  12282  ef0lem  12301  eftlub  12331  efsep  12332  effsumlt  12333  tanval2ap  12354  efi4p  12358  resin4p  12359  recos4p  12360  efeul  12375  sinadd  12377  cosadd  12378  sinmul  12385  ef01bndlem  12397  cos12dec  12409  absef  12411  demoivreALT  12415  dvds2ln  12465  dvdseq  12489  opeo  12538  bezoutlemnewy  12647  nninfctlemfo  12691  eucalginv  12708  eucalglt  12709  eucalg  12711  lcmgcdlem  12729  lcm1  12733  divgcdcoprmex  12754  2sqpwodd  12828  zgcdsq  12853  qden1elz  12857  phiprmpw  12874  eulerthlem1  12879  eulerthlemrprm  12881  prmdiv  12887  hashgcdlem  12890  odzdvds  12898  vfermltl  12904  modprm0  12907  pythagtriplem12  12928  pcqmul  12956  pcaddlem  12992  pcadd  12993  pcadd2  12994  pcmpt  12996  pcmpt2  12997  mul4sqlem  13046  4sqlem11  13054  4sqlem17  13060  nninfdclemp1  13151  ressressg  13238  gsumsplit1r  13561  gsumprval  13562  mndinvmod  13608  mhmco  13653  gsumfzz  13658  grpinvid2  13716  grpasscan2  13727  grpinvssd  13740  grpinvadd  13741  grpsubid1  13748  grpsubadd  13751  grppncan  13754  mulg1  13796  mulgaddcomlem  13812  mulgdirlem  13820  mulgneg2  13823  mulgmodid  13828  nmzsubg  13877  qusinv  13903  qussub  13904  conjnmz  13946  ablsub2inv  13978  abladdsub4  13981  abladdsub  13982  ablpncan2  13983  ablpnpcan  13987  ablnncan  13988  invghm  13996  gsumfzconst  14008  gsumfzsnfd  14012  rngm2neg  14043  srgpcompp  14085  srgpcomppsc  14086  ringinvnzdiv  14144  ringm2neg  14149  dvr1  14233  dvrcan1  14235  dvrcan3  14236  rdivmuldivd  14239  lmodfopne  14422  sralemg  14534  gsumfzfsumlemm  14683  mplsubgfilemcl  14800  mplsubgfileminv  14801  xmetxpbl  15319  ivthinclemuopn  15449  limcimolemlt  15475  cnplimcim  15478  limccnpcntop  15486  limccnp2lem  15487  dvexp  15522  dvmptcmulcn  15532  dvply1  15576  ef2kpi  15617  sinhalfpip  15631  sinhalfpim  15632  coshalfpim  15634  ptolemy  15635  tangtx  15649  rpabscxpbnd  15751  relogbexpap  15769  rplogbcxp  15774  rpcxplogb  15775  binom4  15790  pellexlem2  15792  wilthlem1  15794  0sgm  15799  mpodvdsmulf1o  15804  fsumdvdsmul  15805  sgmppw  15806  0sgmppw  15807  1sgm2ppw  15809  perfectlem1  15813  perfectlem2  15814  perfect  15815  lgsval2lem  15829  lgsval4  15839  lgsval4a  15841  lgsneg  15843  lgsneg1  15844  lgsdirprm  15853  lgsdir  15854  lgsne0  15857  lgsmulsqcoprm  15865  gausslemma2dlem1a  15877  gausslemma2dlem6  15886  gausslemma2d  15888  lgseisenlem3  15891  lgseisenlem4  15892  lgseisen  15893  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem1  15900  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2lgslem3d1  15919  2sqlem3  15936  structiedg0val  15981  uhgr2edg  16147  usgr1e  16182  vtxdgfifival  16232  vtxdfifiun  16238  vtxdumgrfival  16239  vtxduspgrfvedgfi  16242  1loopgredg  16245  1loopgrvd2fi  16246  1hevtxdg1en  16249  p1evtxdeqfi  16253  edginwlkd  16296  clwwlknonex2lem1  16378  eupthvdres  16416  peano4nninf  16732  repiecele0  16758  repiecege0  16759  trilpolemclim  16768  trilpolemeq1  16772  apdifflemf  16778  gfsumval  16809  gfsumsn  16814