Theorem 3eqtrd 2271

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 2267	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	1, 4	eqtrd 2267	1 ⊢ (𝜑 → 𝐴 = 𝐷)

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  tpeq123d  3788  diftpsn3  3840  oteq123d  3903  resiima  5125  fvun1  5748  fvmptd  5763  fmptpr  5881  caovlem2d  6255  offval  6283  ofvalg  6285  cnvf1olem  6433  supp0  6451  suppsnopdc  6463  suppofss1dcl  6477  suppofss2dcl  6478  suppcofn  6479  nnm1  6771  updjudhcoinlf  7384  updjudhcoinrg  7385  caseinl  7395  caseinr  7396  omp1eomlem  7398  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  ltexnqq  7739  prarloclemarch  7749  ltrnqg  7751  nq02m  7796  prarloclemcalc  7833  mulnqprl  7899  mulnqpru  7900  ltexprlemloc  7938  addcanprleml  7945  recexprlem1ssu  7965  cauappcvgprlem1  7990  caucvgsrlemfv  8122  caucvgsrlemoffval  8127  recidpirqlemcalc  8188  axmulass  8204  axrnegex  8210  muladd11r  8445  addcan2  8470  addsub  8500  subsub2  8517  negsubdi2  8548  muladd  8674  mulsub  8691  cru  8893  mulreim  8895  recextlem1  8942  mulap0  8945  muleqadd  8959  divrecap  8979  div23ap  8982  div12ap  8985  divmulasscomap  8987  divcanap7  9012  conjmulap  9020  apmul1  9079  nndivtr  9296  subhalfhalf  9490  xp1d2m1eqxm1d2  9508  div4p1lem1div2  9509  qapne  9989  xnegneg  10185  rexsub  10205  xnegid  10211  fseq1p1m1  10450  nn0split  10492  nnsplit  10493  fzosplitsnm1  10576  fzosplitpr  10601  fzosplitprm1  10602  ceilid  10701  flqdiv  10707  zmod10  10726  modqcyc  10745  modqaddabs  10748  mulqaddmodid  10750  modqadd2mod  10760  modqm1p1mod0  10761  modqmul12d  10764  modqadd12d  10766  modqmulmodr  10776  modqaddmulmod  10777  frecuzrdgsuc  10800  seqeq123d  10842  seqvalcd  10847  seq3f1olemqsumkj  10897  seq3f1oleml  10902  seqf1oglem2  10906  seq3id3  10910  seq3id  10911  seq3homo  10913  seq3z  10914  seqhomog  10916  exp1  10931  expnegap0  10933  expmulzap  10971  m1expeven  10972  expdivap  10976  binom3  11043  sqoddm1div8  11080  mulsubdivbinom2ap  11098  bcn1  11145  bcnp1n  11146  bcval5  11150  bcn2m1  11157  bcn2p1  11158  hashdifpr  11210  hashmap  11217  hashfibclem  11231  ccatlen  11308  ccatalpha  11326  ccatw2s1leng  11351  ccats1val2  11353  lswccats1  11356  swrdlend  11375  ccatswrd  11387  pfxmpt  11397  pfxfv  11401  pfxfvlsw  11412  ccatpfx  11418  pfx1  11420  pfxswrd  11423  swrdpfx  11424  pfxpfx  11425  lenrevpfxcctswrd  11429  wrdind  11439  wrd2ind  11440  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatpfx2  11454  pfxccatid  11458  cats1fvnd  11482  crim  11568  remullem  11581  remul2  11583  immul2  11590  ipcnval  11596  cjreim  11613  recvguniqlem  11704  resqrexlemover  11720  resqrexlemcalc1  11724  absid  11781  amgm2  11828  max0addsup  11929  minabs  11946  xrmaxrecl  11965  xrminadd  11985  fsumsplitf  12119  sumsnf  12120  fsump1i  12144  fsum2dlemstep  12145  fsumshftm  12156  fsummulc2  12159  modfsummodlemstep  12168  telfsumo  12177  fsumrelem  12182  hash2iun1dif1  12191  binomlem  12194  binom1dif  12198  arisum  12209  geo2sum  12225  geo2sum2  12226  cvgratz  12243  mertenslemi1  12246  clim2prod  12250  fprodeq0  12328  fprod2dlemstep  12333  fproddivap  12341  fproddivapf  12342  fprodmodd  12352  ef0lem  12371  eftlub  12401  efsep  12402  effsumlt  12403  tanval2ap  12424  efi4p  12428  resin4p  12429  recos4p  12430  efeul  12445  sinadd  12447  cosadd  12448  sinmul  12455  ef01bndlem  12467  cos12dec  12479  absef  12481  demoivreALT  12485  dvds2ln  12535  dvdseq  12559  opeo  12608  bezoutlemnewy  12717  nninfctlemfo  12761  eucalginv  12778  eucalglt  12779  eucalg  12781  lcmgcdlem  12799  lcm1  12803  divgcdcoprmex  12824  2sqpwodd  12898  zgcdsq  12923  qden1elz  12927  phiprmpw  12944  eulerthlem1  12949  eulerthlemrprm  12951  prmdiv  12957  hashgcdlem  12960  odzdvds  12968  vfermltl  12974  modprm0  12977  pythagtriplem12  12998  pcqmul  13026  pcaddlem  13062  pcadd  13063  pcadd2  13064  pcmpt  13066  pcmpt2  13067  mul4sqlem  13116  4sqlem11  13124  4sqlem17  13130  ballotfilemfp1  13175  ballotfilemfmpn  13178  ballotfilemsi  13202  nninfdclemp1  13285  ressressg  13372  gsumsplit1r  13661  gsumprval  13662  mndinvmod  13706  mhmco  13745  gsumfzz  13750  grpinvid2  13808  grpasscan2  13819  grpinvssd  13832  grpinvadd  13833  grpsubid1  13840  grpsubadd  13843  grppncan  13846  mulg1  13882  mulgaddcomlem  13898  mulgdirlem  13906  mulgneg2  13909  mulgmodid  13914  nmzsubg  13963  qusinv  13989  qussub  13990  conjnmz  14032  ablsub2inv  14064  abladdsub4  14067  abladdsub  14068  ablpncan2  14069  ablpnpcan  14073  ablnncan  14074  invghm  14082  gsumfzconst  14094  gsumfzsnfd  14098  gfsumval  14102  gfsumsn  14107  gfsumz  14109  rngm2neg  14188  srgpcompp  14234  srgpcomppsc  14235  ringinvnzdiv  14293  ringm2neg  14298  dvr1  14383  dvrcan1  14385  dvrcan3  14386  rdivmuldivd  14389  lmodfopne  14600  sralemg  14712  gsumfzfsumlemm  14861  mplsubgfilemcl  14980  mplsubgfileminv  14981  xmetxpbl  15499  ivthinclemuopn  15629  limcimolemlt  15655  cnplimcim  15658  limccnpcntop  15666  limccnp2lem  15667  dvexp  15702  dvmptcmulcn  15712  dvply1  15756  ef2kpi  15797  sinhalfpip  15811  sinhalfpim  15812  coshalfpim  15814  ptolemy  15815  tangtx  15829  rpabscxpbnd  15931  relogbexpap  15949  rplogbcxp  15954  rpcxplogb  15955  binom4  15970  pellexlem2  15972  wilthlem1  15974  0sgm  15979  mpodvdsmulf1o  15984  fsumdvdsmul  15985  sgmppw  15986  0sgmppw  15987  1sgm2ppw  15989  perfectlem1  15993  perfectlem2  15994  perfect  15995  lgsval2lem  16009  lgsval4  16019  lgsval4a  16021  lgsneg  16023  lgsneg1  16024  lgsdirprm  16033  lgsdir  16034  lgsne0  16037  lgsmulsqcoprm  16045  gausslemma2dlem1a  16057  gausslemma2dlem6  16066  gausslemma2d  16068  lgseisenlem3  16071  lgseisenlem4  16072  lgseisen  16073  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem1  16080  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgslem3d1  16099  2sqlem3  16116  structiedg0val  16161  uhgr2edg  16327  usgr1e  16362  vtxdgfifival  16412  vtxdfifiun  16418  vtxdumgrfival  16419  vtxduspgrfvedgfi  16422  1loopgredg  16425  1loopgrvd2fi  16426  1hevtxdg1en  16429  p1evtxdeqfi  16433  edginwlkd  16476  clwwlknonex2lem1  16558  eupthvdres  16596  peano4nninf  16910  repiecele0  16936  repiecege0  16937  trilpolemclim  16946  trilpolemeq1  16950  apdifflemf  16956