Theorem 3eqtr3d 2121

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 2115	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	eqtr3d 2115	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  mpteqb  5282  fvmptt  5283  fsnunfv  5384  f1ocnvfv1  5437  f1ocnvfv2  5438  fcof1  5443  caov12d  5702  caov13d  5704  caov411d  5706  caovimo  5714  grprinvlem  5715  grprinvd  5716  grpridd  5717  tfrlem5  5953  tfrlemiubacc  5967  nndir  6092  fopwdom  6333  addassnqg  6572  distrnqg  6577  enq0tr  6624  distrnq0  6649  distnq0r  6653  addnqprl  6719  addnqpru  6720  appdivnq  6753  ltmprr  6832  addcmpblnr  6916  mulcmpblnrlemg  6917  ltsrprg  6924  1idsr  6945  pn0sr  6948  mulgt0sr  6954  axmulass  7039  ax0id  7044  recriota  7056  mul12  7237  mul4  7240  readdcan  7248  add12  7266  cnegexlem2  7284  addcan  7288  ppncan  7350  addsub4  7351  subaddeqd  7473  muladd  7488  mulcanapd  7751  receuap  7759  div13ap  7781  divdivdivap  7801  divcanap5  7802  divdivap1  7811  divdivap2  7812  halfaddsub  8265  fztp  9095  fseq1p1m1  9111  flqzadd  9300  flqdiv  9323  mulp1mod1  9367  modqnegd  9381  modqsub12d  9383  q2submod  9387  modsumfzodifsn  9398  iseqm1  9447  iseqcaopr  9462  exprecap  9517  expsubap  9524  zesq  9591  nn0opthlem1d  9647  facnn2  9661  faclbnd6  9671  shftval3  9715  crre  9744  resub  9757  imsub  9765  cjsub  9779  climshft2  10145  gcdaddm  10375  modgcd  10382  bezoutlemnewy  10385  absmulgcd  10406  gcdmultiplez  10410  eucialg  10441  lcmgcd  10460  lcmid  10462  qdencn  10785