Theorem 3eqtrd 2268

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  tpeq123d  3763  diftpsn3  3814  oteq123d  3877  resiima  5094  fvun1  5712  fvmptd  5727  fmptpr  5846  caovlem2d  6215  offval  6243  ofvalg  6245  cnvf1olem  6389  nnm1  6693  updjudhcoinlf  7279  updjudhcoinrg  7280  caseinl  7290  caseinr  7291  omp1eomlem  7293  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  ltexnqq  7628  prarloclemarch  7638  ltrnqg  7640  nq02m  7685  prarloclemcalc  7722  mulnqprl  7788  mulnqpru  7789  ltexprlemloc  7827  addcanprleml  7834  recexprlem1ssu  7854  cauappcvgprlem1  7879  caucvgsrlemfv  8011  caucvgsrlemoffval  8016  recidpirqlemcalc  8077  axmulass  8093  axrnegex  8099  muladd11r  8335  addcan2  8360  addsub  8390  subsub2  8407  negsubdi2  8438  muladd  8563  mulsub  8580  cru  8782  mulreim  8784  recextlem1  8831  mulap0  8834  muleqadd  8848  divrecap  8868  div23ap  8871  div12ap  8874  divmulasscomap  8876  divcanap7  8901  conjmulap  8909  apmul1  8968  nndivtr  9185  subhalfhalf  9379  xp1d2m1eqxm1d2  9397  div4p1lem1div2  9398  qapne  9873  xnegneg  10068  rexsub  10088  xnegid  10094  fseq1p1m1  10329  nn0split  10371  nnsplit  10372  fzosplitsnm1  10455  fzosplitpr  10480  fzosplitprm1  10481  ceilid  10578  flqdiv  10584  zmod10  10603  modqcyc  10622  modqaddabs  10625  mulqaddmodid  10627  modqadd2mod  10637  modqm1p1mod0  10638  modqmul12d  10641  modqadd12d  10643  modqmulmodr  10653  modqaddmulmod  10654  frecuzrdgsuc  10677  seqeq123d  10719  seqvalcd  10724  seq3f1olemqsumkj  10774  seq3f1oleml  10779  seqf1oglem2  10783  seq3id3  10787  seq3id  10788  seq3homo  10790  seq3z  10791  seqhomog  10793  exp1  10808  expnegap0  10810  expmulzap  10848  m1expeven  10849  expdivap  10853  binom3  10920  sqoddm1div8  10956  mulsubdivbinom2ap  10974  bcn1  11021  bcnp1n  11022  bcval5  11026  bcn2m1  11032  bcn2p1  11033  hashdifpr  11085  ccatlen  11176  ccatalpha  11194  ccatw2s1leng  11219  ccats1val2  11221  lswccats1  11224  swrdlend  11243  ccatswrd  11255  pfxmpt  11265  pfxfv  11269  pfxfvlsw  11280  ccatpfx  11286  pfx1  11288  pfxswrd  11291  swrdpfx  11292  pfxpfx  11293  lenrevpfxcctswrd  11297  wrdind  11307  wrd2ind  11308  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatpfx2  11322  pfxccatid  11326  cats1fvnd  11350  crim  11423  remullem  11436  remul2  11438  immul2  11445  ipcnval  11451  cjreim  11468  recvguniqlem  11559  resqrexlemover  11575  resqrexlemcalc1  11579  absid  11636  amgm2  11683  max0addsup  11784  minabs  11801  xrmaxrecl  11820  xrminadd  11840  fsumsplitf  11974  sumsnf  11975  fsump1i  11999  fsum2dlemstep  12000  fsumshftm  12011  fsummulc2  12014  modfsummodlemstep  12023  telfsumo  12032  fsumrelem  12037  hash2iun1dif1  12046  binomlem  12049  binom1dif  12053  arisum  12064  geo2sum  12080  geo2sum2  12081  cvgratz  12098  mertenslemi1  12101  clim2prod  12105  fprodeq0  12183  fprod2dlemstep  12188  fproddivap  12196  fproddivapf  12197  fprodmodd  12207  ef0lem  12226  eftlub  12256  efsep  12257  effsumlt  12258  tanval2ap  12279  efi4p  12283  resin4p  12284  recos4p  12285  efeul  12300  sinadd  12302  cosadd  12303  sinmul  12310  ef01bndlem  12322  cos12dec  12334  absef  12336  demoivreALT  12340  dvds2ln  12390  dvdseq  12414  opeo  12463  bezoutlemnewy  12572  nninfctlemfo  12616  eucalginv  12633  eucalglt  12634  eucalg  12636  lcmgcdlem  12654  lcm1  12658  divgcdcoprmex  12679  2sqpwodd  12753  zgcdsq  12778  qden1elz  12782  phiprmpw  12799  eulerthlem1  12804  eulerthlemrprm  12806  prmdiv  12812  hashgcdlem  12815  odzdvds  12823  vfermltl  12829  modprm0  12832  pythagtriplem12  12853  pcqmul  12881  pcaddlem  12917  pcadd  12918  pcadd2  12919  pcmpt  12921  pcmpt2  12922  mul4sqlem  12971  4sqlem11  12979  4sqlem17  12985  nninfdclemp1  13076  ressressg  13163  gsumsplit1r  13486  gsumprval  13487  mndinvmod  13533  mhmco  13578  gsumfzz  13583  grpinvid2  13641  grpasscan2  13652  grpinvssd  13665  grpinvadd  13666  grpsubid1  13673  grpsubadd  13676  grppncan  13679  mulg1  13721  mulgaddcomlem  13737  mulgdirlem  13745  mulgneg2  13748  mulgmodid  13753  nmzsubg  13802  qusinv  13828  qussub  13829  conjnmz  13871  ablsub2inv  13903  abladdsub4  13906  abladdsub  13907  ablpncan2  13908  ablpnpcan  13912  ablnncan  13913  invghm  13921  gsumfzconst  13933  gsumfzsnfd  13937  rngm2neg  13968  srgpcompp  14010  srgpcomppsc  14011  ringinvnzdiv  14069  ringm2neg  14074  dvr1  14158  dvrcan1  14160  dvrcan3  14161  rdivmuldivd  14164  lmodfopne  14346  sralemg  14458  gsumfzfsumlemm  14607  mplsubgfilemcl  14719  mplsubgfileminv  14720  xmetxpbl  15238  ivthinclemuopn  15368  limcimolemlt  15394  cnplimcim  15397  limccnpcntop  15405  limccnp2lem  15406  dvexp  15441  dvmptcmulcn  15451  dvply1  15495  ef2kpi  15536  sinhalfpip  15550  sinhalfpim  15551  coshalfpim  15553  ptolemy  15554  tangtx  15568  rpabscxpbnd  15670  relogbexpap  15688  rplogbcxp  15693  rpcxplogb  15694  binom4  15709  wilthlem1  15710  0sgm  15715  mpodvdsmulf1o  15720  fsumdvdsmul  15721  sgmppw  15722  0sgmppw  15723  1sgm2ppw  15725  perfectlem1  15729  perfectlem2  15730  perfect  15731  lgsval2lem  15745  lgsval4  15755  lgsval4a  15757  lgsneg  15759  lgsneg1  15760  lgsdirprm  15769  lgsdir  15770  lgsne0  15773  lgsmulsqcoprm  15781  gausslemma2dlem1a  15793  gausslemma2dlem6  15802  gausslemma2d  15804  lgseisenlem3  15807  lgseisenlem4  15808  lgseisen  15809  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem1  15816  2lgslem3a  15828  2lgslem3b  15829  2lgslem3c  15830  2lgslem3d  15831  2lgslem3d1  15835  2sqlem3  15852  structiedg0val  15897  uhgr2edg  16063  usgr1e  16098  vtxdgfifival  16148  vtxdfifiun  16154  vtxdumgrfival  16155  vtxduspgrfvedgfi  16158  1loopgredg  16161  1loopgrvd2fi  16162  1hevtxdg1en  16165  p1evtxdeqfi  16169  edginwlkd  16212  clwwlknonex2lem1  16294  eupthvdres  16332  peano4nninf  16634  trilpolemclim  16666  trilpolemeq1  16670  apdifflemf  16676  gfsumval  16707  gfsumsn  16712