Theorem 3eqtrd 2275

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

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  5148  fvun1  5772  fvmptd  5789  fmptpr  5910  caovlem2d  6285  offval  6314  ofvalg  6316  cnvf1olem  6464  supp0  6482  suppsnopdc  6494  suppofss1dcl  6508  suppofss2dcl  6509  suppcofn  6510  nnm1  6803  updjudhcoinlf  7426  updjudhcoinrg  7427  caseinl  7437  caseinr  7438  omp1eomlem  7440  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  ltexnqq  7781  prarloclemarch  7791  ltrnqg  7793  nq02m  7838  prarloclemcalc  7875  mulnqprl  7941  mulnqpru  7942  ltexprlemloc  7980  addcanprleml  7987  recexprlem1ssu  8007  cauappcvgprlem1  8032  caucvgsrlemfv  8164  caucvgsrlemoffval  8169  recidpirqlemcalc  8230  axmulass  8246  axrnegex  8252  muladd11r  8489  addcan2  8514  addsub  8544  subsub2  8561  negsubdi2  8592  muladd  8718  mulsub  8735  cru  8938  mulreim  8940  recextlem1  8987  mulap0  8990  muleqadd  9006  divrecap  9026  div23ap  9029  div12ap  9032  divmulasscomap  9034  divcanap7  9059  conjmulap  9067  apmul1  9126  nndivtr  9355  subhalfhalf  9551  xp1d2m1eqxm1d2  9569  div4p1lem1div2  9570  qapne  10054  xnegneg  10251  rexsub  10271  xnegid  10277  fseq1p1m1  10517  nn0split  10559  nnsplit  10560  fzosplitsnm1  10643  fzosplitpr  10668  fzosplitprm1  10669  ceilid  10772  flqdiv  10778  zmod10  10797  modqcyc  10816  modqaddabs  10819  mulqaddmodid  10821  modqadd2mod  10831  modqm1p1mod0  10832  modqmul12d  10835  modqadd12d  10837  modqmulmodr  10847  modqaddmulmod  10848  frecuzrdgsuc  10871  seqeq123d  10913  seqvalcd  10918  seq3f1olemqsumkj  10968  seq3f1oleml  10973  seqf1oglem2  10977  seq3id3  10981  seq3id  10982  seq3homo  10984  seq3z  10985  seqhomog  10987  exp1  11002  expnegap0  11004  expmulzap  11042  m1expeven  11043  expdivap  11047  binom3  11114  sqoddm1div8  11151  mulsubdivbinom2ap  11170  bcn1  11217  bcnp1n  11218  bcval5  11222  bcn2m1  11229  bcn2p1  11230  hashdifpr  11282  hashmap  11289  hashfibclem  11303  hashf1lem2  11307  ccatlen  11384  ccatalpha  11402  ccatw2s1leng  11427  ccats1val2  11429  lswccats1  11432  swrdlend  11451  ccatswrd  11463  pfxmpt  11473  pfxfv  11477  pfxfvlsw  11488  ccatpfx  11494  pfx1  11496  pfxswrd  11499  swrdpfx  11500  pfxpfx  11501  lenrevpfxcctswrd  11505  wrdind  11515  wrd2ind  11516  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatpfx2  11530  pfxccatid  11534  cats1fvnd  11558  crim  11644  remullem  11657  remul2  11659  immul2  11666  ipcnval  11672  cjreim  11690  recvguniqlem  11781  resqrexlemover  11797  resqrexlemcalc1  11801  absid  11858  amgm2  11906  max0addsup  12007  minabs  12025  xrmaxrecl  12045  xrminadd  12065  fsumsplitf  12199  sumsnf  12200  fsump1i  12224  fsum2dlemstep  12225  fsumshftm  12236  fsummulc2  12239  modfsummodlemstep  12248  telfsumo  12257  fsumrelem  12262  hash2iun1dif1  12271  binomlem  12274  binom1dif  12278  arisum  12289  geo2sum  12305  geo2sum2  12306  cvgratz  12323  mertenslemi1  12326  clim2prod  12330  fprodeq0  12408  fprod2dlemstep  12413  fproddivap  12421  fproddivapf  12422  fprodmodd  12432  ef0lem  12451  eftlub  12481  efsep  12482  effsumlt  12483  tanval2ap  12504  efi4p  12508  resin4p  12509  recos4p  12510  efeul  12525  sinadd  12527  cosadd  12528  sinmul  12535  ef01bndlem  12547  cos12dec  12559  absef  12561  demoivreALT  12565  dvds2ln  12615  dvdseq  12639  opeo  12688  bezoutlemnewy  12797  nninfctlemfo  12841  eucalginv  12858  eucalglt  12859  eucalg  12861  lcmgcdlem  12879  lcm1  12883  divgcdcoprmex  12904  2sqpwodd  12980  zgcdsq  13005  qden1elz  13009  phiprmpw  13028  eulerthlem1  13033  eulerthlemrprm  13035  prmdiv  13041  hashgcdlem  13044  odzdvds  13052  vfermltl  13058  modprm0  13061  pythagtriplem12  13082  pcqmul  13110  pcaddlem  13146  pcadd  13147  pcadd2  13148  pcmpt  13150  pcmpt2  13151  mul4sqlem  13200  4sqlem11  13208  4sqlem17  13214  ballotfilemfp1  13288  ballotfilemfmpn  13291  ballotfilemsi  13315  nninfdclemp1  13398  ressressg  13487  gzsumsplit1r  13773  mndinvmod  13816  mhmco  13855  grpinvid2  13916  grpasscan2  13927  grpinvssd  13940  grpinvadd  13941  grpsubid1  13948  grpsubadd  13951  grppncan  13954  mulg1  13990  mulgaddcomlem  14006  mulgdirlem  14014  mulgneg2  14017  mulgmodid  14022  nmzsubg  14071  qusinv  14097  qussub  14098  conjnmz  14140  cntzsgrpcl  14166  cntzsubm  14169  ablsub2inv  14204  abladdsub4  14207  abladdsub  14208  ablpncan2  14209  ablpnpcan  14213  ablnncan  14214  invghm  14222  gzsumconst  14232  gzsumsnfd  14236  gsumvalfi  14241  gsumsncmn  14245  gsumzfi  14247  gsumf1ofi  14249  gsummptfidmsplit  14253  gsumsnfdcmn  14256  rngm2neg  14354  srgpcompp  14401  srgpcomppsc  14402  ringinvnzdiv  14461  ringm2neg  14466  dvr1  14553  dvrcan1  14555  dvrcan3  14556  rdivmuldivd  14559  lmodfopne  14771  sralemg  14883  assa2ass  15117  assa2ass2  15118  asclmul1  15137  asclmul2  15138  assamulgscmlem2  15150  psrlidmfi  15208  psrridmfi  15209  xmetxpbl  15751  ivthinclemuopn  15881  limcimolemlt  15907  cnplimcim  15910  limccnpcntop  15918  limccnp2lem  15919  dvexp  15954  dvmptcmulcn  15964  dvply1  16008  ef2kpi  16050  sinhalfpip  16064  sinhalfpim  16065  coshalfpim  16067  ptolemy  16068  tangtx  16082  rpabscxpbnd  16192  efnthr  16193  relogbexpap  16211  rplogbcxp  16216  rpcxplogb  16217  zprmlogbaplem2  16233  binom4  16236  log2tlbndlog2  16237  birthdaylem2  16243  pellexlem2  16247  wilthlem1  16249  0sgm  16271  chtprm  16278  ppidif  16286  mpodvdsmulf1o  16301  fsumdvdsmul  16302  sgmppw  16303  0sgmppw  16304  1sgm2ppw  16306  chtublem  16312  chtqub  16313  perfectlem1  16316  perfectlem2  16317  perfect  16318  bposlem5  16332  bposlem9  16336  lgsval2lem  16351  lgsval4  16361  lgsval4a  16363  lgsneg  16365  lgsneg1  16366  lgsdirprm  16375  lgsdir  16376  lgsne0  16379  lgsmulsqcoprm  16387  gausslemma2dlem1a  16399  gausslemma2dlem6  16408  gausslemma2d  16410  lgseisenlem3  16413  lgseisenlem4  16414  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem1  16422  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgslem3d1  16441  2sqlem3  16458  structiedg0val  16503  uhgr2edg  16669  usgr1e  16704  vtxdgfifival  16754  vtxdfifiun  16760  vtxdumgrfival  16761  vtxduspgrfvedgfi  16764  1loopgredg  16767  1loopgrvd2fi  16768  1hevtxdg1en  16771  p1evtxdeqfi  16775  edginwlkd  16818  clwwlknonex2lem1  16900  eupthvdres  16938  peano4nninf  17272  repiecele0  17298  repiecege0  17299  trilpolemclim  17309  trilpolemeq1  17313  apdifflemf  17319