Theorem 3eqtrd 2202

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

Syntax hints:   → wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  tpeq123d  3668  diftpsn3  3714  oteq123d  3773  resiima  4962  fvun1  5552  fvmptd  5567  fmptpr  5677  caovlem2d  6034  offval  6057  ofvalg  6059  cnvf1olem  6192  nnm1  6492  updjudhcoinlf  7045  updjudhcoinrg  7046  caseinl  7056  caseinr  7057  omp1eomlem  7059  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  ltexnqq  7349  prarloclemarch  7359  ltrnqg  7361  nq02m  7406  prarloclemcalc  7443  mulnqprl  7509  mulnqpru  7510  ltexprlemloc  7548  addcanprleml  7555  recexprlem1ssu  7575  cauappcvgprlem1  7600  caucvgsrlemfv  7732  caucvgsrlemoffval  7737  recidpirqlemcalc  7798  axmulass  7814  axrnegex  7820  muladd11r  8054  addcan2  8079  addsub  8109  subsub2  8126  negsubdi2  8157  muladd  8282  mulsub  8299  cru  8500  mulreim  8502  recextlem1  8548  mulap0  8551  muleqadd  8565  divrecap  8584  div23ap  8587  div12ap  8590  divmulasscomap  8592  divcanap7  8617  conjmulap  8625  apmul1  8684  nndivtr  8899  xp1d2m1eqxm1d2  9109  div4p1lem1div2  9110  qapne  9577  xnegneg  9769  rexsub  9789  xnegid  9795  fseq1p1m1  10029  nn0split  10071  nnsplit  10072  fzosplitsnm1  10144  fzosplitprm1  10169  ceilid  10250  flqdiv  10256  zmod10  10275  modqcyc  10294  modqaddabs  10297  mulqaddmodid  10299  modqadd2mod  10309  modqm1p1mod0  10310  modqmul12d  10313  modqadd12d  10315  modqmulmodr  10325  modqaddmulmod  10326  frecuzrdgsuc  10349  seqeq123d  10389  seqvalcd  10394  seq3f1olemqsumkj  10433  seq3f1oleml  10438  seq3id3  10442  seq3id  10443  seq3homo  10445  seq3z  10446  exp1  10461  expnegap0  10463  expmulzap  10501  m1expeven  10502  expdivap  10506  binom3  10572  sqoddm1div8  10608  bcn1  10671  bcnp1n  10672  bcval5  10676  bcn2m1  10682  bcn2p1  10683  hashdifpr  10733  crim  10800  remullem  10813  remul2  10815  immul2  10822  ipcnval  10828  cjreim  10845  recvguniqlem  10936  resqrexlemover  10952  resqrexlemcalc1  10956  absid  11013  amgm2  11060  max0addsup  11161  minabs  11177  xrmaxrecl  11196  xrminadd  11216  fsumsplitf  11349  sumsnf  11350  fsump1i  11374  fsum2dlemstep  11375  fsumshftm  11386  fsummulc2  11389  modfsummodlemstep  11398  telfsumo  11407  fsumrelem  11412  hash2iun1dif1  11421  binomlem  11424  binom1dif  11428  arisum  11439  geo2sum  11455  geo2sum2  11456  cvgratz  11473  mertenslemi1  11476  clim2prod  11480  fprodeq0  11558  fprod2dlemstep  11563  fproddivap  11571  fproddivapf  11572  fprodmodd  11582  ef0lem  11601  eftlub  11631  efsep  11632  effsumlt  11633  tanval2ap  11654  efi4p  11658  resin4p  11659  recos4p  11660  efeul  11675  sinadd  11677  cosadd  11678  sinmul  11685  ef01bndlem  11697  cos12dec  11708  absef  11710  demoivreALT  11714  dvds2ln  11764  dvdseq  11786  opeo  11834  bezoutlemnewy  11929  eucalginv  11988  eucalglt  11989  eucalg  11991  lcmgcdlem  12009  lcm1  12013  divgcdcoprmex  12034  2sqpwodd  12108  zgcdsq  12133  qden1elz  12137  phiprmpw  12154  eulerthlem1  12159  eulerthlemrprm  12161  prmdiv  12167  hashgcdlem  12170  odzdvds  12177  vfermltl  12183  modprm0  12186  pythagtriplem12  12207  pcqmul  12235  pcaddlem  12270  pcadd  12271  pcmpt  12273  pcmpt2  12274  mul4sqlem  12323  nninfdclemp1  12383  xmetxpbl  13148  ivthinclemuopn  13256  limcimolemlt  13273  cnplimcim  13276  limccnpcntop  13284  limccnp2lem  13285  dvexp  13315  dvmptcmulcn  13323  ef2kpi  13367  sinhalfpip  13381  sinhalfpim  13382  coshalfpim  13384  ptolemy  13385  tangtx  13399  rpabscxpbnd  13499  relogbexpap  13516  rplogbcxp  13521  rpcxplogb  13522  binom4  13537  lgsval2lem  13551  lgsval4  13561  lgsval4a  13563  lgsneg  13565  lgsneg1  13566  lgsdirprm  13575  lgsdir  13576  lgsne0  13579  lgsmulsqcoprm  13587  2sqlem3  13593  peano4nninf  13886  trilpolemclim  13915  trilpolemeq1  13919  apdifflemf  13925