Theorem eqtr4d 2148

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

Syntax hints:   → wi 4   = wceq 1312

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-17 1487  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-cleq 2106

This theorem is referenced by:  3eqtr2d  2151  3eqtr2rd  2152  3eqtr4d  2155  3eqtr4rd  2156  3eqtr4a  2171  sbnfc2  3024  ifsbdc  3450  ifeq1dadc  3466  eqifdc  3470  ifandc  3472  onsucuni2  4437  relop  4647  riinint  4756  iotauni  5056  fniinfv  5431  fsn2  5546  fmptapd  5563  fconst2g  5587  fniunfv  5615  ofres  5948  ofco  5952  frecsuclem  6255  frecrdg  6257  oasuc  6312  nnacom  6332  nnaass  6333  nndi  6334  nnmass  6335  nnmsucr  6336  nnmcom  6337  funresdfunsndc  6354  uniqs2  6441  en1bg  6646  fundmen  6652  1domsn  6664  mapxpen  6693  xpmapenlem  6694  phplem4dom  6707  en2eqpr  6752  sbthlemi5  6799  omp1eomlem  6929  difinfsnlem  6934  ctmlemr  6943  ctssdccl  6946  ctssdc  6948  infnninf  6970  addcmpblnq  7117  distrnqg  7137  ltexnqq  7158  addcmpblnq0  7193  nqnq0a  7204  nqnq0m  7205  nq0m0r  7206  nq0a0  7207  nnanq0  7208  distrnq0  7209  prarloclemlo  7244  prarloclemcalc  7252  genpassl  7274  genpassu  7275  ltsosr  7501  0idsr  7504  1idsr  7505  mulextsr1lem  7516  cnegex  7857  subsub3  7911  subadd4  7923  mulneg12  8072  mulsub  8076  apreap  8261  cru  8276  recextlem1  8319  cju  8623  halfaddsub  8852  nn0supp  8927  nneo  9052  zeo2  9055  uzin  9254  xaddcom  9531  xaddass  9539  xleaddadd  9557  iccf1o  9674  fzsuc2  9746  flqeqceilz  9978  zmod1congr  10001  modqcyc  10019  modqcyc2  10020  modqaddabs  10022  modqmul1  10037  modqaddmulmod  10051  addmodlteq  10058  frec2uzrdg  10069  frecuzrdgsuctlem  10083  seq3val  10118  seqvalcd  10119  seq3fveq2  10129  seq3split  10139  seq3distr  10173  ser0f  10175  expp1  10187  mulexp  10219  mulexpzap  10220  expadd  10222  expaddzap  10224  expmul  10225  expmulzap  10226  expsubap  10228  expdivap  10231  subsq  10286  mulbinom2  10295  binom3  10296  bernneq  10299  nn0opthd  10355  faclbnd  10374  faclbnd6  10377  bccmpl  10387  bcp1n  10394  zfz1isolemiso  10469  seq3coll  10472  shftval2  10485  shftval4  10487  seq3shft  10497  crre  10516  remim  10519  remullem  10530  cjexp  10552  cnrecnv  10569  resqrexlemlo  10671  resqrexlemcalc1  10672  resqrexlemcalc2  10673  resqrexlemcalc3  10674  resqrexlemnm  10676  rsqrmo  10685  abscj  10710  absid  10729  absre  10735  recvalap  10755  maxabsle  10862  maxltsup  10876  2zsupmax  10883  minabs  10893  bdtrilem  10896  bdtri  10897  xrmaxiflemab  10902  xrmaxiflemcom  10904  xrmaxadd  10916  xrbdtri  10931  iooinsup  10932  climaddc1  10984  climmulc2  10986  climsubc1  10987  climsubc2  10988  climcvg1nlem  11004  summodclem3  11035  zsumdc  11039  isum  11040  isumz  11044  isumss  11046  fisumss  11047  fsum3cvg2  11049  fsumadd  11061  isummulc2  11081  sumsplitdc  11087  fsum2dlemstep  11089  fisumcom2  11093  fisum0diag2  11102  fsumconst  11109  telfsumo  11121  fsumparts  11125  fsumrelem  11126  binomlem  11138  isumshft  11145  isumsplit  11146  arisum  11153  arisum2  11154  trireciplem  11155  geolim2  11167  geo2sum  11169  0.999...  11176  cvgratz  11187  mertensabs  11192  ef0lem  11211  efval2  11216  ege2le3  11222  efaddlem  11225  efsub  11232  eftlub  11241  efsep  11242  tanval3ap  11266  efi4p  11269  sinneg  11278  sinmul  11296  sincossq  11300  cos2t  11302  demoivreALT  11324  eirraplem  11325  odd2np1  11412  omoe  11435  divalglemex  11461  divalglemeuneg  11462  divalgmod  11466  flodddiv4  11473  gcdneg  11512  gcdaddm  11514  modgcd  11521  bezoutlemnewy  11524  gcdass  11543  gcdmultiple  11548  algrp1  11567  lcmneg  11595  lcmgcdeq  11604  lcmass  11606  cncongr2  11625  prmexpb  11669  sqrt2irr  11680  2sqpwodd  11693  qnumdenbi  11709  phiprmpw  11737  ctiunctlemfo  11789  strslfv3  11841  restuni2  12183  lmfval  12198  cnfval  12200  cnpfval  12201  txtopon  12267  txcnp  12276  upxp  12277  txrest  12281  cnmptcom  12303  bl2in  12386  xblss2  12388  isxms2  12435  setsmsdsg  12463  setsmstsetg  12464  metss  12477  resubmet  12528  cncfcncntop  12560  dvidlemap  12609  dvcnp2cntop  12612  0nninf  12878  nninfalllemn  12883  trilpolemisumle  12912