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  6802  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  10055  xnegneg  10252  rexsub  10272  xnegid  10278  fseq1p1m1  10518  nn0split  10560  nnsplit  10561  fzosplitsnm1  10644  fzosplitpr  10669  fzosplitprm1  10670  ceilid  10773  flqdiv  10779  zmod10  10798  modqcyc  10817  modqaddabs  10820  mulqaddmodid  10822  modqadd2mod  10832  modqm1p1mod0  10833  modqmul12d  10836  modqadd12d  10838  modqmulmodr  10848  modqaddmulmod  10849  frecuzrdgsuc  10872  seqeq123d  10914  seqvalcd  10919  seq3f1olemqsumkj  10969  seq3f1oleml  10974  seqf1oglem2  10978  seq3id3  10982  seq3id  10983  seq3homo  10985  seq3z  10986  seqhomog  10988  exp1  11003  expnegap0  11005  expmulzap  11043  m1expeven  11044  expdivap  11048  binom3  11115  sqoddm1div8  11152  mulsubdivbinom2ap  11171  bcn1  11218  bcnp1n  11219  bcval5  11223  bcn2m1  11230  bcn2p1  11231  hashdifpr  11283  hashmap  11290  hashfibclem  11304  hashf1lem2  11308  ccatlen  11385  ccatalpha  11403  ccatw2s1leng  11428  ccats1val2  11430  lswccats1  11433  swrdlend  11452  ccatswrd  11464  pfxmpt  11474  pfxfv  11478  pfxfvlsw  11489  ccatpfx  11495  pfx1  11497  pfxswrd  11500  swrdpfx  11501  pfxpfx  11502  lenrevpfxcctswrd  11506  wrdind  11516  wrd2ind  11517  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatpfx2  11531  pfxccatid  11535  cats1fvnd  11559  crim  11645  remullem  11658  remul2  11660  immul2  11667  ipcnval  11673  cjreim  11691  recvguniqlem  11782  resqrexlemover  11798  resqrexlemcalc1  11802  absid  11859  amgm2  11907  max0addsup  12008  minabs  12026  xrmaxrecl  12046  xrminadd  12066  fsumsplitf  12200  sumsnf  12201  fsump1i  12225  fsum2dlemstep  12226  fsumshftm  12237  fsummulc2  12240  modfsummodlemstep  12249  telfsumo  12258  fsumrelem  12263  hash2iun1dif1  12272  binomlem  12275  binom1dif  12279  arisum  12290  geo2sum  12306  geo2sum2  12307  cvgratz  12324  mertenslemi1  12327  clim2prod  12331  fprodeq0  12409  fprod2dlemstep  12414  fproddivap  12422  fproddivapf  12423  fprodmodd  12433  ef0lem  12452  eftlub  12482  efsep  12483  effsumlt  12484  tanval2ap  12505  efi4p  12509  resin4p  12510  recos4p  12511  efeul  12526  sinadd  12528  cosadd  12529  sinmul  12536  ef01bndlem  12548  cos12dec  12560  absef  12562  demoivreALT  12566  dvds2ln  12616  dvdseq  12640  opeo  12689  bezoutlemnewy  12798  nninfctlemfo  12842  eucalginv  12859  eucalglt  12860  eucalg  12862  lcmgcdlem  12880  lcm1  12884  divgcdcoprmex  12905  2sqpwodd  12981  zgcdsq  13006  qden1elz  13010  phiprmpw  13029  eulerthlem1  13034  eulerthlemrprm  13036  prmdiv  13042  hashgcdlem  13045  odzdvds  13053  vfermltl  13059  modprm0  13062  pythagtriplem12  13083  pcqmul  13111  pcaddlem  13147  pcadd  13148  pcadd2  13149  pcmpt  13151  pcmpt2  13152  mul4sqlem  13201  4sqlem11  13209  4sqlem17  13215  ballotfilemfp1  13289  ballotfilemfmpn  13292  ballotfilemsi  13316  nninfdclemp1  13399  ressressg  13488  gzsumsplit1r  13774  mndinvmod  13817  mhmco  13856  grpinvid2  13917  grpasscan2  13928  grpinvssd  13941  grpinvadd  13942  grpsubid1  13949  grpsubadd  13952  grppncan  13955  mulg1  13991  mulgaddcomlem  14007  mulgdirlem  14015  mulgneg2  14018  mulgmodid  14023  nmzsubg  14072  qusinv  14098  qussub  14099  conjnmz  14141  cntzsgrpcl  14167  cntzsubm  14170  ablsub2inv  14205  abladdsub4  14208  abladdsub  14209  ablpncan2  14210  ablpnpcan  14214  ablnncan  14215  invghm  14223  gzsumconst  14233  gzsumsnfd  14237  gsumvalfi  14242  gsumsncmn  14246  gsumzfi  14248  gsumf1ofi  14250  gsummptfidmsplit  14254  gsumsnfdcmn  14257  rngm2neg  14355  srgpcompp  14402  srgpcomppsc  14403  ringinvnzdiv  14462  ringm2neg  14467  dvr1  14554  dvrcan1  14556  dvrcan3  14557  rdivmuldivd  14560  lmodfopne  14772  sralemg  14884  assa2ass  15118  assa2ass2  15119  asclmul1  15138  asclmul2  15139  assamulgscmlem2  15151  psrlidmfi  15199  psrridmfi  15200  mplsubgfilemcl  15215  mplsubgfileminv  15216  xmetxpbl  15734  ivthinclemuopn  15864  limcimolemlt  15890  cnplimcim  15893  limccnpcntop  15901  limccnp2lem  15902  dvexp  15937  dvmptcmulcn  15947  dvply1  15991  ef2kpi  16033  sinhalfpip  16047  sinhalfpim  16048  coshalfpim  16050  ptolemy  16051  tangtx  16065  rpabscxpbnd  16175  efnthr  16176  relogbexpap  16194  rplogbcxp  16199  rpcxplogb  16200  zprmlogbaplem2  16216  binom4  16219  log2tlbndlog2  16220  birthdaylem2  16226  pellexlem2  16230  wilthlem1  16232  0sgm  16254  chtprm  16261  ppidif  16269  mpodvdsmulf1o  16284  fsumdvdsmul  16285  sgmppw  16286  0sgmppw  16287  1sgm2ppw  16289  chtublem  16295  chtqub  16296  perfectlem1  16299  perfectlem2  16300  perfect  16301  bposlem5  16315  bposlem9  16319  lgsval2lem  16334  lgsval4  16344  lgsval4a  16346  lgsneg  16348  lgsneg1  16349  lgsdirprm  16358  lgsdir  16359  lgsne0  16362  lgsmulsqcoprm  16370  gausslemma2dlem1a  16382  gausslemma2dlem6  16391  gausslemma2d  16393  lgseisenlem3  16396  lgseisenlem4  16397  lgseisen  16398  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem1  16405  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgslem3d1  16424  2sqlem3  16441  structiedg0val  16486  uhgr2edg  16652  usgr1e  16687  vtxdgfifival  16737  vtxdfifiun  16743  vtxdumgrfival  16744  vtxduspgrfvedgfi  16747  1loopgredg  16750  1loopgrvd2fi  16751  1hevtxdg1en  16754  p1evtxdeqfi  16758  edginwlkd  16801  clwwlknonex2lem1  16883  eupthvdres  16921  peano4nninf  17255  repiecele0  17281  repiecege0  17282  trilpolemclim  17292  trilpolemeq1  17296  apdifflemf  17302