Theorem 3eqtrd 2233

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  tpeq123d  3715  diftpsn3  3764  oteq123d  3824  resiima  5028  fvun1  5630  fvmptd  5645  fmptpr  5757  caovlem2d  6120  offval  6147  ofvalg  6149  cnvf1olem  6291  nnm1  6592  updjudhcoinlf  7155  updjudhcoinrg  7156  caseinl  7166  caseinr  7167  omp1eomlem  7169  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  ltexnqq  7494  prarloclemarch  7504  ltrnqg  7506  nq02m  7551  prarloclemcalc  7588  mulnqprl  7654  mulnqpru  7655  ltexprlemloc  7693  addcanprleml  7700  recexprlem1ssu  7720  cauappcvgprlem1  7745  caucvgsrlemfv  7877  caucvgsrlemoffval  7882  recidpirqlemcalc  7943  axmulass  7959  axrnegex  7965  muladd11r  8201  addcan2  8226  addsub  8256  subsub2  8273  negsubdi2  8304  muladd  8429  mulsub  8446  cru  8648  mulreim  8650  recextlem1  8697  mulap0  8700  muleqadd  8714  divrecap  8734  div23ap  8737  div12ap  8740  divmulasscomap  8742  divcanap7  8767  conjmulap  8775  apmul1  8834  nndivtr  9051  subhalfhalf  9245  xp1d2m1eqxm1d2  9263  div4p1lem1div2  9264  qapne  9732  xnegneg  9927  rexsub  9947  xnegid  9953  fseq1p1m1  10188  nn0split  10230  nnsplit  10231  fzosplitsnm1  10304  fzosplitprm1  10329  ceilid  10426  flqdiv  10432  zmod10  10451  modqcyc  10470  modqaddabs  10473  mulqaddmodid  10475  modqadd2mod  10485  modqm1p1mod0  10486  modqmul12d  10489  modqadd12d  10491  modqmulmodr  10501  modqaddmulmod  10502  frecuzrdgsuc  10525  seqeq123d  10567  seqvalcd  10572  seq3f1olemqsumkj  10622  seq3f1oleml  10627  seqf1oglem2  10631  seq3id3  10635  seq3id  10636  seq3homo  10638  seq3z  10639  seqhomog  10641  exp1  10656  expnegap0  10658  expmulzap  10696  m1expeven  10697  expdivap  10701  binom3  10768  sqoddm1div8  10804  mulsubdivbinom2ap  10822  bcn1  10869  bcnp1n  10870  bcval5  10874  bcn2m1  10880  bcn2p1  10881  hashdifpr  10931  crim  11042  remullem  11055  remul2  11057  immul2  11064  ipcnval  11070  cjreim  11087  recvguniqlem  11178  resqrexlemover  11194  resqrexlemcalc1  11198  absid  11255  amgm2  11302  max0addsup  11403  minabs  11420  xrmaxrecl  11439  xrminadd  11459  fsumsplitf  11592  sumsnf  11593  fsump1i  11617  fsum2dlemstep  11618  fsumshftm  11629  fsummulc2  11632  modfsummodlemstep  11641  telfsumo  11650  fsumrelem  11655  hash2iun1dif1  11664  binomlem  11667  binom1dif  11671  arisum  11682  geo2sum  11698  geo2sum2  11699  cvgratz  11716  mertenslemi1  11719  clim2prod  11723  fprodeq0  11801  fprod2dlemstep  11806  fproddivap  11814  fproddivapf  11815  fprodmodd  11825  ef0lem  11844  eftlub  11874  efsep  11875  effsumlt  11876  tanval2ap  11897  efi4p  11901  resin4p  11902  recos4p  11903  efeul  11918  sinadd  11920  cosadd  11921  sinmul  11928  ef01bndlem  11940  cos12dec  11952  absef  11954  demoivreALT  11958  dvds2ln  12008  dvdseq  12032  opeo  12081  bezoutlemnewy  12190  nninfctlemfo  12234  eucalginv  12251  eucalglt  12252  eucalg  12254  lcmgcdlem  12272  lcm1  12276  divgcdcoprmex  12297  2sqpwodd  12371  zgcdsq  12396  qden1elz  12400  phiprmpw  12417  eulerthlem1  12422  eulerthlemrprm  12424  prmdiv  12430  hashgcdlem  12433  odzdvds  12441  vfermltl  12447  modprm0  12450  pythagtriplem12  12471  pcqmul  12499  pcaddlem  12535  pcadd  12536  pcadd2  12537  pcmpt  12539  pcmpt2  12540  mul4sqlem  12589  4sqlem11  12597  4sqlem17  12603  nninfdclemp1  12694  ressressg  12780  gsumsplit1r  13102  gsumprval  13103  mndinvmod  13149  mhmco  13194  gsumfzz  13199  grpinvid2  13257  grpasscan2  13268  grpinvssd  13281  grpinvadd  13282  grpsubid1  13289  grpsubadd  13292  grppncan  13295  mulg1  13337  mulgaddcomlem  13353  mulgdirlem  13361  mulgneg2  13364  mulgmodid  13369  nmzsubg  13418  qusinv  13444  qussub  13445  conjnmz  13487  ablsub2inv  13519  abladdsub4  13522  abladdsub  13523  ablpncan2  13524  ablpnpcan  13528  ablnncan  13529  invghm  13537  gsumfzconst  13549  gsumfzsnfd  13553  rngm2neg  13583  srgpcompp  13625  srgpcomppsc  13626  ringinvnzdiv  13684  ringm2neg  13689  dvr1  13772  dvrcan1  13774  dvrcan3  13775  rdivmuldivd  13778  lmodfopne  13960  sralemg  14072  gsumfzfsumlemm  14221  mplsubgfilemcl  14333  mplsubgfileminv  14334  xmetxpbl  14852  ivthinclemuopn  14982  limcimolemlt  15008  cnplimcim  15011  limccnpcntop  15019  limccnp2lem  15020  dvexp  15055  dvmptcmulcn  15065  dvply1  15109  ef2kpi  15150  sinhalfpip  15164  sinhalfpim  15165  coshalfpim  15167  ptolemy  15168  tangtx  15182  rpabscxpbnd  15284  relogbexpap  15302  rplogbcxp  15307  rpcxplogb  15308  binom4  15323  wilthlem1  15324  0sgm  15329  mpodvdsmulf1o  15334  fsumdvdsmul  15335  sgmppw  15336  0sgmppw  15337  1sgm2ppw  15339  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgsval2lem  15359  lgsval4  15369  lgsval4a  15371  lgsneg  15373  lgsneg1  15374  lgsdirprm  15383  lgsdir  15384  lgsne0  15387  lgsmulsqcoprm  15395  gausslemma2dlem1a  15407  gausslemma2dlem6  15416  gausslemma2d  15418  lgseisenlem3  15421  lgseisenlem4  15422  lgseisen  15423  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2lem1  15430  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgslem3d1  15449  2sqlem3  15466  peano4nninf  15761  trilpolemclim  15793  trilpolemeq1  15797  apdifflemf  15803