Theorem 3eqtrd 2212

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 2208	. 2 |- ( ph -> B = D )
5	1, 4	eqtrd 2208	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 1445  ax-gen 1447  ax-4 1508  ax-17 1524  ax-ext 2157

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

This theorem is referenced by:  tpeq123d  3681  diftpsn3  3730  oteq123d  3789  resiima  4979  fvun1  5574  fvmptd  5589  fmptpr  5700  caovlem2d  6057  offval  6080  ofvalg  6082  cnvf1olem  6215  nnm1  6516  updjudhcoinlf  7069  updjudhcoinrg  7070  caseinl  7080  caseinr  7081  omp1eomlem  7083  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  ltexnqq  7382  prarloclemarch  7392  ltrnqg  7394  nq02m  7439  prarloclemcalc  7476  mulnqprl  7542  mulnqpru  7543  ltexprlemloc  7581  addcanprleml  7588  recexprlem1ssu  7608  cauappcvgprlem1  7633  caucvgsrlemfv  7765  caucvgsrlemoffval  7770  recidpirqlemcalc  7831  axmulass  7847  axrnegex  7853  muladd11r  8087  addcan2  8112  addsub  8142  subsub2  8159  negsubdi2  8190  muladd  8315  mulsub  8332  cru  8533  mulreim  8535  recextlem1  8581  mulap0  8584  muleqadd  8598  divrecap  8618  div23ap  8621  div12ap  8624  divmulasscomap  8626  divcanap7  8651  conjmulap  8659  apmul1  8718  nndivtr  8934  xp1d2m1eqxm1d2  9144  div4p1lem1div2  9145  qapne  9612  xnegneg  9804  rexsub  9824  xnegid  9830  fseq1p1m1  10064  nn0split  10106  nnsplit  10107  fzosplitsnm1  10179  fzosplitprm1  10204  ceilid  10285  flqdiv  10291  zmod10  10310  modqcyc  10329  modqaddabs  10332  mulqaddmodid  10334  modqadd2mod  10344  modqm1p1mod0  10345  modqmul12d  10348  modqadd12d  10350  modqmulmodr  10360  modqaddmulmod  10361  frecuzrdgsuc  10384  seqeq123d  10424  seqvalcd  10429  seq3f1olemqsumkj  10468  seq3f1oleml  10473  seq3id3  10477  seq3id  10478  seq3homo  10480  seq3z  10481  exp1  10496  expnegap0  10498  expmulzap  10536  m1expeven  10537  expdivap  10541  binom3  10607  sqoddm1div8  10643  bcn1  10706  bcnp1n  10707  bcval5  10711  bcn2m1  10717  bcn2p1  10718  hashdifpr  10768  crim  10835  remullem  10848  remul2  10850  immul2  10857  ipcnval  10863  cjreim  10880  recvguniqlem  10971  resqrexlemover  10987  resqrexlemcalc1  10991  absid  11048  amgm2  11095  max0addsup  11196  minabs  11212  xrmaxrecl  11231  xrminadd  11251  fsumsplitf  11384  sumsnf  11385  fsump1i  11409  fsum2dlemstep  11410  fsumshftm  11421  fsummulc2  11424  modfsummodlemstep  11433  telfsumo  11442  fsumrelem  11447  hash2iun1dif1  11456  binomlem  11459  binom1dif  11463  arisum  11474  geo2sum  11490  geo2sum2  11491  cvgratz  11508  mertenslemi1  11511  clim2prod  11515  fprodeq0  11593  fprod2dlemstep  11598  fproddivap  11606  fproddivapf  11607  fprodmodd  11617  ef0lem  11636  eftlub  11666  efsep  11667  effsumlt  11668  tanval2ap  11689  efi4p  11693  resin4p  11694  recos4p  11695  efeul  11710  sinadd  11712  cosadd  11713  sinmul  11720  ef01bndlem  11732  cos12dec  11743  absef  11745  demoivreALT  11749  dvds2ln  11799  dvdseq  11821  opeo  11869  bezoutlemnewy  11964  eucalginv  12023  eucalglt  12024  eucalg  12026  lcmgcdlem  12044  lcm1  12048  divgcdcoprmex  12069  2sqpwodd  12143  zgcdsq  12168  qden1elz  12172  phiprmpw  12189  eulerthlem1  12194  eulerthlemrprm  12196  prmdiv  12202  hashgcdlem  12205  odzdvds  12212  vfermltl  12218  modprm0  12221  pythagtriplem12  12242  pcqmul  12270  pcaddlem  12305  pcadd  12306  pcmpt  12308  pcmpt2  12309  mul4sqlem  12358  nninfdclemp1  12418  mndinvmod  12709  mhmco  12736  grpinvid2  12787  grpasscan2  12795  grpinvssd  12808  grpinvadd  12809  grpsubid1  12816  grpsubadd  12819  grppncan  12822  mulg1  12851  mulgaddcomlem  12866  mulgdirlem  12874  mulgneg2  12877  mulgmodid  12882  ablsub2inv  12913  abladdsub4  12916  abladdsub  12917  ablpncan2  12918  ablpnpcan  12922  ablnncan  12923  srgpcompp  12971  srgpcomppsc  12972  ringinvnzdiv  13023  ringm2neg  13028  xmetxpbl  13579  ivthinclemuopn  13687  limcimolemlt  13704  cnplimcim  13707  limccnpcntop  13715  limccnp2lem  13716  dvexp  13746  dvmptcmulcn  13754  ef2kpi  13798  sinhalfpip  13812  sinhalfpim  13813  coshalfpim  13815  ptolemy  13816  tangtx  13830  rpabscxpbnd  13930  relogbexpap  13947  rplogbcxp  13952  rpcxplogb  13953  binom4  13968  lgsval2lem  13982  lgsval4  13992  lgsval4a  13994  lgsneg  13996  lgsneg1  13997  lgsdirprm  14006  lgsdir  14007  lgsne0  14010  lgsmulsqcoprm  14018  2sqlem3  14024  peano4nninf  14316  trilpolemclim  14345  trilpolemeq1  14349  apdifflemf  14355