Theorem 3eqtrd 2201

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

Syntax hints:   → wi 4   = wceq 1342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-4 1497  ax-17 1513  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-cleq 2157

This theorem is referenced by:  tpeq123d  3662  diftpsn3  3708  oteq123d  3767  resiima  4956  fvun1  5546  fvmptd  5561  fmptpr  5671  caovlem2d  6025  offval  6051  ofvalg  6053  cnvf1olem  6183  nnm1  6483  updjudhcoinlf  7036  updjudhcoinrg  7037  caseinl  7047  caseinr  7048  omp1eomlem  7050  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  ltexnqq  7340  prarloclemarch  7350  ltrnqg  7352  nq02m  7397  prarloclemcalc  7434  mulnqprl  7500  mulnqpru  7501  ltexprlemloc  7539  addcanprleml  7546  recexprlem1ssu  7566  cauappcvgprlem1  7591  caucvgsrlemfv  7723  caucvgsrlemoffval  7728  recidpirqlemcalc  7789  axmulass  7805  axrnegex  7811  muladd11r  8045  addcan2  8070  addsub  8100  subsub2  8117  negsubdi2  8148  muladd  8273  mulsub  8290  cru  8491  mulreim  8493  recextlem1  8539  mulap0  8542  muleqadd  8556  divrecap  8575  div23ap  8578  div12ap  8581  divmulasscomap  8583  divcanap7  8608  conjmulap  8616  apmul1  8675  nndivtr  8890  xp1d2m1eqxm1d2  9100  div4p1lem1div2  9101  qapne  9568  xnegneg  9760  rexsub  9780  xnegid  9786  fseq1p1m1  10019  nn0split  10061  nnsplit  10062  fzosplitsnm1  10134  fzosplitprm1  10159  ceilid  10240  flqdiv  10246  zmod10  10265  modqcyc  10284  modqaddabs  10287  mulqaddmodid  10289  modqadd2mod  10299  modqm1p1mod0  10300  modqmul12d  10303  modqadd12d  10305  modqmulmodr  10315  modqaddmulmod  10316  frecuzrdgsuc  10339  seqeq123d  10379  seqvalcd  10384  seq3f1olemqsumkj  10423  seq3f1oleml  10428  seq3id3  10432  seq3id  10433  seq3homo  10435  seq3z  10436  exp1  10451  expnegap0  10453  expmulzap  10491  m1expeven  10492  expdivap  10496  binom3  10561  sqoddm1div8  10597  bcn1  10660  bcnp1n  10661  bcval5  10665  bcn2m1  10671  bcn2p1  10672  hashdifpr  10722  crim  10786  remullem  10799  remul2  10801  immul2  10808  ipcnval  10814  cjreim  10831  recvguniqlem  10922  resqrexlemover  10938  resqrexlemcalc1  10942  absid  10999  amgm2  11046  max0addsup  11147  minabs  11163  xrmaxrecl  11182  xrminadd  11202  fsumsplitf  11335  sumsnf  11336  fsump1i  11360  fsum2dlemstep  11361  fsumshftm  11372  fsummulc2  11375  modfsummodlemstep  11384  telfsumo  11393  fsumrelem  11398  hash2iun1dif1  11407  binomlem  11410  binom1dif  11414  arisum  11425  geo2sum  11441  geo2sum2  11442  cvgratz  11459  mertenslemi1  11462  clim2prod  11466  fprodeq0  11544  fprod2dlemstep  11549  fproddivap  11557  fproddivapf  11558  fprodmodd  11568  ef0lem  11587  eftlub  11617  efsep  11618  effsumlt  11619  tanval2ap  11640  efi4p  11644  resin4p  11645  recos4p  11646  efeul  11661  sinadd  11663  cosadd  11664  sinmul  11671  ef01bndlem  11683  cos12dec  11694  absef  11696  demoivreALT  11700  dvds2ln  11750  dvdseq  11771  opeo  11819  bezoutlemnewy  11914  eucalginv  11967  eucalglt  11968  eucalg  11970  lcmgcdlem  11988  lcm1  11992  divgcdcoprmex  12013  2sqpwodd  12085  zgcdsq  12110  qden1elz  12114  phiprmpw  12131  eulerthlem1  12136  eulerthlemrprm  12138  prmdiv  12144  hashgcdlem  12147  odzdvds  12154  vfermltl  12160  modprm0  12163  pythagtriplem12  12184  pcqmul  12212  pcaddlem  12247  pcadd  12248  pcmpt  12250  pcmpt2  12251  nninfdclemp1  12322  xmetxpbl  13049  ivthinclemuopn  13157  limcimolemlt  13174  cnplimcim  13177  limccnpcntop  13185  limccnp2lem  13186  dvexp  13216  dvmptcmulcn  13224  ef2kpi  13268  sinhalfpip  13282  sinhalfpim  13283  coshalfpim  13285  ptolemy  13286  tangtx  13300  rpabscxpbnd  13400  relogbexpap  13417  rplogbcxp  13422  rpcxplogb  13423  binom4  13438  peano4nninf  13720  trilpolemclim  13749  trilpolemeq1  13753  apdifflemf  13759