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  6425  nqnq0a  6436  nqnq0m  6437  nq0m0r  6438  nq0a0  6439  nnanq0  6440  distrnq0  6441  prarloclemlo  6476  prarloclemcalc  6484  genpassl  6507  genpassu  6508  ltsosr  6652  0idsr  6655  1idsr  6656  mulextsr1lem  6666  cnegex  6946  subsub3  6999  subadd4  7011  mulneg12  7150  mulsub  7154  apreap  7331  cru  7346  recextlem1  7374  cju  7654  halfaddsub  7896  nn0supp  7970  nneo  8077  zeo2  8080  uzin  8241  iccf1o  8602  fzsuc2  8671  frec2uzrdg  8836  iseqfveq2  8865  expp1  8876  mulexp  8908  mulexpzap  8909  expadd  8911  expaddzap  8913  expmul  8914  expmulzap  8915  expsubap  8916  expdivap  8919  subsq  8971  binom3  8979  bernneq  8982  crre  9045  remim  9048  remullem  9059  cjexp  9081  cnrecnv  9098