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  3675  diftpsn3  3721  oteq123d  3780  resiima  4969  fvun1  5562  fvmptd  5577  fmptpr  5688  caovlem2d  6045  offval  6068  ofvalg  6070  cnvf1olem  6203  nnm1  6504  updjudhcoinlf  7057  updjudhcoinrg  7058  caseinl  7068  caseinr  7069  omp1eomlem  7071  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  ltexnqq  7370  prarloclemarch  7380  ltrnqg  7382  nq02m  7427  prarloclemcalc  7464  mulnqprl  7530  mulnqpru  7531  ltexprlemloc  7569  addcanprleml  7576  recexprlem1ssu  7596  cauappcvgprlem1  7621  caucvgsrlemfv  7753  caucvgsrlemoffval  7758  recidpirqlemcalc  7819  axmulass  7835  axrnegex  7841  muladd11r  8075  addcan2  8100  addsub  8130  subsub2  8147  negsubdi2  8178  muladd  8303  mulsub  8320  cru  8521  mulreim  8523  recextlem1  8569  mulap0  8572  muleqadd  8586  divrecap  8605  div23ap  8608  div12ap  8611  divmulasscomap  8613  divcanap7  8638  conjmulap  8646  apmul1  8705  nndivtr  8920  xp1d2m1eqxm1d2  9130  div4p1lem1div2  9131  qapne  9598  xnegneg  9790  rexsub  9810  xnegid  9816  fseq1p1m1  10050  nn0split  10092  nnsplit  10093  fzosplitsnm1  10165  fzosplitprm1  10190  ceilid  10271  flqdiv  10277  zmod10  10296  modqcyc  10315  modqaddabs  10318  mulqaddmodid  10320  modqadd2mod  10330  modqm1p1mod0  10331  modqmul12d  10334  modqadd12d  10336  modqmulmodr  10346  modqaddmulmod  10347  frecuzrdgsuc  10370  seqeq123d  10410  seqvalcd  10415  seq3f1olemqsumkj  10454  seq3f1oleml  10459  seq3id3  10463  seq3id  10464  seq3homo  10466  seq3z  10467  exp1  10482  expnegap0  10484  expmulzap  10522  m1expeven  10523  expdivap  10527  binom3  10593  sqoddm1div8  10629  bcn1  10692  bcnp1n  10693  bcval5  10697  bcn2m1  10703  bcn2p1  10704  hashdifpr  10755  crim  10822  remullem  10835  remul2  10837  immul2  10844  ipcnval  10850  cjreim  10867  recvguniqlem  10958  resqrexlemover  10974  resqrexlemcalc1  10978  absid  11035  amgm2  11082  max0addsup  11183  minabs  11199  xrmaxrecl  11218  xrminadd  11238  fsumsplitf  11371  sumsnf  11372  fsump1i  11396  fsum2dlemstep  11397  fsumshftm  11408  fsummulc2  11411  modfsummodlemstep  11420  telfsumo  11429  fsumrelem  11434  hash2iun1dif1  11443  binomlem  11446  binom1dif  11450  arisum  11461  geo2sum  11477  geo2sum2  11478  cvgratz  11495  mertenslemi1  11498  clim2prod  11502  fprodeq0  11580  fprod2dlemstep  11585  fproddivap  11593  fproddivapf  11594  fprodmodd  11604  ef0lem  11623  eftlub  11653  efsep  11654  effsumlt  11655  tanval2ap  11676  efi4p  11680  resin4p  11681  recos4p  11682  efeul  11697  sinadd  11699  cosadd  11700  sinmul  11707  ef01bndlem  11719  cos12dec  11730  absef  11732  demoivreALT  11736  dvds2ln  11786  dvdseq  11808  opeo  11856  bezoutlemnewy  11951  eucalginv  12010  eucalglt  12011  eucalg  12013  lcmgcdlem  12031  lcm1  12035  divgcdcoprmex  12056  2sqpwodd  12130  zgcdsq  12155  qden1elz  12159  phiprmpw  12176  eulerthlem1  12181  eulerthlemrprm  12183  prmdiv  12189  hashgcdlem  12192  odzdvds  12199  vfermltl  12205  modprm0  12208  pythagtriplem12  12229  pcqmul  12257  pcaddlem  12292  pcadd  12293  pcmpt  12295  pcmpt2  12296  mul4sqlem  12345  nninfdclemp1  12405  mndinvmod  12678  mhmco  12705  grpinvid2  12755  grpasscan2  12763  xmetxpbl  13302  ivthinclemuopn  13410  limcimolemlt  13427  cnplimcim  13430  limccnpcntop  13438  limccnp2lem  13439  dvexp  13469  dvmptcmulcn  13477  ef2kpi  13521  sinhalfpip  13535  sinhalfpim  13536  coshalfpim  13538  ptolemy  13539  tangtx  13553  rpabscxpbnd  13653  relogbexpap  13670  rplogbcxp  13675  rpcxplogb  13676  binom4  13691  lgsval2lem  13705  lgsval4  13715  lgsval4a  13717  lgsneg  13719  lgsneg1  13720  lgsdirprm  13729  lgsdir  13730  lgsne0  13733  lgsmulsqcoprm  13741  2sqlem3  13747  peano4nninf  14039  trilpolemclim  14068  trilpolemeq1  14072  apdifflemf  14078