Theorem eqtrdi 2253

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
eqtrdi	⊢ (𝜑 → 𝐴 = 𝐶)

Proof of Theorem eqtrdi

Step	Hyp	Ref	Expression
1		eqtrdi.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtrdi.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	a1i 9	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4	1, 3	eqtrd 2237	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197

This theorem is referenced by:  eqtr2di  2254  eqtr4di  2255  3eqtr3g  2260  3eqtr4a  2263  cbvralcsf  3155  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  csbprc  3505  un00  3506  disjssun  3523  disjpr2  3696  tppreq3  3735  diftpsn3  3773  preq12b  3810  intsng  3918  uniintsnr  3920  rint0  3923  riin0  3998  iununir  4010  intexr  4193  exmid1stab  4251  sucprc  4457  op1stbg  4524  elreldm  4902  xpeq0r  5102  xpdisj1  5104  xpdisj2  5105  resdisj  5108  xpima1  5126  xpima2m  5127  elxp4  5167  unixp0im  5216  uniabio  5239  iotass  5246  cnvresid  5342  funimacnv  5344  fimadmfo  5501  f1o00  5551  dffv4g  5567  fv2prc  5607  fnrnfv  5619  feqresmpt  5627  dffn5imf  5628  funfvdm2f  5638  fvun1  5639  fvmpt2  5657  fndmin  5681  fmptcof  5741  fmptcos  5742  fvunsng  5768  fvpr1  5778  fnrnov  6082  offval  6156  ofrfval  6157  op1std  6224  op2ndd  6225  fmpoco  6292  tpostpos  6340  tfr0  6399  rdgival  6458  frec0g  6473  2oconcl  6515  om0  6534  oei0  6535  oasuc  6540  omv2  6541  nnm0r  6555  uniqs2  6672  en1  6876  en1bg  6877  fundmen  6883  mapsnen  6888  xpsnen  6898  xpcomco  6903  xpdom2  6908  xpmapenlem  6928  exmidpweq  6988  unsnfidcex  6999  fiintim  7010  ssfirab  7015  sbthlemi8  7048  elfi2  7056  fi0  7059  fieq0  7060  djudom  7177  ismkvnex  7239  nninfwlpoimlemg  7259  en2other2  7286  exmidfodomrlemim  7291  nq0m0r  7551  addpinq1  7559  genipv  7604  genpelvl  7607  genpelvu  7608  cauappcvgprlem1  7754  caucvgsrlemoffres  7895  addresr  7932  mulresr  7933  axcnre  7976  add20  8529  rimul  8640  rereim  8641  mulreim  8659  sup3exmid  9012  fv0p1e1  9133  div4p1lem1div2  9273  nnm1nn0  9318  znegcl  9385  peano2z  9390  nneoor  9457  nn0ind-raph  9472  xnegneg  9937  xltnegi  9939  xaddpnf1  9950  xnegid  9963  xnn0xadd0  9971  xnegdi  9972  xsubge0  9985  xposdif  9986  xlesubadd  9987  xleaddadd  9991  fz0to4untppr  10228  fzo0to2pr  10328  nninfdcex  10361  fldiv4p1lem1div2  10429  fldiv4lem1div2  10431  mulp1mod1  10491  frecfzennn  10552  iseqf1olemqk  10633  exp0  10669  expp1  10672  expnegap0  10673  1exp  10694  mulexp  10704  m1expeven  10712  sq0i  10757  bernneq  10786  facp1  10856  faclbnd3  10869  facubnd  10871  bcval5  10889  hashinfom  10904  hashsng  10924  hashxp  10952  resunimafz0  10957  zfz1iso  10967  lsw1  11018  imre  11081  reim0b  11092  rereb  11093  resqrexlemover  11240  resqrexlemcalc1  11244  abs00bd  11296  maxabslemlub  11437  xrmaxiflemcom  11479  xrmaxadd  11491  climconst  11520  isumz  11619  fsumf1o  11620  fsumcllem  11629  fsumadd  11636  fsumxp  11666  fsumcnv  11667  fsummulc2  11678  fsumconst  11684  fsumabs  11695  telfsumo  11696  fsumparts  11700  fsumrelem  11701  fsumiun  11707  binomlem  11713  binom  11714  binom11  11716  isumsplit  11721  arisum  11728  arisum2  11729  trireciplem  11730  georeclim  11743  cvgratnnlemseq  11756  prodfrecap  11776  prod1dc  11816  fprodf1o  11818  fprodcl2lem  11835  fprodcllem  11836  fprodfac  11845  fprod2d  11853  fprodxp  11854  fprodcnv  11855  fprodrec  11859  fprodmodd  11871  ef0lem  11890  ege2le3  11901  efaddlem  11904  efcan  11906  eft0val  11923  ef4p  11924  efgt1p2  11925  efi4p  11947  sincossq  11978  cos2tsin  11981  absefi  11999  demoivreALT  12004  p1modz1  12024  dvdsabseq  12077  odd2np1lem  12102  oddp1even  12106  opoe  12125  m1expo  12130  m1exp1  12131  nn0o1gt2  12135  bitsinv1  12192  gcddvds  12203  gcdcl  12206  gcdeq0  12217  gcd0id  12219  bezoutr1  12273  nnmindc  12274  nnminle  12275  eucalg  12300  lcm0val  12306  lcmid  12321  rpmul  12339  dfphi2  12461  phiprmpw  12463  hashgcdeq  12481  odzdvds  12487  nnnn0modprm0  12497  pythagtriplem4  12510  pythagtriplem12  12517  pcaddlem  12581  pcmpt  12585  pockthi  12600  4sqlem12  12644  2expltfac  12681  ennnfonelem0  12695  ennnfonelem1  12697  ennnfonelemhdmp1  12699  ennnfonelemkh  12702  ennnfonelemhf1o  12703  ennnfonelemf1  12708  ctiunctlemfo  12729  setsresg  12789  strressid  12822  strle1g  12857  restid2  12998  prdsbas3  13037  gsumwmhm  13248  grplactcnv  13352  mulg0  13379  mulgnn0gsum  13382  mulgneg  13394  mulgneg2  13410  gsumfzconst  13595  gsumfzsnfd  13599  gsumfzfsumlem0  14266  zrhval2  14299  mpl0fi  14382  tgval2  14441  tgidm  14464  epttop  14480  tgrest  14559  restco  14564  restsn  14570  tgcn  14598  cnptopresti  14628  cnptoprest  14629  txbas  14648  upxp  14662  txrest  14666  txdis  14667  txhmeo  14709  txswaphmeolem  14710  xblss2ps  14794  xblss2  14795  qtopbasss  14911  fsumcncntop  14957  hoverb  15038  limcimolemlt  15054  dvcnp2cntop  15089  dvcoapbr  15097  dvexp  15101  dvexp2  15102  dvmptid  15106  dveflem  15116  dvef  15117  plymullem1  15138  plyadd  15141  plymul  15142  plycoeid3  15147  plycjlemc  15150  plycj  15151  sin0pilem1  15171  sin2kpi  15201  cos2kpi  15202  coseq0q4123  15224  coseq0negpitopi  15226  sincosq1eq  15229  sinkpi  15237  coskpi  15238  1cxp  15290  mpodvdsmulf1o  15380  lgslem2  15396  lgsfcl2  15401  lgs0  15408  lgs2  15412  lgsneg  15419  lgsdilem  15422  lgsdir2lem4  15426  lgsdir2lem5  15427  lgsne0  15433  lgssq  15435  lgssq2  15436  gausslemma2dlem3  15458  gausslemma2dlem4  15459  lgseisenlem1  15465  lgsquadlem2  15473  lgsquad2lem2  15477  lgsquad3  15479  m1lgs  15480  2lgslem1a2  15482  2lgsoddprmlem3  15506  2sqlem9  15519  2sqlem10  15520  ex-ceil  15526  bj-intexr  15708  peano3nninf  15808  nninfall  15810  isomninnlem  15833  iswomni0  15854  ismkvnnlem  15855  nconstwlpolem0  15866