Theorem 3eqtr3d 2198

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtr3d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3d	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr3d

Step	Hyp	Ref	Expression
1		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3	1, 2	eqtr3d 2192	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	eqtr3d 2192	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1335

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139

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

This theorem is referenced by:  mpteqb  5558  fvmptt  5559  fsnunfv  5668  f1ocnvfv1  5727  f1ocnvfv2  5728  fcof1  5733  caov12d  6002  caov13d  6004  caov411d  6006  caovimo  6014  grprinvlem  6015  grprinvd  6016  grpridd  6017  tfrlem5  6261  tfrlemiubacc  6277  tfr1onlemubacc  6293  tfrcllemubacc  6306  nndir  6437  fopwdom  6781  updjud  7026  omp1eomlem  7038  addassnqg  7302  distrnqg  7307  enq0tr  7354  distrnq0  7379  distnq0r  7383  addnqprl  7449  addnqpru  7450  appdivnq  7483  ltmprr  7562  addcmpblnr  7659  mulcmpblnrlemg  7660  ltsrprg  7667  1idsr  7688  pn0sr  7691  mulgt0sr  7698  map2psrprg  7725  axmulass  7793  ax0id  7798  recriota  7810  mul12  8004  mul4  8007  readdcan  8015  add12  8033  cnegexlem2  8051  addcan  8055  ppncan  8117  addsub4  8118  subeqxfrd  8238  subaddeqd  8244  muladd  8259  mulcanapd  8535  receuap  8543  div13ap  8566  divdivdivap  8586  divcanap5  8587  divdivap1  8596  divdivap2  8597  halfaddsub  9067  fztp  9980  fseq1p1m1  9996  flqzadd  10197  flqdiv  10220  mulp1mod1  10264  modqnegd  10278  modqsub12d  10280  q2submod  10284  modsumfzodifsn  10295  seq3m1  10367  seq3caopr  10382  iseqf1olemab  10388  iseqf1olemnanb  10389  seq3f1olemqsumk  10398  exprecap  10460  expsubap  10467  zesq  10536  nn0opthlem1d  10594  facnn2  10608  faclbnd6  10618  zfz1isolemsplit  10709  seq3coll  10713  shftval3  10727  crre  10757  resub  10770  imsub  10778  cjsub  10792  bdtrilem  11138  bdtri  11139  climshft2  11203  nnf1o  11273  fsumf1o  11287  isumss  11288  fisumss  11289  fsumadd  11303  isumclim3  11320  fsummulc2  11345  fsumsub  11349  telfsumo  11363  telfsumo2  11364  hashiun  11375  bcxmas  11386  isumshft  11387  trireciplem  11397  geoserap  11404  geo2sum2  11412  fprodf1o  11485  prodssdc  11486  fprodssdc  11487  fprodmul  11488  fprodm1  11495  sinsub  11637  cossub  11638  p1modz1  11690  gcdaddm  11867  modgcd  11874  bezoutlemnewy  11879  absmulgcd  11900  gcdmultiplez  11904  eucalg  11935  lcmgcd  11954  lcmid  11956  numdensq  12076  dfphi2  12094  phiprm  12097  fermltl  12108  prmdiveq  12110  hashgcdlem  12112  odzdvds  12119  ennnfonelem1  12136  ennnfonelemex  12143  topnpropgd  12365  restin  12576  blpnfctr  12839  xmssym  12869  limcimolemlt  13033  dvmulxxbr  13066  dvrecap  13077  dvmptaddx  13081  dvmptmulx  13082  dvmptnegcn  13084  dvmptsubcn  13085  dvmptcjx  13086  dveflem  13087  sin0pilem1  13102  ptolemy  13145  tangtx  13159  rpcxpneg  13228  rpcxpsub  13229  cxprec  13231  rpcxproot  13234  cxpcom  13257  rpabscxpbnd  13259  peano4nninf  13578  nninfalllem1  13580  nninfall  13581  nninfsellemqall  13587  qdencn  13598