Theorem eqtr4d 2120

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

Syntax hints:   → wi 4   = wceq 1287

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 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067

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

This theorem is referenced by:  3eqtr2d  2123  3eqtr2rd  2124  3eqtr4d  2127  3eqtr4rd  2128  3eqtr4a  2143  sbnfc2  2977  ifsbdc  3391  ifeq1dadc  3407  eqifdc  3411  ifandc  3413  onsucuni2  4353  relop  4554  riinint  4662  iotauni  4958  fniinfv  5325  fsn2  5434  fmptapd  5451  fconst2g  5473  fniunfv  5502  ofres  5826  ofco  5830  frecsuclem  6125  frecrdg  6127  oasuc  6179  nnacom  6199  nnaass  6200  nndi  6201  nnmass  6202  nnmsucr  6203  nnmcom  6204  uniqs2  6304  en1bg  6469  fundmen  6475  1domsn  6487  mapxpen  6516  xpmapenlem  6517  phplem4dom  6530  en2eqpr  6575  sbthlemi5  6614  djur  6701  infnninf  6749  addcmpblnq  6870  distrnqg  6890  ltexnqq  6911  addcmpblnq0  6946  nqnq0a  6957  nqnq0m  6958  nq0m0r  6959  nq0a0  6960  nnanq0  6961  distrnq0  6962  prarloclemlo  6997  prarloclemcalc  7005  genpassl  7027  genpassu  7028  ltsosr  7254  0idsr  7257  1idsr  7258  mulextsr1lem  7269  cnegex  7604  subsub3  7658  subadd4  7670  mulneg12  7819  mulsub  7823  apreap  8005  cru  8020  recextlem1  8059  cju  8356  halfaddsub  8583  nn0supp  8658  nneo  8782  zeo2  8785  uzin  8983  iccf1o  9353  fzsuc2  9423  flqeqceilz  9653  zmod1congr  9676  modqcyc  9694  modqcyc2  9695  modqaddabs  9697  modqmul1  9712  modqaddmulmod  9726  addmodlteq  9733  frec2uzrdg  9744  frecuzrdgsuctlem  9758  iseqvalt  9790  iseqoveq  9798  iseqss  9799  iseqsst  9800  iseqfveq2  9802  iseqsplit  9812  iseqdistr  9846  iser0f  9848  expp1  9860  mulexp  9892  mulexpzap  9893  expadd  9895  expaddzap  9897  expmul  9898  expmulzap  9899  expsubap  9901  expdivap  9904  subsq  9958  mulbinom2  9966  binom3  9967  bernneq  9970  nn0opthd  10026  faclbnd  10045  faclbnd6  10048  bccmpl  10058  bcp1n  10065  zfz1isolemiso  10140  iseqcoll  10143  shftval2  10156  shftval4  10158  crre  10186  remim  10189  remullem  10200  cjexp  10222  cnrecnv  10239  resqrexlemlo  10341  resqrexlemcalc1  10342  resqrexlemcalc2  10343  resqrexlemcalc3  10344  resqrexlemnm  10346  rsqrmo  10355  abscj  10380  absid  10399  absre  10405  recvalap  10425  maxabsle  10532  maxltsup  10546  climaddc1  10609  climmulc2  10611  climsubc1  10612  climsubc2  10613  climcvg1nlem  10628  isummolem3  10659  zisum  10663  iisum  10664  isumz  10667  isumss  10669  fisumss  10670  odd2np1  10748  omoe  10771  divalglemex  10797  divalglemeuneg  10798  divalgmod  10802  flodddiv4  10809  gcdneg  10848  gcdaddm  10850  modgcd  10857  bezoutlemnewy  10860  gcdass  10879  gcdmultiple  10884  ialgrp1  10903  lcmneg  10931  lcmgcdeq  10940  lcmass  10942  cncongr2  10961  prmexpb  11005  sqrt2irr  11016  2sqpwodd  11029  qnumdenbi  11045  phiprmpw  11073  0nninf  11331  nninfalllemn  11336