Theorem 3eqtrd 2230

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

Syntax hints:   -> wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  tpeq123d  3711  diftpsn3  3760  oteq123d  3820  resiima  5024  fvun1  5624  fvmptd  5639  fmptpr  5751  caovlem2d  6113  offval  6140  ofvalg  6142  cnvf1olem  6279  nnm1  6580  updjudhcoinlf  7141  updjudhcoinrg  7142  caseinl  7152  caseinr  7153  omp1eomlem  7155  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  ltexnqq  7470  prarloclemarch  7480  ltrnqg  7482  nq02m  7527  prarloclemcalc  7564  mulnqprl  7630  mulnqpru  7631  ltexprlemloc  7669  addcanprleml  7676  recexprlem1ssu  7696  cauappcvgprlem1  7721  caucvgsrlemfv  7853  caucvgsrlemoffval  7858  recidpirqlemcalc  7919  axmulass  7935  axrnegex  7941  muladd11r  8177  addcan2  8202  addsub  8232  subsub2  8249  negsubdi2  8280  muladd  8405  mulsub  8422  cru  8623  mulreim  8625  recextlem1  8672  mulap0  8675  muleqadd  8689  divrecap  8709  div23ap  8712  div12ap  8715  divmulasscomap  8717  divcanap7  8742  conjmulap  8750  apmul1  8809  nndivtr  9026  subhalfhalf  9220  xp1d2m1eqxm1d2  9238  div4p1lem1div2  9239  qapne  9707  xnegneg  9902  rexsub  9922  xnegid  9928  fseq1p1m1  10163  nn0split  10205  nnsplit  10206  fzosplitsnm1  10279  fzosplitprm1  10304  ceilid  10389  flqdiv  10395  zmod10  10414  modqcyc  10433  modqaddabs  10436  mulqaddmodid  10438  modqadd2mod  10448  modqm1p1mod0  10449  modqmul12d  10452  modqadd12d  10454  modqmulmodr  10464  modqaddmulmod  10465  frecuzrdgsuc  10488  seqeq123d  10530  seqvalcd  10535  seq3f1olemqsumkj  10585  seq3f1oleml  10590  seqf1oglem2  10594  seq3id3  10598  seq3id  10599  seq3homo  10601  seq3z  10602  seqhomog  10604  exp1  10619  expnegap0  10621  expmulzap  10659  m1expeven  10660  expdivap  10664  binom3  10731  sqoddm1div8  10767  mulsubdivbinom2ap  10785  bcn1  10832  bcnp1n  10833  bcval5  10837  bcn2m1  10843  bcn2p1  10844  hashdifpr  10894  crim  11005  remullem  11018  remul2  11020  immul2  11027  ipcnval  11033  cjreim  11050  recvguniqlem  11141  resqrexlemover  11157  resqrexlemcalc1  11161  absid  11218  amgm2  11265  max0addsup  11366  minabs  11382  xrmaxrecl  11401  xrminadd  11421  fsumsplitf  11554  sumsnf  11555  fsump1i  11579  fsum2dlemstep  11580  fsumshftm  11591  fsummulc2  11594  modfsummodlemstep  11603  telfsumo  11612  fsumrelem  11617  hash2iun1dif1  11626  binomlem  11629  binom1dif  11633  arisum  11644  geo2sum  11660  geo2sum2  11661  cvgratz  11678  mertenslemi1  11681  clim2prod  11685  fprodeq0  11763  fprod2dlemstep  11768  fproddivap  11776  fproddivapf  11777  fprodmodd  11787  ef0lem  11806  eftlub  11836  efsep  11837  effsumlt  11838  tanval2ap  11859  efi4p  11863  resin4p  11864  recos4p  11865  efeul  11880  sinadd  11882  cosadd  11883  sinmul  11890  ef01bndlem  11902  cos12dec  11914  absef  11916  demoivreALT  11920  dvds2ln  11970  dvdseq  11993  opeo  12041  bezoutlemnewy  12136  nninfctlemfo  12180  eucalginv  12197  eucalglt  12198  eucalg  12200  lcmgcdlem  12218  lcm1  12222  divgcdcoprmex  12243  2sqpwodd  12317  zgcdsq  12342  qden1elz  12346  phiprmpw  12363  eulerthlem1  12368  eulerthlemrprm  12370  prmdiv  12376  hashgcdlem  12379  odzdvds  12386  vfermltl  12392  modprm0  12395  pythagtriplem12  12416  pcqmul  12444  pcaddlem  12480  pcadd  12481  pcadd2  12482  pcmpt  12484  pcmpt2  12485  mul4sqlem  12534  4sqlem11  12542  4sqlem17  12548  nninfdclemp1  12610  ressressg  12696  gsumsplit1r  12984  gsumprval  12985  mndinvmod  13029  mhmco  13065  gsumfzz  13070  grpinvid2  13128  grpasscan2  13139  grpinvssd  13152  grpinvadd  13153  grpsubid1  13160  grpsubadd  13163  grppncan  13166  mulg1  13202  mulgaddcomlem  13218  mulgdirlem  13226  mulgneg2  13229  mulgmodid  13234  nmzsubg  13283  qusinv  13309  qussub  13310  conjnmz  13352  ablsub2inv  13384  abladdsub4  13387  abladdsub  13388  ablpncan2  13389  ablpnpcan  13393  ablnncan  13394  invghm  13402  gsumfzconst  13414  gsumfzsnfd  13418  rngm2neg  13448  srgpcompp  13490  srgpcomppsc  13491  ringinvnzdiv  13549  ringm2neg  13554  dvr1  13637  dvrcan1  13639  dvrcan3  13640  rdivmuldivd  13643  lmodfopne  13825  sralemg  13937  gsumfzfsumlemm  14086  xmetxpbl  14687  ivthinclemuopn  14817  limcimolemlt  14843  cnplimcim  14846  limccnpcntop  14854  limccnp2lem  14855  dvexp  14890  dvmptcmulcn  14900  dvply1  14943  ef2kpi  14982  sinhalfpip  14996  sinhalfpim  14997  coshalfpim  14999  ptolemy  15000  tangtx  15014  rpabscxpbnd  15114  relogbexpap  15131  rplogbcxp  15136  rpcxplogb  15137  binom4  15152  wilthlem1  15153  lgsval2lem  15167  lgsval4  15177  lgsval4a  15179  lgsneg  15181  lgsneg1  15182  lgsdirprm  15191  lgsdir  15192  lgsne0  15195  lgsmulsqcoprm  15203  gausslemma2dlem1a  15215  gausslemma2dlem6  15224  gausslemma2d  15226  lgseisenlem3  15229  lgseisenlem4  15230  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem1  15238  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgslem3d1  15257  2sqlem3  15274  peano4nninf  15566  trilpolemclim  15596  trilpolemeq1  15600  apdifflemf  15606