Theorem eqtr4d 2053

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

Hypotheses

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

Assertion

Ref	Expression
eqtr4d	⊢ (φ → A = 𝐶)

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 ⊢ (φ → A = B)
2		eqtr4d.2	. . 3 ⊢ (φ → 𝐶 = B)
3	2	eqcomd 2023	. 2 ⊢ (φ → B = 𝐶)
4	1, 3	eqtrd 2050	1 ⊢ (φ → A = 𝐶)

Syntax hints:   → wi 4   = wceq 1226

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-gen 1314  ax-4 1377  ax-17 1396  ax-ext 2000

This theorem depends on definitions:  df-bi 110  df-cleq 2011

This theorem is referenced by:  3eqtr2d  2056  3eqtr2rd  2057  3eqtr4d  2060  3eqtr4rd  2061  3eqtr4a  2076  sbnfc2  2879  relop  4409  riinint  4516  iotauni  4802  fniinfv  5152  fsn2  5258  fmptapd  5275  fconst2g  5297  fniunfv  5322  ofres  5644  ofco  5648  frecsuclem2  5901  frecrdg  5904  oasuc  5955  nnacom  5974  nnaass  5975  nndi  5976  nnmass  5977  nnmsucr  5978  nnmcom  5979  uniqs2  6073  addcmpblnq  6220  distrnqg  6240  ltexnqq  6260  addcmpblnq0  6292  nqnq0a  6303  nqnq0m  6304  nq0m0r  6305  nq0a0  6306  nnanq0  6307  distrnq0  6308  prarloclemlo  6342  prarloclemcalc  6350  genpassl  6373  genpassu  6374  ltsosr  6505  0idsr  6508  1idsr  6509  cnegex  6776  subsub3  6829  subadd4  6841  mulneg12  6980  mulsub  6984