Theorem 3eqtrd 2275

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  tpeq123d  3803  diftpsn3  3856  oteq123d  3919  resiima  5145  fvun1  5769  fvmptd  5786  fmptpr  5907  caovlem2d  6282  offval  6310  ofvalg  6312  cnvf1olem  6460  supp0  6478  suppsnopdc  6490  suppofss1dcl  6504  suppofss2dcl  6505  suppcofn  6506  nnm1  6798  updjudhcoinlf  7420  updjudhcoinrg  7421  caseinl  7431  caseinr  7432  omp1eomlem  7434  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  ltexnqq  7775  prarloclemarch  7785  ltrnqg  7787  nq02m  7832  prarloclemcalc  7869  mulnqprl  7935  mulnqpru  7936  ltexprlemloc  7974  addcanprleml  7981  recexprlem1ssu  8001  cauappcvgprlem1  8026  caucvgsrlemfv  8158  caucvgsrlemoffval  8163  recidpirqlemcalc  8224  axmulass  8240  axrnegex  8246  muladd11r  8483  addcan2  8508  addsub  8538  subsub2  8555  negsubdi2  8586  muladd  8712  mulsub  8729  cru  8932  mulreim  8934  recextlem1  8981  mulap0  8984  muleqadd  9000  divrecap  9020  div23ap  9023  div12ap  9026  divmulasscomap  9028  divcanap7  9053  conjmulap  9061  apmul1  9120  nndivtr  9348  subhalfhalf  9544  xp1d2m1eqxm1d2  9562  div4p1lem1div2  9563  qapne  10048  xnegneg  10245  rexsub  10265  xnegid  10271  fseq1p1m1  10511  nn0split  10553  nnsplit  10554  fzosplitsnm1  10637  fzosplitpr  10662  fzosplitprm1  10663  ceilid  10765  flqdiv  10771  zmod10  10790  modqcyc  10809  modqaddabs  10812  mulqaddmodid  10814  modqadd2mod  10824  modqm1p1mod0  10825  modqmul12d  10828  modqadd12d  10830  modqmulmodr  10840  modqaddmulmod  10841  frecuzrdgsuc  10864  seqeq123d  10906  seqvalcd  10911  seq3f1olemqsumkj  10961  seq3f1oleml  10966  seqf1oglem2  10970  seq3id3  10974  seq3id  10975  seq3homo  10977  seq3z  10978  seqhomog  10980  exp1  10995  expnegap0  10997  expmulzap  11035  m1expeven  11036  expdivap  11040  binom3  11107  sqoddm1div8  11144  mulsubdivbinom2ap  11163  bcn1  11210  bcnp1n  11211  bcval5  11215  bcn2m1  11222  bcn2p1  11223  hashdifpr  11275  hashmap  11282  hashfibclem  11296  hashf1lem2  11300  ccatlen  11377  ccatalpha  11395  ccatw2s1leng  11420  ccats1val2  11422  lswccats1  11425  swrdlend  11444  ccatswrd  11456  pfxmpt  11466  pfxfv  11470  pfxfvlsw  11481  ccatpfx  11487  pfx1  11489  pfxswrd  11492  swrdpfx  11493  pfxpfx  11494  lenrevpfxcctswrd  11498  wrdind  11508  wrd2ind  11509  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatpfx2  11523  pfxccatid  11527  cats1fvnd  11551  crim  11637  remullem  11650  remul2  11652  immul2  11659  ipcnval  11665  cjreim  11683  recvguniqlem  11774  resqrexlemover  11790  resqrexlemcalc1  11794  absid  11851  amgm2  11899  max0addsup  12000  minabs  12017  xrmaxrecl  12037  xrminadd  12057  fsumsplitf  12191  sumsnf  12192  fsump1i  12216  fsum2dlemstep  12217  fsumshftm  12228  fsummulc2  12231  modfsummodlemstep  12240  telfsumo  12249  fsumrelem  12254  hash2iun1dif1  12263  binomlem  12266  binom1dif  12270  arisum  12281  geo2sum  12297  geo2sum2  12298  cvgratz  12315  mertenslemi1  12318  clim2prod  12322  fprodeq0  12400  fprod2dlemstep  12405  fproddivap  12413  fproddivapf  12414  fprodmodd  12424  ef0lem  12443  eftlub  12473  efsep  12474  effsumlt  12475  tanval2ap  12496  efi4p  12500  resin4p  12501  recos4p  12502  efeul  12517  sinadd  12519  cosadd  12520  sinmul  12527  ef01bndlem  12539  cos12dec  12551  absef  12553  demoivreALT  12557  dvds2ln  12607  dvdseq  12631  opeo  12680  bezoutlemnewy  12789  nninfctlemfo  12833  eucalginv  12850  eucalglt  12851  eucalg  12853  lcmgcdlem  12871  lcm1  12875  divgcdcoprmex  12896  2sqpwodd  12972  zgcdsq  12997  qden1elz  13001  phiprmpw  13020  eulerthlem1  13025  eulerthlemrprm  13027  prmdiv  13033  hashgcdlem  13036  odzdvds  13044  vfermltl  13050  modprm0  13053  pythagtriplem12  13074  pcqmul  13102  pcaddlem  13138  pcadd  13139  pcadd2  13140  pcmpt  13142  pcmpt2  13143  mul4sqlem  13192  4sqlem11  13200  4sqlem17  13206  ballotfilemfp1  13280  ballotfilemfmpn  13283  ballotfilemsi  13307  nninfdclemp1  13390  ressressg  13478  gzsumsplit1r  13764  mndinvmod  13807  mhmco  13846  grpinvid2  13907  grpasscan2  13918  grpinvssd  13931  grpinvadd  13932  grpsubid1  13939  grpsubadd  13942  grppncan  13945  mulg1  13981  mulgaddcomlem  13997  mulgdirlem  14005  mulgneg2  14008  mulgmodid  14013  nmzsubg  14062  qusinv  14088  qussub  14089  conjnmz  14131  ablsub2inv  14164  abladdsub4  14167  abladdsub  14168  ablpncan2  14169  ablpnpcan  14173  ablnncan  14174  invghm  14182  gzsumconst  14192  gzsumsnfd  14196  gsumvalfi  14201  gsumsncmn  14205  gsumzfi  14207  gsumf1ofi  14209  rngm2neg  14297  srgpcompp  14344  srgpcomppsc  14345  ringinvnzdiv  14404  ringm2neg  14409  dvr1  14494  dvrcan1  14496  dvrcan3  14497  rdivmuldivd  14500  lmodfopne  14712  sralemg  14824  assa2ass  15058  assa2ass2  15059  asclmul1  15078  asclmul2  15079  assamulgscmlem2  15091  mplsubgfilemcl  15139  mplsubgfileminv  15140  xmetxpbl  15658  ivthinclemuopn  15788  limcimolemlt  15814  cnplimcim  15817  limccnpcntop  15825  limccnp2lem  15826  dvexp  15861  dvmptcmulcn  15871  dvply1  15915  ef2kpi  15957  sinhalfpip  15971  sinhalfpim  15972  coshalfpim  15974  ptolemy  15975  tangtx  15989  rpabscxpbnd  16095  relogbexpap  16113  rplogbcxp  16118  rpcxplogb  16119  zprmlogbaplem2  16135  binom4  16138  log2tlbndlog2  16139  birthdaylem2  16145  pellexlem2  16149  wilthlem1  16151  0sgm  16166  ppidif  16175  mpodvdsmulf1o  16185  fsumdvdsmul  16186  sgmppw  16187  0sgmppw  16188  1sgm2ppw  16190  perfectlem1  16197  perfectlem2  16198  perfect  16199  bposlem5  16213  lgsval2lem  16227  lgsval4  16237  lgsval4a  16239  lgsneg  16241  lgsneg1  16242  lgsdirprm  16251  lgsdir  16252  lgsne0  16255  lgsmulsqcoprm  16263  gausslemma2dlem1a  16275  gausslemma2dlem6  16284  gausslemma2d  16286  lgseisenlem3  16289  lgseisenlem4  16290  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem1  16298  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgslem3d1  16317  2sqlem3  16334  structiedg0val  16379  uhgr2edg  16545  usgr1e  16580  vtxdgfifival  16630  vtxdfifiun  16636  vtxdumgrfival  16637  vtxduspgrfvedgfi  16640  1loopgredg  16643  1loopgrvd2fi  16644  1hevtxdg1en  16647  p1evtxdeqfi  16651  edginwlkd  16694  clwwlknonex2lem1  16776  eupthvdres  16814  peano4nninf  17147  repiecele0  17173  repiecege0  17174  trilpolemclim  17183  trilpolemeq1  17187  apdifflemf  17193