Theorem eqtr4d 2173

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

Syntax hints:   → wi 4   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

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

This theorem is referenced by:  3eqtr2d  2176  3eqtr2rd  2177  3eqtr4d  2180  3eqtr4rd  2181  3eqtr4a  2196  sbnfc2  3055  ifsbdc  3481  ifeq1dadc  3497  eqifdc  3501  ifandc  3503  onsucuni2  4474  relop  4684  riinint  4795  iotauni  5095  fniinfv  5472  fsn2  5587  fmptapd  5604  fconst2g  5628  fniunfv  5656  ofres  5989  ofco  5993  frecsuclem  6296  frecrdg  6298  oasuc  6353  nnacom  6373  nnaass  6374  nndi  6375  nnmass  6376  nnmsucr  6377  nnmcom  6378  funresdfunsndc  6395  uniqs2  6482  en1bg  6687  fundmen  6693  1domsn  6706  mapxpen  6735  xpmapenlem  6736  phplem4dom  6749  en2eqpr  6794  sbthlemi5  6842  omp1eomlem  6972  difinfsnlem  6977  ctmlemr  6986  ctssdccl  6989  ctssdc  6991  infnninf  7015  exmidonfinlem  7042  addcmpblnq  7168  distrnqg  7188  ltexnqq  7209  addcmpblnq0  7244  nqnq0a  7255  nqnq0m  7256  nq0m0r  7257  nq0a0  7258  nnanq0  7259  distrnq0  7260  prarloclemlo  7295  prarloclemcalc  7303  genpassl  7325  genpassu  7326  ltsosr  7565  0idsr  7568  1idsr  7569  mulextsr1lem  7581  cnegex  7933  subsub3  7987  subadd4  7999  mulneg12  8152  mulsub  8156  apreap  8342  cru  8357  recextlem1  8405  cju  8712  halfaddsub  8947  nn0supp  9022  nneo  9147  zeo2  9150  uzin  9351  xaddcom  9637  xaddass  9645  xleaddadd  9663  iccf1o  9780  fzsuc2  9852  flqeqceilz  10084  zmod1congr  10107  modqcyc  10125  modqcyc2  10126  modqaddabs  10128  modqmul1  10143  modqaddmulmod  10157  addmodlteq  10164  frec2uzrdg  10175  frecuzrdgsuctlem  10189  seq3val  10224  seqvalcd  10225  seq3fveq2  10235  seq3split  10245  seq3distr  10279  ser0f  10281  expp1  10293  mulexp  10325  mulexpzap  10326  expadd  10328  expaddzap  10330  expmul  10331  expmulzap  10332  expsubap  10334  expdivap  10337  subsq  10392  mulbinom2  10401  binom3  10402  bernneq  10405  nn0opthd  10461  faclbnd  10480  faclbnd6  10483  bccmpl  10493  bcp1n  10500  zfz1isolemiso  10575  seq3coll  10578  shftval2  10591  shftval4  10593  seq3shft  10603  crre  10622  remim  10625  remullem  10636  cjexp  10658  cnrecnv  10675  resqrexlemlo  10778  resqrexlemcalc1  10779  resqrexlemcalc2  10780  resqrexlemcalc3  10781  resqrexlemnm  10783  rsqrmo  10792  abscj  10817  absid  10836  absre  10842  recvalap  10862  maxabsle  10969  maxltsup  10983  2zsupmax  10990  minabs  11000  bdtrilem  11003  bdtri  11004  xrmaxiflemab  11009  xrmaxiflemcom  11011  xrmaxadd  11023  xrbdtri  11038  iooinsup  11039  climaddc1  11091  climmulc2  11093  climsubc1  11094  climsubc2  11095  climcvg1nlem  11111  summodclem3  11142  zsumdc  11146  isum  11147  isumz  11151  isumss  11153  fisumss  11154  fsum3cvg2  11156  fsumadd  11168  isummulc2  11188  sumsplitdc  11194  fsum2dlemstep  11196  fisumcom2  11200  fisum0diag2  11209  fsumconst  11216  telfsumo  11228  fsumparts  11232  fsumrelem  11233  binomlem  11245  isumshft  11252  isumsplit  11253  arisum  11260  arisum2  11261  trireciplem  11262  geolim2  11274  geo2sum  11276  0.999...  11283  cvgratz  11294  mertensabs  11299  clim2prod  11301  prodf1f  11305  ef0lem  11355  efval2  11360  ege2le3  11366  efaddlem  11369  efsub  11376  eftlub  11385  efsep  11386  tanval3ap  11410  efi4p  11413  sinneg  11422  sinmul  11440  sincossq  11444  cos2t  11446  demoivreALT  11469  eirraplem  11472  odd2np1  11559  omoe  11582  divalglemex  11608  divalglemeuneg  11609  divalgmod  11613  flodddiv4  11620  gcdneg  11659  gcdaddm  11661  modgcd  11668  bezoutlemnewy  11673  gcdass  11692  gcdmultiple  11697  algrp1  11716  lcmneg  11744  lcmgcdeq  11753  lcmass  11755  cncongr2  11774  prmexpb  11818  sqrt2irr  11829  2sqpwodd  11843  qnumdenbi  11859  phiprmpw  11887  ctiunctlemfo  11941  strslfv3  11993  restuni2  12335  lmfval  12350  cnfval  12352  cnpfval  12353  txtopon  12420  txcnp  12429  upxp  12430  txrest  12434  cnmptcom  12456  bl2in  12561  xblss2  12563  isxms2  12610  setsmsdsg  12638  setsmstsetg  12639  metss  12652  resubmet  12706  cncfcncntop  12738  dvidlemap  12818  dvcnp2cntop  12821  dvcoapbr  12829  dvcjbr  12830  dvexp  12833  dvexp2  12834  dvrecap  12835  efimpi  12889  tangtx  12908  0nninf  13186  nninfalllemn  13191  trilpolemisumle  13220