Theorem eqtr4d 2075

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

Hypotheses

Ref	Expression
eqtr4d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐵)

Assertion

Ref	Expression
eqtr4d	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtr4d

Step	Hyp	Ref	Expression
1		eqtr4d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	2	eqcomd 2045	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eqtrd 2072	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1243

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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

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

This theorem is referenced by:  3eqtr2d  2078  3eqtr2rd  2079  3eqtr4d  2082  3eqtr4rd  2083  3eqtr4a  2098  sbnfc2  2906  onsucuni2  4288  relop  4486  riinint  4593  iotauni  4879  fniinfv  5231  fsn2  5337  fmptapd  5354  fconst2g  5376  fniunfv  5401  ofres  5725  ofco  5729  frecsuclem2  5989  frecrdg  5992  oasuc  6044  nnacom  6063  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  nnmcom  6068  uniqs2  6166  en1bg  6280  fundmen  6286  phplem4dom  6324  addcmpblnq  6463  distrnqg  6483  ltexnqq  6504  addcmpblnq0  6539  nqnq0a  6550  nqnq0m  6551  nq0m0r  6552  nq0a0  6553  nnanq0  6554  distrnq0  6555  prarloclemlo  6590  prarloclemcalc  6598  genpassl  6620  genpassu  6621  ltsosr  6847  0idsr  6850  1idsr  6851  mulextsr1lem  6862  cnegex  7187  subsub3  7241  subadd4  7253  mulneg12  7392  mulsub  7396  apreap  7576  cru  7591  recextlem1  7630  cju  7911  halfaddsub  8157  nn0supp  8232  nneo  8339  zeo2  8342  uzin  8503  iccf1o  8870  fzsuc2  8939  flqeqceilz  9158  frec2uzrdg  9169  iseqss  9200  iseqfveq2  9202  iseqsplit  9212  iseqdistr  9223  iser0f  9225  expp1  9236  mulexp  9268  mulexpzap  9269  expadd  9271  expaddzap  9273  expmul  9274  expmulzap  9275  expsubap  9276  expdivap  9279  subsq  9332  binom3  9340  bernneq  9343  shftval2  9401  shftval4  9403  crre  9431  remim  9434  remullem  9445  cjexp  9467  cnrecnv  9484  resqrexlemlo  9585  resqrexlemcalc1  9586  resqrexlemcalc2  9587  resqrexlemcalc3  9588  resqrexlemnm  9590  rsqrmo  9599  abscj  9624  absid  9643  absre  9647  recvalap  9667  climaddc1  9823  climmulc2  9825  climsubc1  9826  climsubc2  9827  climcvg1nlem  9842  sqrt2irr  9852  ialgrp1  9859