Theorem eqtr4d 2388

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

Hypotheses

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

Assertion

Ref	Expression
eqtr4d	⊢ (φ → A = C)

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 ⊢ (φ → A = B)
2		eqtr4d.2	. . 3 ⊢ (φ → C = B)
3	2	eqcomd 2358	. 2 ⊢ (φ → B = C)
4	1, 3	eqtrd 2385	1 ⊢ (φ → A = 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:  3eqtr2d  2391  3eqtr2rd  2392  3eqtr4d  2395  3eqtr4rd  2396  3eqtr4a  2411  sbnfc2  3197  ifsb  3672  ifeq1da  3688  ifeq2da  3689  ifnot  3701  ifan  3702  ifor  3703  setswith  4322  iotauni  4352  dfiota3  4371  dfiota4  4373  nnsucelrlem3  4427  nnpw1ex  4485  tfin11  4494  sfin112  4530  fveqres  5356  funfv  5376  fsn2  5435  fvunsn  5445  fconst2g  5453  ndmovcom  5618  ndmovass  5619  ndmovdistr  5620  fvmpti  5700  fvmptex  5722  fvfullfun  5865  uniqs2  5986  enprmaplem3  6079  nchoicelem7  6296  nchoicelem15  6304  nchoicelem17  6306  fnfrec  6321