Theorem 3eqtrd 2244

Description: A deduction from three chained equalities. (Contributed by NM, 29-Oct-1995.)

Hypotheses

Ref	Expression
3eqtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)
3eqtrd.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
3eqtrd	⊢ (𝜑 → 𝐴 = 𝐷)

Proof of Theorem 3eqtrd

Step	Hyp	Ref	Expression
1		3eqtrd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3		3eqtrd.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	2, 3	eqtrd 2240	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	1, 4	eqtrd 2240	1 ⊢ (𝜑 → 𝐴 = 𝐷)

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  tpeq123d  3735  diftpsn3  3785  oteq123d  3848  resiima  5059  fvun1  5668  fvmptd  5683  fmptpr  5799  caovlem2d  6162  offval  6189  ofvalg  6191  cnvf1olem  6333  nnm1  6634  updjudhcoinlf  7208  updjudhcoinrg  7209  caseinl  7219  caseinr  7220  omp1eomlem  7222  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  ltexnqq  7556  prarloclemarch  7566  ltrnqg  7568  nq02m  7613  prarloclemcalc  7650  mulnqprl  7716  mulnqpru  7717  ltexprlemloc  7755  addcanprleml  7762  recexprlem1ssu  7782  cauappcvgprlem1  7807  caucvgsrlemfv  7939  caucvgsrlemoffval  7944  recidpirqlemcalc  8005  axmulass  8021  axrnegex  8027  muladd11r  8263  addcan2  8288  addsub  8318  subsub2  8335  negsubdi2  8366  muladd  8491  mulsub  8508  cru  8710  mulreim  8712  recextlem1  8759  mulap0  8762  muleqadd  8776  divrecap  8796  div23ap  8799  div12ap  8802  divmulasscomap  8804  divcanap7  8829  conjmulap  8837  apmul1  8896  nndivtr  9113  subhalfhalf  9307  xp1d2m1eqxm1d2  9325  div4p1lem1div2  9326  qapne  9795  xnegneg  9990  rexsub  10010  xnegid  10016  fseq1p1m1  10251  nn0split  10293  nnsplit  10294  fzosplitsnm1  10375  fzosplitprm1  10400  ceilid  10497  flqdiv  10503  zmod10  10522  modqcyc  10541  modqaddabs  10544  mulqaddmodid  10546  modqadd2mod  10556  modqm1p1mod0  10557  modqmul12d  10560  modqadd12d  10562  modqmulmodr  10572  modqaddmulmod  10573  frecuzrdgsuc  10596  seqeq123d  10638  seqvalcd  10643  seq3f1olemqsumkj  10693  seq3f1oleml  10698  seqf1oglem2  10702  seq3id3  10706  seq3id  10707  seq3homo  10709  seq3z  10710  seqhomog  10712  exp1  10727  expnegap0  10729  expmulzap  10767  m1expeven  10768  expdivap  10772  binom3  10839  sqoddm1div8  10875  mulsubdivbinom2ap  10893  bcn1  10940  bcnp1n  10941  bcval5  10945  bcn2m1  10951  bcn2p1  10952  hashdifpr  11002  ccatlen  11089  ccats1val2  11130  lswccats1  11133  swrdlend  11149  ccatswrd  11161  pfxmpt  11171  pfxfv  11175  pfxfvlsw  11186  ccatpfx  11192  pfx1  11194  pfxswrd  11197  swrdpfx  11198  pfxpfx  11199  lenrevpfxcctswrd  11203  wrdind  11213  wrd2ind  11214  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatpfx2  11228  pfxccatid  11232  crim  11284  remullem  11297  remul2  11299  immul2  11306  ipcnval  11312  cjreim  11329  recvguniqlem  11420  resqrexlemover  11436  resqrexlemcalc1  11440  absid  11497  amgm2  11544  max0addsup  11645  minabs  11662  xrmaxrecl  11681  xrminadd  11701  fsumsplitf  11834  sumsnf  11835  fsump1i  11859  fsum2dlemstep  11860  fsumshftm  11871  fsummulc2  11874  modfsummodlemstep  11883  telfsumo  11892  fsumrelem  11897  hash2iun1dif1  11906  binomlem  11909  binom1dif  11913  arisum  11924  geo2sum  11940  geo2sum2  11941  cvgratz  11958  mertenslemi1  11961  clim2prod  11965  fprodeq0  12043  fprod2dlemstep  12048  fproddivap  12056  fproddivapf  12057  fprodmodd  12067  ef0lem  12086  eftlub  12116  efsep  12117  effsumlt  12118  tanval2ap  12139  efi4p  12143  resin4p  12144  recos4p  12145  efeul  12160  sinadd  12162  cosadd  12163  sinmul  12170  ef01bndlem  12182  cos12dec  12194  absef  12196  demoivreALT  12200  dvds2ln  12250  dvdseq  12274  opeo  12323  bezoutlemnewy  12432  nninfctlemfo  12476  eucalginv  12493  eucalglt  12494  eucalg  12496  lcmgcdlem  12514  lcm1  12518  divgcdcoprmex  12539  2sqpwodd  12613  zgcdsq  12638  qden1elz  12642  phiprmpw  12659  eulerthlem1  12664  eulerthlemrprm  12666  prmdiv  12672  hashgcdlem  12675  odzdvds  12683  vfermltl  12689  modprm0  12692  pythagtriplem12  12713  pcqmul  12741  pcaddlem  12777  pcadd  12778  pcadd2  12779  pcmpt  12781  pcmpt2  12782  mul4sqlem  12831  4sqlem11  12839  4sqlem17  12845  nninfdclemp1  12936  ressressg  13022  gsumsplit1r  13345  gsumprval  13346  mndinvmod  13392  mhmco  13437  gsumfzz  13442  grpinvid2  13500  grpasscan2  13511  grpinvssd  13524  grpinvadd  13525  grpsubid1  13532  grpsubadd  13535  grppncan  13538  mulg1  13580  mulgaddcomlem  13596  mulgdirlem  13604  mulgneg2  13607  mulgmodid  13612  nmzsubg  13661  qusinv  13687  qussub  13688  conjnmz  13730  ablsub2inv  13762  abladdsub4  13765  abladdsub  13766  ablpncan2  13767  ablpnpcan  13771  ablnncan  13772  invghm  13780  gsumfzconst  13792  gsumfzsnfd  13796  rngm2neg  13826  srgpcompp  13868  srgpcomppsc  13869  ringinvnzdiv  13927  ringm2neg  13932  dvr1  14015  dvrcan1  14017  dvrcan3  14018  rdivmuldivd  14021  lmodfopne  14203  sralemg  14315  gsumfzfsumlemm  14464  mplsubgfilemcl  14576  mplsubgfileminv  14577  xmetxpbl  15095  ivthinclemuopn  15225  limcimolemlt  15251  cnplimcim  15254  limccnpcntop  15262  limccnp2lem  15263  dvexp  15298  dvmptcmulcn  15308  dvply1  15352  ef2kpi  15393  sinhalfpip  15407  sinhalfpim  15408  coshalfpim  15410  ptolemy  15411  tangtx  15425  rpabscxpbnd  15527  relogbexpap  15545  rplogbcxp  15550  rpcxplogb  15551  binom4  15566  wilthlem1  15567  0sgm  15572  mpodvdsmulf1o  15577  fsumdvdsmul  15578  sgmppw  15579  0sgmppw  15580  1sgm2ppw  15582  perfectlem1  15586  perfectlem2  15587  perfect  15588  lgsval2lem  15602  lgsval4  15612  lgsval4a  15614  lgsneg  15616  lgsneg1  15617  lgsdirprm  15626  lgsdir  15627  lgsne0  15630  lgsmulsqcoprm  15638  gausslemma2dlem1a  15650  gausslemma2dlem6  15659  gausslemma2d  15661  lgseisenlem3  15664  lgseisenlem4  15665  lgseisen  15666  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem1  15673  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgslem3d1  15692  2sqlem3  15709  structiedg0val  15754  peano4nninf  16145  trilpolemclim  16177  trilpolemeq1  16181  apdifflemf  16187