Theorem eqtr4d 2116

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 2086	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eqtrd 2113	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  3eqtr2d  2119  3eqtr2rd  2120  3eqtr4d  2123  3eqtr4rd  2124  3eqtr4a  2139  sbnfc2  2962  ifsbdc  3363  ifeq1dadc  3379  onsucuni2  4307  relop  4504  riinint  4611  iotauni  4899  fniinfv  5252  fsn2  5358  fmptapd  5375  fconst2g  5397  fniunfv  5422  ofres  5745  ofco  5749  frecsuclem2  6012  frecrdg  6015  oasuc  6067  nnacom  6086  nnaass  6087  nndi  6088  nnmass  6089  nnmsucr  6090  nnmcom  6091  uniqs2  6189  en1bg  6303  fundmen  6309  phplem4dom  6348  en2eqpr  6380  addcmpblnq  6557  distrnqg  6577  ltexnqq  6598  addcmpblnq0  6633  nqnq0a  6644  nqnq0m  6645  nq0m0r  6646  nq0a0  6647  nnanq0  6648  distrnq0  6649  prarloclemlo  6684  prarloclemcalc  6692  genpassl  6714  genpassu  6715  ltsosr  6941  0idsr  6944  1idsr  6945  mulextsr1lem  6956  cnegex  7286  subsub3  7340  subadd4  7352  mulneg12  7501  mulsub  7505  apreap  7687  cru  7702  recextlem1  7741  cju  8038  halfaddsub  8265  nn0supp  8340  nneo  8450  zeo2  8453  uzin  8651  iccf1o  9026  fzsuc2  9096  flqeqceilz  9320  zmod1congr  9343  modqcyc  9361  modqcyc2  9362  modqaddabs  9364  modqmul1  9379  modqaddmulmod  9393  addmodlteq  9400  frec2uzrdg  9411  iseqss  9446  iseqfveq2  9448  iseqsplit  9458  iseqdistr  9470  iser0f  9472  expp1  9483  mulexp  9515  mulexpzap  9516  expadd  9518  expaddzap  9520  expmul  9521  expmulzap  9522  expsubap  9524  expdivap  9527  subsq  9581  mulbinom2  9589  binom3  9590  bernneq  9593  nn0opthd  9649  faclbnd  9668  faclbnd6  9671  bccmpl  9681  bcp1n  9688  shftval2  9714  shftval4  9716  crre  9744  remim  9747  remullem  9758  cjexp  9780  cnrecnv  9797  resqrexlemlo  9899  resqrexlemcalc1  9900  resqrexlemcalc2  9901  resqrexlemcalc3  9902  resqrexlemnm  9904  rsqrmo  9913  abscj  9938  absid  9957  absre  9963  recvalap  9983  maxabsle  10090  maxltsup  10104  climaddc1  10167  climmulc2  10169  climsubc1  10170  climsubc2  10171  climcvg1nlem  10186  odd2np1  10272  omoe  10296  divalglemex  10322  divalglemeuneg  10323  divalgmod  10327  flodddiv4  10334  gcdneg  10373  gcdaddm  10375  modgcd  10382  bezoutlemnewy  10385  gcdass  10404  gcdmultiple  10409  ialgrp1  10428  lcmneg  10456  lcmgcdeq  10465  lcmass  10467  cncongr2  10486  prmexpb  10530  sqrt2irr  10541  2sqpwodd  10554