Theorem 3eqtrd 2226

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

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

This theorem is referenced by:  tpeq123d  3699  diftpsn3  3748  oteq123d  3808  resiima  5004  fvun1  5603  fvmptd  5618  fmptpr  5729  caovlem2d  6090  offval  6115  ofvalg  6117  cnvf1olem  6250  nnm1  6551  updjudhcoinlf  7110  updjudhcoinrg  7111  caseinl  7121  caseinr  7122  omp1eomlem  7124  exmidfodomrlemr  7232  exmidfodomrlemrALT  7233  ltexnqq  7438  prarloclemarch  7448  ltrnqg  7450  nq02m  7495  prarloclemcalc  7532  mulnqprl  7598  mulnqpru  7599  ltexprlemloc  7637  addcanprleml  7644  recexprlem1ssu  7664  cauappcvgprlem1  7689  caucvgsrlemfv  7821  caucvgsrlemoffval  7826  recidpirqlemcalc  7887  axmulass  7903  axrnegex  7909  muladd11r  8144  addcan2  8169  addsub  8199  subsub2  8216  negsubdi2  8247  muladd  8372  mulsub  8389  cru  8590  mulreim  8592  recextlem1  8639  mulap0  8642  muleqadd  8656  divrecap  8676  div23ap  8679  div12ap  8682  divmulasscomap  8684  divcanap7  8709  conjmulap  8717  apmul1  8776  nndivtr  8992  xp1d2m1eqxm1d2  9202  div4p1lem1div2  9203  qapne  9671  xnegneg  9865  rexsub  9885  xnegid  9891  fseq1p1m1  10126  nn0split  10168  nnsplit  10169  fzosplitsnm1  10241  fzosplitprm1  10266  ceilid  10348  flqdiv  10354  zmod10  10373  modqcyc  10392  modqaddabs  10395  mulqaddmodid  10397  modqadd2mod  10407  modqm1p1mod0  10408  modqmul12d  10411  modqadd12d  10413  modqmulmodr  10423  modqaddmulmod  10424  frecuzrdgsuc  10447  seqeq123d  10487  seqvalcd  10492  seq3f1olemqsumkj  10531  seq3f1oleml  10536  seq3id3  10540  seq3id  10541  seq3homo  10543  seq3z  10544  exp1  10560  expnegap0  10562  expmulzap  10600  m1expeven  10601  expdivap  10605  binom3  10672  sqoddm1div8  10708  mulsubdivbinom2ap  10726  bcn1  10773  bcnp1n  10774  bcval5  10778  bcn2m1  10784  bcn2p1  10785  hashdifpr  10835  crim  10902  remullem  10915  remul2  10917  immul2  10924  ipcnval  10930  cjreim  10947  recvguniqlem  11038  resqrexlemover  11054  resqrexlemcalc1  11058  absid  11115  amgm2  11162  max0addsup  11263  minabs  11279  xrmaxrecl  11298  xrminadd  11318  fsumsplitf  11451  sumsnf  11452  fsump1i  11476  fsum2dlemstep  11477  fsumshftm  11488  fsummulc2  11491  modfsummodlemstep  11500  telfsumo  11509  fsumrelem  11514  hash2iun1dif1  11523  binomlem  11526  binom1dif  11530  arisum  11541  geo2sum  11557  geo2sum2  11558  cvgratz  11575  mertenslemi1  11578  clim2prod  11582  fprodeq0  11660  fprod2dlemstep  11665  fproddivap  11673  fproddivapf  11674  fprodmodd  11684  ef0lem  11703  eftlub  11733  efsep  11734  effsumlt  11735  tanval2ap  11756  efi4p  11760  resin4p  11761  recos4p  11762  efeul  11777  sinadd  11779  cosadd  11780  sinmul  11787  ef01bndlem  11799  cos12dec  11810  absef  11812  demoivreALT  11816  dvds2ln  11866  dvdseq  11889  opeo  11937  bezoutlemnewy  12032  eucalginv  12091  eucalglt  12092  eucalg  12094  lcmgcdlem  12112  lcm1  12116  divgcdcoprmex  12137  2sqpwodd  12211  zgcdsq  12236  qden1elz  12240  phiprmpw  12257  eulerthlem1  12262  eulerthlemrprm  12264  prmdiv  12270  hashgcdlem  12273  odzdvds  12280  vfermltl  12286  modprm0  12289  pythagtriplem12  12310  pcqmul  12338  pcaddlem  12374  pcadd  12375  pcadd2  12376  pcmpt  12378  pcmpt2  12379  mul4sqlem  12428  4sqlem11  12436  4sqlem17  12442  nninfdclemp1  12504  ressressg  12590  gsumsplit1r  12876  gsumprval  12877  mndinvmod  12921  mhmco  12957  grpinvid2  13012  grpasscan2  13023  grpinvssd  13036  grpinvadd  13037  grpsubid1  13044  grpsubadd  13047  grppncan  13050  mulg1  13086  mulgaddcomlem  13102  mulgdirlem  13110  mulgneg2  13113  mulgmodid  13118  nmzsubg  13166  qusinv  13192  qussub  13193  conjnmz  13235  ablsub2inv  13267  abladdsub4  13270  abladdsub  13271  ablpncan2  13272  ablpnpcan  13276  ablnncan  13277  rngm2neg  13320  srgpcompp  13362  srgpcomppsc  13363  ringinvnzdiv  13419  ringm2neg  13424  dvr1  13505  dvrcan1  13507  dvrcan3  13508  rdivmuldivd  13511  lmodfopne  13659  sralemg  13771  xmetxpbl  14485  ivthinclemuopn  14593  limcimolemlt  14610  cnplimcim  14613  limccnpcntop  14621  limccnp2lem  14622  dvexp  14652  dvmptcmulcn  14660  ef2kpi  14704  sinhalfpip  14718  sinhalfpim  14719  coshalfpim  14721  ptolemy  14722  tangtx  14736  rpabscxpbnd  14836  relogbexpap  14853  rplogbcxp  14858  rpcxplogb  14859  binom4  14874  wilthlem1  14875  lgsval2lem  14889  lgsval4  14899  lgsval4a  14901  lgsneg  14903  lgsneg1  14904  lgsdirprm  14913  lgsdir  14914  lgsne0  14917  lgsmulsqcoprm  14925  2sqlem3  14942  peano4nninf  15234  trilpolemclim  15263  trilpolemeq1  15267  apdifflemf  15273