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  4429  riinint  4536  iotauni  4822  fniinfv  5174  fsn2  5280  fmptapd  5297  fconst2g  5319  fniunfv  5344  ofres  5667  ofco  5671  frecsuclem2  5928  frecrdg  5931  oasuc  5983  nnacom  6002  nnaass  6003  nndi  6004  nnmass  6005  nnmsucr  6006  nnmcom  6007  uniqs2  6102  en1bg  6216  fundmen  6222  addcmpblnq  6351  distrnqg  6371  ltexnqq  6391  addcmpblnq0  6426  nqnq0a  6437  nqnq0m  6438  nq0m0r  6439  nq0a0  6440  nnanq0  6441  distrnq0  6442  prarloclemlo  6477  prarloclemcalc  6485  genpassl  6507  genpassu  6508  ltsosr  6692  0idsr  6695  1idsr  6696  mulextsr1lem  6706  cnegex  6986  subsub3  7039  subadd4  7051  mulneg12  7190  mulsub  7194  apreap  7371  cru  7386  recextlem1  7414  cju  7694  halfaddsub  7936  nn0supp  8010  nneo  8117  zeo2  8120  uzin  8281  iccf1o  8642  fzsuc2  8711  frec2uzrdg  8876  iseqfveq2  8905  expp1  8916  mulexp  8948  mulexpzap  8949  expadd  8951  expaddzap  8953  expmul  8954  expmulzap  8955  expsubap  8956  expdivap  8959  subsq  9011  binom3  9019  bernneq  9022  crre  9085  remim  9088  remullem  9099  cjexp  9121  cnrecnv  9138  abscj  9220  absid  9225  absre  9228