Theorem 3eqtrd 2241

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

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  tpeq123d  3724  diftpsn3  3773  oteq123d  3833  resiima  5039  fvun1  5644  fvmptd  5659  fmptpr  5775  caovlem2d  6138  offval  6165  ofvalg  6167  cnvf1olem  6309  nnm1  6610  updjudhcoinlf  7181  updjudhcoinrg  7182  caseinl  7192  caseinr  7193  omp1eomlem  7195  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  ltexnqq  7520  prarloclemarch  7530  ltrnqg  7532  nq02m  7577  prarloclemcalc  7614  mulnqprl  7680  mulnqpru  7681  ltexprlemloc  7719  addcanprleml  7726  recexprlem1ssu  7746  cauappcvgprlem1  7771  caucvgsrlemfv  7903  caucvgsrlemoffval  7908  recidpirqlemcalc  7969  axmulass  7985  axrnegex  7991  muladd11r  8227  addcan2  8252  addsub  8282  subsub2  8299  negsubdi2  8330  muladd  8455  mulsub  8472  cru  8674  mulreim  8676  recextlem1  8723  mulap0  8726  muleqadd  8740  divrecap  8760  div23ap  8763  div12ap  8766  divmulasscomap  8768  divcanap7  8793  conjmulap  8801  apmul1  8860  nndivtr  9077  subhalfhalf  9271  xp1d2m1eqxm1d2  9289  div4p1lem1div2  9290  qapne  9759  xnegneg  9954  rexsub  9974  xnegid  9980  fseq1p1m1  10215  nn0split  10257  nnsplit  10258  fzosplitsnm1  10336  fzosplitprm1  10361  ceilid  10458  flqdiv  10464  zmod10  10483  modqcyc  10502  modqaddabs  10505  mulqaddmodid  10507  modqadd2mod  10517  modqm1p1mod0  10518  modqmul12d  10521  modqadd12d  10523  modqmulmodr  10533  modqaddmulmod  10534  frecuzrdgsuc  10557  seqeq123d  10599  seqvalcd  10604  seq3f1olemqsumkj  10654  seq3f1oleml  10659  seqf1oglem2  10663  seq3id3  10667  seq3id  10668  seq3homo  10670  seq3z  10671  seqhomog  10673  exp1  10688  expnegap0  10690  expmulzap  10728  m1expeven  10729  expdivap  10733  binom3  10800  sqoddm1div8  10836  mulsubdivbinom2ap  10854  bcn1  10901  bcnp1n  10902  bcval5  10906  bcn2m1  10912  bcn2p1  10913  hashdifpr  10963  ccatlen  11049  ccats1val2  11090  lswccats1  11093  crim  11140  remullem  11153  remul2  11155  immul2  11162  ipcnval  11168  cjreim  11185  recvguniqlem  11276  resqrexlemover  11292  resqrexlemcalc1  11296  absid  11353  amgm2  11400  max0addsup  11501  minabs  11518  xrmaxrecl  11537  xrminadd  11557  fsumsplitf  11690  sumsnf  11691  fsump1i  11715  fsum2dlemstep  11716  fsumshftm  11727  fsummulc2  11730  modfsummodlemstep  11739  telfsumo  11748  fsumrelem  11753  hash2iun1dif1  11762  binomlem  11765  binom1dif  11769  arisum  11780  geo2sum  11796  geo2sum2  11797  cvgratz  11814  mertenslemi1  11817  clim2prod  11821  fprodeq0  11899  fprod2dlemstep  11904  fproddivap  11912  fproddivapf  11913  fprodmodd  11923  ef0lem  11942  eftlub  11972  efsep  11973  effsumlt  11974  tanval2ap  11995  efi4p  11999  resin4p  12000  recos4p  12001  efeul  12016  sinadd  12018  cosadd  12019  sinmul  12026  ef01bndlem  12038  cos12dec  12050  absef  12052  demoivreALT  12056  dvds2ln  12106  dvdseq  12130  opeo  12179  bezoutlemnewy  12288  nninfctlemfo  12332  eucalginv  12349  eucalglt  12350  eucalg  12352  lcmgcdlem  12370  lcm1  12374  divgcdcoprmex  12395  2sqpwodd  12469  zgcdsq  12494  qden1elz  12498  phiprmpw  12515  eulerthlem1  12520  eulerthlemrprm  12522  prmdiv  12528  hashgcdlem  12531  odzdvds  12539  vfermltl  12545  modprm0  12548  pythagtriplem12  12569  pcqmul  12597  pcaddlem  12633  pcadd  12634  pcadd2  12635  pcmpt  12637  pcmpt2  12638  mul4sqlem  12687  4sqlem11  12695  4sqlem17  12701  nninfdclemp1  12792  ressressg  12878  gsumsplit1r  13201  gsumprval  13202  mndinvmod  13248  mhmco  13293  gsumfzz  13298  grpinvid2  13356  grpasscan2  13367  grpinvssd  13380  grpinvadd  13381  grpsubid1  13388  grpsubadd  13391  grppncan  13394  mulg1  13436  mulgaddcomlem  13452  mulgdirlem  13460  mulgneg2  13463  mulgmodid  13468  nmzsubg  13517  qusinv  13543  qussub  13544  conjnmz  13586  ablsub2inv  13618  abladdsub4  13621  abladdsub  13622  ablpncan2  13623  ablpnpcan  13627  ablnncan  13628  invghm  13636  gsumfzconst  13648  gsumfzsnfd  13652  rngm2neg  13682  srgpcompp  13724  srgpcomppsc  13725  ringinvnzdiv  13783  ringm2neg  13788  dvr1  13871  dvrcan1  13873  dvrcan3  13874  rdivmuldivd  13877  lmodfopne  14059  sralemg  14171  gsumfzfsumlemm  14320  mplsubgfilemcl  14432  mplsubgfileminv  14433  xmetxpbl  14951  ivthinclemuopn  15081  limcimolemlt  15107  cnplimcim  15110  limccnpcntop  15118  limccnp2lem  15119  dvexp  15154  dvmptcmulcn  15164  dvply1  15208  ef2kpi  15249  sinhalfpip  15263  sinhalfpim  15264  coshalfpim  15266  ptolemy  15267  tangtx  15281  rpabscxpbnd  15383  relogbexpap  15401  rplogbcxp  15406  rpcxplogb  15407  binom4  15422  wilthlem1  15423  0sgm  15428  mpodvdsmulf1o  15433  fsumdvdsmul  15434  sgmppw  15435  0sgmppw  15436  1sgm2ppw  15438  perfectlem1  15442  perfectlem2  15443  perfect  15444  lgsval2lem  15458  lgsval4  15468  lgsval4a  15470  lgsneg  15472  lgsneg1  15473  lgsdirprm  15482  lgsdir  15483  lgsne0  15486  lgsmulsqcoprm  15494  gausslemma2dlem1a  15506  gausslemma2dlem6  15515  gausslemma2d  15517  lgseisenlem3  15520  lgseisenlem4  15521  lgseisen  15522  lgsquadlem1  15525  lgsquadlem2  15526  lgsquad2lem1  15529  2lgslem3a  15541  2lgslem3b  15542  2lgslem3c  15543  2lgslem3d  15544  2lgslem3d1  15548  2sqlem3  15565  structiedg0val  15608  peano4nninf  15905  trilpolemclim  15937  trilpolemeq1  15941  apdifflemf  15947