Theorem eqtr4d 2072

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 2042	. 2 ⊢ (φ → B = 𝐶)
4	1, 3	eqtrd 2069	1 ⊢ (φ → A = 𝐶)

Syntax hints:   → wi 4   = wceq 1242

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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019

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

This theorem is referenced by:  3eqtr2d  2075  3eqtr2rd  2076  3eqtr4d  2079  3eqtr4rd  2080  3eqtr4a  2095  sbnfc2  2900  relop  4428  riinint  4535  iotauni  4821  fniinfv  5172  fsn2  5278  fmptapd  5295  fconst2g  5317  fniunfv  5342  ofres  5664  ofco  5668  frecsuclem2  5922  frecrdg  5925  oasuc  5976  nnacom  5995  nnaass  5996  nndi  5997  nnmass  5998  nnmsucr  5999  nnmcom  6000  uniqs2  6095  en1bg  6209  fundmen  6215  addcmpblnq  6344  distrnqg  6364  ltexnqq  6384  addcmpblnq0  6418  nqnq0a  6429  nqnq0m  6430  nq0m0r  6431  nq0a0  6432  nnanq0  6433  distrnq0  6434  prarloclemlo  6469  prarloclemcalc  6477  genpassl  6500  genpassu  6501  ltsosr  6644  0idsr  6647  1idsr  6648  mulextsr1lem  6658  cnegex  6938  subsub3  6991  subadd4  7003  mulneg12  7142  mulsub  7146  apreap  7323  cru  7338  recextlem1  7366  cju  7645  halfaddsub  7886  nn0supp  7960  nneo  8066  zeo2  8069  uzin  8230  iccf1o  8590  fzsuc2  8657