Theorem 3eqtrd 2214

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  tpeq123d  3684  diftpsn3  3733  oteq123d  3792  resiima  4983  fvun1  5579  fvmptd  5594  fmptpr  5705  caovlem2d  6062  offval  6085  ofvalg  6087  cnvf1olem  6220  nnm1  6521  updjudhcoinlf  7074  updjudhcoinrg  7075  caseinl  7085  caseinr  7086  omp1eomlem  7088  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  ltexnqq  7402  prarloclemarch  7412  ltrnqg  7414  nq02m  7459  prarloclemcalc  7496  mulnqprl  7562  mulnqpru  7563  ltexprlemloc  7601  addcanprleml  7608  recexprlem1ssu  7628  cauappcvgprlem1  7653  caucvgsrlemfv  7785  caucvgsrlemoffval  7790  recidpirqlemcalc  7851  axmulass  7867  axrnegex  7873  muladd11r  8107  addcan2  8132  addsub  8162  subsub2  8179  negsubdi2  8210  muladd  8335  mulsub  8352  cru  8553  mulreim  8555  recextlem1  8602  mulap0  8605  muleqadd  8619  divrecap  8639  div23ap  8642  div12ap  8645  divmulasscomap  8647  divcanap7  8672  conjmulap  8680  apmul1  8739  nndivtr  8955  xp1d2m1eqxm1d2  9165  div4p1lem1div2  9166  qapne  9633  xnegneg  9827  rexsub  9847  xnegid  9853  fseq1p1m1  10087  nn0split  10129  nnsplit  10130  fzosplitsnm1  10202  fzosplitprm1  10227  ceilid  10308  flqdiv  10314  zmod10  10333  modqcyc  10352  modqaddabs  10355  mulqaddmodid  10357  modqadd2mod  10367  modqm1p1mod0  10368  modqmul12d  10371  modqadd12d  10373  modqmulmodr  10383  modqaddmulmod  10384  frecuzrdgsuc  10407  seqeq123d  10447  seqvalcd  10452  seq3f1olemqsumkj  10491  seq3f1oleml  10496  seq3id3  10500  seq3id  10501  seq3homo  10503  seq3z  10504  exp1  10519  expnegap0  10521  expmulzap  10559  m1expeven  10560  expdivap  10564  binom3  10630  sqoddm1div8  10666  bcn1  10729  bcnp1n  10730  bcval5  10734  bcn2m1  10740  bcn2p1  10741  hashdifpr  10791  crim  10858  remullem  10871  remul2  10873  immul2  10880  ipcnval  10886  cjreim  10903  recvguniqlem  10994  resqrexlemover  11010  resqrexlemcalc1  11014  absid  11071  amgm2  11118  max0addsup  11219  minabs  11235  xrmaxrecl  11254  xrminadd  11274  fsumsplitf  11407  sumsnf  11408  fsump1i  11432  fsum2dlemstep  11433  fsumshftm  11444  fsummulc2  11447  modfsummodlemstep  11456  telfsumo  11465  fsumrelem  11470  hash2iun1dif1  11479  binomlem  11482  binom1dif  11486  arisum  11497  geo2sum  11513  geo2sum2  11514  cvgratz  11531  mertenslemi1  11534  clim2prod  11538  fprodeq0  11616  fprod2dlemstep  11621  fproddivap  11629  fproddivapf  11630  fprodmodd  11640  ef0lem  11659  eftlub  11689  efsep  11690  effsumlt  11691  tanval2ap  11712  efi4p  11716  resin4p  11717  recos4p  11718  efeul  11733  sinadd  11735  cosadd  11736  sinmul  11743  ef01bndlem  11755  cos12dec  11766  absef  11768  demoivreALT  11772  dvds2ln  11822  dvdseq  11844  opeo  11892  bezoutlemnewy  11987  eucalginv  12046  eucalglt  12047  eucalg  12049  lcmgcdlem  12067  lcm1  12071  divgcdcoprmex  12092  2sqpwodd  12166  zgcdsq  12191  qden1elz  12195  phiprmpw  12212  eulerthlem1  12217  eulerthlemrprm  12219  prmdiv  12225  hashgcdlem  12228  odzdvds  12235  vfermltl  12241  modprm0  12244  pythagtriplem12  12265  pcqmul  12293  pcaddlem  12328  pcadd  12329  pcmpt  12331  pcmpt2  12332  mul4sqlem  12381  nninfdclemp1  12441  ressressg  12524  mndinvmod  12774  mhmco  12802  grpinvid2  12853  grpasscan2  12862  grpinvssd  12875  grpinvadd  12876  grpsubid1  12883  grpsubadd  12886  grppncan  12889  mulg1  12918  mulgaddcomlem  12933  mulgdirlem  12941  mulgneg2  12944  mulgmodid  12949  ablsub2inv  13014  abladdsub4  13017  abladdsub  13018  ablpncan2  13019  ablpnpcan  13023  ablnncan  13024  srgpcompp  13074  srgpcomppsc  13075  ringinvnzdiv  13127  ringm2neg  13132  dvr1  13206  dvrcan1  13208  dvrcan3  13209  rdivmuldivd  13212  xmetxpbl  13790  ivthinclemuopn  13898  limcimolemlt  13915  cnplimcim  13918  limccnpcntop  13926  limccnp2lem  13927  dvexp  13957  dvmptcmulcn  13965  ef2kpi  14009  sinhalfpip  14023  sinhalfpim  14024  coshalfpim  14026  ptolemy  14027  tangtx  14041  rpabscxpbnd  14141  relogbexpap  14158  rplogbcxp  14163  rpcxplogb  14164  binom4  14179  lgsval2lem  14193  lgsval4  14203  lgsval4a  14205  lgsneg  14207  lgsneg1  14208  lgsdirprm  14217  lgsdir  14218  lgsne0  14221  lgsmulsqcoprm  14229  2sqlem3  14235  peano4nninf  14526  trilpolemclim  14555  trilpolemeq1  14559  apdifflemf  14565