Theorem eqtr3d 2387

Description: An equality transitivity equality deduction. (Contributed by NM, 18-Jul-1995.)

Hypotheses

Ref	Expression
eqtr3d.1	⊢ (φ → A = B)
eqtr3d.2	⊢ (φ → A = C)

Assertion

Ref	Expression
eqtr3d	⊢ (φ → B = C)

Proof of Theorem eqtr3d

Step	Hyp	Ref	Expression
1		eqtr3d.1	. . 3 ⊢ (φ → A = B)
2	1	eqcomd 2358	. 2 ⊢ (φ → B = A)
3		eqtr3d.2	. 2 ⊢ (φ → A = C)
4	2, 3	eqtrd 2385	1 ⊢ (φ → B = C)

Syntax hints:   → wi 4   = wceq 1642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346

This theorem is referenced by:  3eqtr3d  2393  3eqtr3rd  2394  3eqtr3a  2409  uniintsn  3964  f00  5250  f1imacnv  5303  foimacnv  5304  fvsnun2  5449  oprssov  5604  caovmo  5646  fvfullfunlem3  5864  ecss  5967  uniqs2  5986  map0b  6025  enprmaplem3  6079  ncdisjun  6137  ncspw1eu  6160  addcdi  6251  nchoicelem17  6306