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  6506  genpassu  6507  ltsosr  6672  0idsr  6675  1idsr  6676  mulextsr1lem  6686  cnegex  6966  subsub3  7019  subadd4  7031  mulneg12  7170  mulsub  7174  apreap  7351  cru  7366  recextlem1  7394  cju  7674  halfaddsub  7916  nn0supp  7990  nneo  8097  zeo2  8100  uzin  8261  iccf1o  8622  fzsuc2  8691  frec2uzrdg  8856  iseqfveq2  8885  expp1  8896  mulexp  8928  mulexpzap  8929  expadd  8931  expaddzap  8933  expmul  8934  expmulzap  8935  expsubap  8936  expdivap  8939  subsq  8991  binom3  8999  bernneq  9002  crre  9065  remim  9068  remullem  9079  cjexp  9101  cnrecnv  9118  abscj  9200  absid  9205  absre  9208