Theorem 3eqtrd 2207

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

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  tpeq123d  3673  diftpsn3  3719  oteq123d  3778  resiima  4967  fvun1  5560  fvmptd  5575  fmptpr  5686  caovlem2d  6043  offval  6066  ofvalg  6068  cnvf1olem  6201  nnm1  6502  updjudhcoinlf  7055  updjudhcoinrg  7056  caseinl  7066  caseinr  7067  omp1eomlem  7069  exmidfodomrlemr  7172  exmidfodomrlemrALT  7173  ltexnqq  7363  prarloclemarch  7373  ltrnqg  7375  nq02m  7420  prarloclemcalc  7457  mulnqprl  7523  mulnqpru  7524  ltexprlemloc  7562  addcanprleml  7569  recexprlem1ssu  7589  cauappcvgprlem1  7614  caucvgsrlemfv  7746  caucvgsrlemoffval  7751  recidpirqlemcalc  7812  axmulass  7828  axrnegex  7834  muladd11r  8068  addcan2  8093  addsub  8123  subsub2  8140  negsubdi2  8171  muladd  8296  mulsub  8313  cru  8514  mulreim  8516  recextlem1  8562  mulap0  8565  muleqadd  8579  divrecap  8598  div23ap  8601  div12ap  8604  divmulasscomap  8606  divcanap7  8631  conjmulap  8639  apmul1  8698  nndivtr  8913  xp1d2m1eqxm1d2  9123  div4p1lem1div2  9124  qapne  9591  xnegneg  9783  rexsub  9803  xnegid  9809  fseq1p1m1  10043  nn0split  10085  nnsplit  10086  fzosplitsnm1  10158  fzosplitprm1  10183  ceilid  10264  flqdiv  10270  zmod10  10289  modqcyc  10308  modqaddabs  10311  mulqaddmodid  10313  modqadd2mod  10323  modqm1p1mod0  10324  modqmul12d  10327  modqadd12d  10329  modqmulmodr  10339  modqaddmulmod  10340  frecuzrdgsuc  10363  seqeq123d  10403  seqvalcd  10408  seq3f1olemqsumkj  10447  seq3f1oleml  10452  seq3id3  10456  seq3id  10457  seq3homo  10459  seq3z  10460  exp1  10475  expnegap0  10477  expmulzap  10515  m1expeven  10516  expdivap  10520  binom3  10586  sqoddm1div8  10622  bcn1  10685  bcnp1n  10686  bcval5  10690  bcn2m1  10696  bcn2p1  10697  hashdifpr  10748  crim  10815  remullem  10828  remul2  10830  immul2  10837  ipcnval  10843  cjreim  10860  recvguniqlem  10951  resqrexlemover  10967  resqrexlemcalc1  10971  absid  11028  amgm2  11075  max0addsup  11176  minabs  11192  xrmaxrecl  11211  xrminadd  11231  fsumsplitf  11364  sumsnf  11365  fsump1i  11389  fsum2dlemstep  11390  fsumshftm  11401  fsummulc2  11404  modfsummodlemstep  11413  telfsumo  11422  fsumrelem  11427  hash2iun1dif1  11436  binomlem  11439  binom1dif  11443  arisum  11454  geo2sum  11470  geo2sum2  11471  cvgratz  11488  mertenslemi1  11491  clim2prod  11495  fprodeq0  11573  fprod2dlemstep  11578  fproddivap  11586  fproddivapf  11587  fprodmodd  11597  ef0lem  11616  eftlub  11646  efsep  11647  effsumlt  11648  tanval2ap  11669  efi4p  11673  resin4p  11674  recos4p  11675  efeul  11690  sinadd  11692  cosadd  11693  sinmul  11700  ef01bndlem  11712  cos12dec  11723  absef  11725  demoivreALT  11729  dvds2ln  11779  dvdseq  11801  opeo  11849  bezoutlemnewy  11944  eucalginv  12003  eucalglt  12004  eucalg  12006  lcmgcdlem  12024  lcm1  12028  divgcdcoprmex  12049  2sqpwodd  12123  zgcdsq  12148  qden1elz  12152  phiprmpw  12169  eulerthlem1  12174  eulerthlemrprm  12176  prmdiv  12182  hashgcdlem  12185  odzdvds  12192  vfermltl  12198  modprm0  12201  pythagtriplem12  12222  pcqmul  12250  pcaddlem  12285  pcadd  12286  pcmpt  12288  pcmpt2  12289  mul4sqlem  12338  nninfdclemp1  12398  mndinvmod  12671  mhmco  12698  xmetxpbl  13267  ivthinclemuopn  13375  limcimolemlt  13392  cnplimcim  13395  limccnpcntop  13403  limccnp2lem  13404  dvexp  13434  dvmptcmulcn  13442  ef2kpi  13486  sinhalfpip  13500  sinhalfpim  13501  coshalfpim  13503  ptolemy  13504  tangtx  13518  rpabscxpbnd  13618  relogbexpap  13635  rplogbcxp  13640  rpcxplogb  13641  binom4  13656  lgsval2lem  13670  lgsval4  13680  lgsval4a  13682  lgsneg  13684  lgsneg1  13685  lgsdirprm  13694  lgsdir  13695  lgsne0  13698  lgsmulsqcoprm  13706  2sqlem3  13712  peano4nninf  14004  trilpolemclim  14033  trilpolemeq1  14037  apdifflemf  14043