Theorem 3eqtrd 2242

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 2238	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	1, 4	eqtrd 2238	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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  tpeq123d  3725  diftpsn3  3774  oteq123d  3834  resiima  5040  fvun1  5645  fvmptd  5660  fmptpr  5776  caovlem2d  6139  offval  6166  ofvalg  6168  cnvf1olem  6310  nnm1  6611  updjudhcoinlf  7182  updjudhcoinrg  7183  caseinl  7193  caseinr  7194  omp1eomlem  7196  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  ltexnqq  7521  prarloclemarch  7531  ltrnqg  7533  nq02m  7578  prarloclemcalc  7615  mulnqprl  7681  mulnqpru  7682  ltexprlemloc  7720  addcanprleml  7727  recexprlem1ssu  7747  cauappcvgprlem1  7772  caucvgsrlemfv  7904  caucvgsrlemoffval  7909  recidpirqlemcalc  7970  axmulass  7986  axrnegex  7992  muladd11r  8228  addcan2  8253  addsub  8283  subsub2  8300  negsubdi2  8331  muladd  8456  mulsub  8473  cru  8675  mulreim  8677  recextlem1  8724  mulap0  8727  muleqadd  8741  divrecap  8761  div23ap  8764  div12ap  8767  divmulasscomap  8769  divcanap7  8794  conjmulap  8802  apmul1  8861  nndivtr  9078  subhalfhalf  9272  xp1d2m1eqxm1d2  9290  div4p1lem1div2  9291  qapne  9760  xnegneg  9955  rexsub  9975  xnegid  9981  fseq1p1m1  10216  nn0split  10258  nnsplit  10259  fzosplitsnm1  10338  fzosplitprm1  10363  ceilid  10460  flqdiv  10466  zmod10  10485  modqcyc  10504  modqaddabs  10507  mulqaddmodid  10509  modqadd2mod  10519  modqm1p1mod0  10520  modqmul12d  10523  modqadd12d  10525  modqmulmodr  10535  modqaddmulmod  10536  frecuzrdgsuc  10559  seqeq123d  10601  seqvalcd  10606  seq3f1olemqsumkj  10656  seq3f1oleml  10661  seqf1oglem2  10665  seq3id3  10669  seq3id  10670  seq3homo  10672  seq3z  10673  seqhomog  10675  exp1  10690  expnegap0  10692  expmulzap  10730  m1expeven  10731  expdivap  10735  binom3  10802  sqoddm1div8  10838  mulsubdivbinom2ap  10856  bcn1  10903  bcnp1n  10904  bcval5  10908  bcn2m1  10914  bcn2p1  10915  hashdifpr  10965  ccatlen  11051  ccats1val2  11092  lswccats1  11095  swrdlend  11111  ccatswrd  11123  crim  11169  remullem  11182  remul2  11184  immul2  11191  ipcnval  11197  cjreim  11214  recvguniqlem  11305  resqrexlemover  11321  resqrexlemcalc1  11325  absid  11382  amgm2  11429  max0addsup  11530  minabs  11547  xrmaxrecl  11566  xrminadd  11586  fsumsplitf  11719  sumsnf  11720  fsump1i  11744  fsum2dlemstep  11745  fsumshftm  11756  fsummulc2  11759  modfsummodlemstep  11768  telfsumo  11777  fsumrelem  11782  hash2iun1dif1  11791  binomlem  11794  binom1dif  11798  arisum  11809  geo2sum  11825  geo2sum2  11826  cvgratz  11843  mertenslemi1  11846  clim2prod  11850  fprodeq0  11928  fprod2dlemstep  11933  fproddivap  11941  fproddivapf  11942  fprodmodd  11952  ef0lem  11971  eftlub  12001  efsep  12002  effsumlt  12003  tanval2ap  12024  efi4p  12028  resin4p  12029  recos4p  12030  efeul  12045  sinadd  12047  cosadd  12048  sinmul  12055  ef01bndlem  12067  cos12dec  12079  absef  12081  demoivreALT  12085  dvds2ln  12135  dvdseq  12159  opeo  12208  bezoutlemnewy  12317  nninfctlemfo  12361  eucalginv  12378  eucalglt  12379  eucalg  12381  lcmgcdlem  12399  lcm1  12403  divgcdcoprmex  12424  2sqpwodd  12498  zgcdsq  12523  qden1elz  12527  phiprmpw  12544  eulerthlem1  12549  eulerthlemrprm  12551  prmdiv  12557  hashgcdlem  12560  odzdvds  12568  vfermltl  12574  modprm0  12577  pythagtriplem12  12598  pcqmul  12626  pcaddlem  12662  pcadd  12663  pcadd2  12664  pcmpt  12666  pcmpt2  12667  mul4sqlem  12716  4sqlem11  12724  4sqlem17  12730  nninfdclemp1  12821  ressressg  12907  gsumsplit1r  13230  gsumprval  13231  mndinvmod  13277  mhmco  13322  gsumfzz  13327  grpinvid2  13385  grpasscan2  13396  grpinvssd  13409  grpinvadd  13410  grpsubid1  13417  grpsubadd  13420  grppncan  13423  mulg1  13465  mulgaddcomlem  13481  mulgdirlem  13489  mulgneg2  13492  mulgmodid  13497  nmzsubg  13546  qusinv  13572  qussub  13573  conjnmz  13615  ablsub2inv  13647  abladdsub4  13650  abladdsub  13651  ablpncan2  13652  ablpnpcan  13656  ablnncan  13657  invghm  13665  gsumfzconst  13677  gsumfzsnfd  13681  rngm2neg  13711  srgpcompp  13753  srgpcomppsc  13754  ringinvnzdiv  13812  ringm2neg  13817  dvr1  13900  dvrcan1  13902  dvrcan3  13903  rdivmuldivd  13906  lmodfopne  14088  sralemg  14200  gsumfzfsumlemm  14349  mplsubgfilemcl  14461  mplsubgfileminv  14462  xmetxpbl  14980  ivthinclemuopn  15110  limcimolemlt  15136  cnplimcim  15139  limccnpcntop  15147  limccnp2lem  15148  dvexp  15183  dvmptcmulcn  15193  dvply1  15237  ef2kpi  15278  sinhalfpip  15292  sinhalfpim  15293  coshalfpim  15295  ptolemy  15296  tangtx  15310  rpabscxpbnd  15412  relogbexpap  15430  rplogbcxp  15435  rpcxplogb  15436  binom4  15451  wilthlem1  15452  0sgm  15457  mpodvdsmulf1o  15462  fsumdvdsmul  15463  sgmppw  15464  0sgmppw  15465  1sgm2ppw  15467  perfectlem1  15471  perfectlem2  15472  perfect  15473  lgsval2lem  15487  lgsval4  15497  lgsval4a  15499  lgsneg  15501  lgsneg1  15502  lgsdirprm  15511  lgsdir  15512  lgsne0  15515  lgsmulsqcoprm  15523  gausslemma2dlem1a  15535  gausslemma2dlem6  15544  gausslemma2d  15546  lgseisenlem3  15549  lgseisenlem4  15550  lgseisen  15551  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem1  15558  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2lgslem3d1  15577  2sqlem3  15594  structiedg0val  15637  peano4nninf  15943  trilpolemclim  15975  trilpolemeq1  15979  apdifflemf  15985