Theorem 3eqtrd 2271

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  tpeq123d  3789  diftpsn3  3841  oteq123d  3904  resiima  5127  fvun1  5750  fvmptd  5765  fmptpr  5883  caovlem2d  6257  offval  6285  ofvalg  6287  cnvf1olem  6435  supp0  6453  suppsnopdc  6465  suppofss1dcl  6479  suppofss2dcl  6480  suppcofn  6481  nnm1  6773  updjudhcoinlf  7386  updjudhcoinrg  7387  caseinl  7397  caseinr  7398  omp1eomlem  7400  exmidfodomrlemr  7520  exmidfodomrlemrALT  7521  ltexnqq  7741  prarloclemarch  7751  ltrnqg  7753  nq02m  7798  prarloclemcalc  7835  mulnqprl  7901  mulnqpru  7902  ltexprlemloc  7940  addcanprleml  7947  recexprlem1ssu  7967  cauappcvgprlem1  7992  caucvgsrlemfv  8124  caucvgsrlemoffval  8129  recidpirqlemcalc  8190  axmulass  8206  axrnegex  8212  muladd11r  8448  addcan2  8473  addsub  8503  subsub2  8520  negsubdi2  8551  muladd  8677  mulsub  8694  cru  8896  mulreim  8898  recextlem1  8945  mulap0  8948  muleqadd  8964  divrecap  8984  div23ap  8987  div12ap  8990  divmulasscomap  8992  divcanap7  9017  conjmulap  9025  apmul1  9084  nndivtr  9301  subhalfhalf  9495  xp1d2m1eqxm1d2  9513  div4p1lem1div2  9514  qapne  9994  xnegneg  10190  rexsub  10210  xnegid  10216  fseq1p1m1  10455  nn0split  10497  nnsplit  10498  fzosplitsnm1  10581  fzosplitpr  10606  fzosplitprm1  10607  ceilid  10706  flqdiv  10712  zmod10  10731  modqcyc  10750  modqaddabs  10753  mulqaddmodid  10755  modqadd2mod  10765  modqm1p1mod0  10766  modqmul12d  10769  modqadd12d  10771  modqmulmodr  10781  modqaddmulmod  10782  frecuzrdgsuc  10805  seqeq123d  10847  seqvalcd  10852  seq3f1olemqsumkj  10902  seq3f1oleml  10907  seqf1oglem2  10911  seq3id3  10915  seq3id  10916  seq3homo  10918  seq3z  10919  seqhomog  10921  exp1  10936  expnegap0  10938  expmulzap  10976  m1expeven  10977  expdivap  10981  binom3  11048  sqoddm1div8  11085  mulsubdivbinom2ap  11103  bcn1  11150  bcnp1n  11151  bcval5  11155  bcn2m1  11162  bcn2p1  11163  hashdifpr  11215  hashmap  11222  hashfibclem  11236  ccatlen  11313  ccatalpha  11331  ccatw2s1leng  11356  ccats1val2  11358  lswccats1  11361  swrdlend  11380  ccatswrd  11392  pfxmpt  11402  pfxfv  11406  pfxfvlsw  11417  ccatpfx  11423  pfx1  11425  pfxswrd  11428  swrdpfx  11429  pfxpfx  11430  lenrevpfxcctswrd  11434  wrdind  11444  wrd2ind  11445  swrdccatin2  11451  pfxccatin12lem2  11453  pfxccatpfx2  11459  pfxccatid  11463  cats1fvnd  11487  crim  11573  remullem  11586  remul2  11588  immul2  11595  ipcnval  11601  cjreim  11619  recvguniqlem  11710  resqrexlemover  11726  resqrexlemcalc1  11730  absid  11787  amgm2  11834  max0addsup  11935  minabs  11952  xrmaxrecl  11971  xrminadd  11991  fsumsplitf  12125  sumsnf  12126  fsump1i  12150  fsum2dlemstep  12151  fsumshftm  12162  fsummulc2  12165  modfsummodlemstep  12174  telfsumo  12183  fsumrelem  12188  hash2iun1dif1  12197  binomlem  12200  binom1dif  12204  arisum  12215  geo2sum  12231  geo2sum2  12232  cvgratz  12249  mertenslemi1  12252  clim2prod  12256  fprodeq0  12334  fprod2dlemstep  12339  fproddivap  12347  fproddivapf  12348  fprodmodd  12358  ef0lem  12377  eftlub  12407  efsep  12408  effsumlt  12409  tanval2ap  12430  efi4p  12434  resin4p  12435  recos4p  12436  efeul  12451  sinadd  12453  cosadd  12454  sinmul  12461  ef01bndlem  12473  cos12dec  12485  absef  12487  demoivreALT  12491  dvds2ln  12541  dvdseq  12565  opeo  12614  bezoutlemnewy  12723  nninfctlemfo  12767  eucalginv  12784  eucalglt  12785  eucalg  12787  lcmgcdlem  12805  lcm1  12809  divgcdcoprmex  12830  2sqpwodd  12904  zgcdsq  12929  qden1elz  12933  phiprmpw  12950  eulerthlem1  12955  eulerthlemrprm  12957  prmdiv  12963  hashgcdlem  12966  odzdvds  12974  vfermltl  12980  modprm0  12983  pythagtriplem12  13004  pcqmul  13032  pcaddlem  13068  pcadd  13069  pcadd2  13070  pcmpt  13072  pcmpt2  13073  mul4sqlem  13122  4sqlem11  13130  4sqlem17  13136  ballotfilemfp1  13181  ballotfilemfmpn  13184  ballotfilemsi  13208  nninfdclemp1  13291  ressressg  13378  gsumsplit1r  13667  gsumprval  13668  mndinvmod  13712  mhmco  13751  gsumfzz  13756  grpinvid2  13814  grpasscan2  13825  grpinvssd  13838  grpinvadd  13839  grpsubid1  13846  grpsubadd  13849  grppncan  13852  mulg1  13888  mulgaddcomlem  13904  mulgdirlem  13912  mulgneg2  13915  mulgmodid  13920  nmzsubg  13969  qusinv  13995  qussub  13996  conjnmz  14038  ablsub2inv  14070  abladdsub4  14073  abladdsub  14074  ablpncan2  14075  ablpnpcan  14079  ablnncan  14080  invghm  14088  gsumfzconst  14100  gsumfzsnfd  14104  gfsumval  14108  gfsumsn  14113  gfsumz  14115  rngm2neg  14194  srgpcompp  14240  srgpcomppsc  14241  ringinvnzdiv  14299  ringm2neg  14304  dvr1  14389  dvrcan1  14391  dvrcan3  14392  rdivmuldivd  14395  lmodfopne  14606  sralemg  14718  gsumfzfsumlemm  14867  mplsubgfilemcl  14986  mplsubgfileminv  14987  xmetxpbl  15505  ivthinclemuopn  15635  limcimolemlt  15661  cnplimcim  15664  limccnpcntop  15672  limccnp2lem  15673  dvexp  15708  dvmptcmulcn  15718  dvply1  15762  ef2kpi  15803  sinhalfpip  15817  sinhalfpim  15818  coshalfpim  15820  ptolemy  15821  tangtx  15835  rpabscxpbnd  15937  relogbexpap  15955  rplogbcxp  15960  rpcxplogb  15961  binom4  15976  pellexlem2  15978  wilthlem1  15980  0sgm  15985  mpodvdsmulf1o  15990  fsumdvdsmul  15991  sgmppw  15992  0sgmppw  15993  1sgm2ppw  15995  perfectlem1  15999  perfectlem2  16000  perfect  16001  lgsval2lem  16015  lgsval4  16025  lgsval4a  16027  lgsneg  16029  lgsneg1  16030  lgsdirprm  16039  lgsdir  16040  lgsne0  16043  lgsmulsqcoprm  16051  gausslemma2dlem1a  16063  gausslemma2dlem6  16072  gausslemma2d  16074  lgseisenlem3  16077  lgseisenlem4  16078  lgseisen  16079  lgsquadlem1  16082  lgsquadlem2  16083  lgsquad2lem1  16086  2lgslem3a  16098  2lgslem3b  16099  2lgslem3c  16100  2lgslem3d  16101  2lgslem3d1  16105  2sqlem3  16122  structiedg0val  16167  uhgr2edg  16333  usgr1e  16368  vtxdgfifival  16418  vtxdfifiun  16424  vtxdumgrfival  16425  vtxduspgrfvedgfi  16428  1loopgredg  16431  1loopgrvd2fi  16432  1hevtxdg1en  16435  p1evtxdeqfi  16439  edginwlkd  16482  clwwlknonex2lem1  16564  eupthvdres  16602  peano4nninf  16926  repiecele0  16952  repiecege0  16953  trilpolemclim  16962  trilpolemeq1  16966  apdifflemf  16972