Theorem 3eqtrd 2214

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  tpeq123d  3686  diftpsn3  3735  oteq123d  3795  resiima  4988  fvun1  5584  fvmptd  5599  fmptpr  5710  caovlem2d  6069  offval  6092  ofvalg  6094  cnvf1olem  6227  nnm1  6528  updjudhcoinlf  7081  updjudhcoinrg  7082  caseinl  7092  caseinr  7093  omp1eomlem  7095  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  ltexnqq  7409  prarloclemarch  7419  ltrnqg  7421  nq02m  7466  prarloclemcalc  7503  mulnqprl  7569  mulnqpru  7570  ltexprlemloc  7608  addcanprleml  7615  recexprlem1ssu  7635  cauappcvgprlem1  7660  caucvgsrlemfv  7792  caucvgsrlemoffval  7797  recidpirqlemcalc  7858  axmulass  7874  axrnegex  7880  muladd11r  8115  addcan2  8140  addsub  8170  subsub2  8187  negsubdi2  8218  muladd  8343  mulsub  8360  cru  8561  mulreim  8563  recextlem1  8610  mulap0  8613  muleqadd  8627  divrecap  8647  div23ap  8650  div12ap  8653  divmulasscomap  8655  divcanap7  8680  conjmulap  8688  apmul1  8747  nndivtr  8963  xp1d2m1eqxm1d2  9173  div4p1lem1div2  9174  qapne  9641  xnegneg  9835  rexsub  9855  xnegid  9861  fseq1p1m1  10096  nn0split  10138  nnsplit  10139  fzosplitsnm1  10211  fzosplitprm1  10236  ceilid  10317  flqdiv  10323  zmod10  10342  modqcyc  10361  modqaddabs  10364  mulqaddmodid  10366  modqadd2mod  10376  modqm1p1mod0  10377  modqmul12d  10380  modqadd12d  10382  modqmulmodr  10392  modqaddmulmod  10393  frecuzrdgsuc  10416  seqeq123d  10456  seqvalcd  10461  seq3f1olemqsumkj  10500  seq3f1oleml  10505  seq3id3  10509  seq3id  10510  seq3homo  10512  seq3z  10513  exp1  10528  expnegap0  10530  expmulzap  10568  m1expeven  10569  expdivap  10573  binom3  10640  sqoddm1div8  10676  mulsubdivbinom2ap  10693  bcn1  10740  bcnp1n  10741  bcval5  10745  bcn2m1  10751  bcn2p1  10752  hashdifpr  10802  crim  10869  remullem  10882  remul2  10884  immul2  10891  ipcnval  10897  cjreim  10914  recvguniqlem  11005  resqrexlemover  11021  resqrexlemcalc1  11025  absid  11082  amgm2  11129  max0addsup  11230  minabs  11246  xrmaxrecl  11265  xrminadd  11285  fsumsplitf  11418  sumsnf  11419  fsump1i  11443  fsum2dlemstep  11444  fsumshftm  11455  fsummulc2  11458  modfsummodlemstep  11467  telfsumo  11476  fsumrelem  11481  hash2iun1dif1  11490  binomlem  11493  binom1dif  11497  arisum  11508  geo2sum  11524  geo2sum2  11525  cvgratz  11542  mertenslemi1  11545  clim2prod  11549  fprodeq0  11627  fprod2dlemstep  11632  fproddivap  11640  fproddivapf  11641  fprodmodd  11651  ef0lem  11670  eftlub  11700  efsep  11701  effsumlt  11702  tanval2ap  11723  efi4p  11727  resin4p  11728  recos4p  11729  efeul  11744  sinadd  11746  cosadd  11747  sinmul  11754  ef01bndlem  11766  cos12dec  11777  absef  11779  demoivreALT  11783  dvds2ln  11833  dvdseq  11856  opeo  11904  bezoutlemnewy  11999  eucalginv  12058  eucalglt  12059  eucalg  12061  lcmgcdlem  12079  lcm1  12083  divgcdcoprmex  12104  2sqpwodd  12178  zgcdsq  12203  qden1elz  12207  phiprmpw  12224  eulerthlem1  12229  eulerthlemrprm  12231  prmdiv  12237  hashgcdlem  12240  odzdvds  12247  vfermltl  12253  modprm0  12256  pythagtriplem12  12277  pcqmul  12305  pcaddlem  12340  pcadd  12341  pcmpt  12343  pcmpt2  12344  mul4sqlem  12393  nninfdclemp1  12453  ressressg  12536  mndinvmod  12851  mhmco  12879  grpinvid2  12930  grpasscan2  12939  grpinvssd  12952  grpinvadd  12953  grpsubid1  12960  grpsubadd  12963  grppncan  12966  mulg1  12995  mulgaddcomlem  13011  mulgdirlem  13019  mulgneg2  13022  mulgmodid  13027  nmzsubg  13075  ablsub2inv  13119  abladdsub4  13122  abladdsub  13123  ablpncan2  13124  ablpnpcan  13128  ablnncan  13129  srgpcompp  13179  srgpcomppsc  13180  ringinvnzdiv  13232  ringm2neg  13237  dvr1  13312  dvrcan1  13314  dvrcan3  13315  rdivmuldivd  13318  lmodfopne  13421  xmetxpbl  14047  ivthinclemuopn  14155  limcimolemlt  14172  cnplimcim  14175  limccnpcntop  14183  limccnp2lem  14184  dvexp  14214  dvmptcmulcn  14222  ef2kpi  14266  sinhalfpip  14280  sinhalfpim  14281  coshalfpim  14283  ptolemy  14284  tangtx  14298  rpabscxpbnd  14398  relogbexpap  14415  rplogbcxp  14420  rpcxplogb  14421  binom4  14436  lgsval2lem  14450  lgsval4  14460  lgsval4a  14462  lgsneg  14464  lgsneg1  14465  lgsdirprm  14474  lgsdir  14475  lgsne0  14478  lgsmulsqcoprm  14486  2sqlem3  14503  peano4nninf  14794  trilpolemclim  14823  trilpolemeq1  14827  apdifflemf  14833