Theorem eqtrdi 2278

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 2262	1 ⊢ (𝜑 → 𝐴 = 𝐶)

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqtr2di  2279  eqtr4di  2280  3eqtr3g  2285  3eqtr4a  2288  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  csbprc  3537  un00  3538  disjssun  3555  disjpr2  3730  tppreq3  3769  diftpsn3  3809  ssprsseq  3830  preq12b  3848  intsng  3957  uniintsnr  3959  rint0  3962  riin0  4037  iununir  4049  intexr  4235  exmid1stab  4293  sucprc  4504  op1stbg  4571  elreldm  4953  xpeq0r  5154  xpdisj1  5156  xpdisj2  5157  resdisj  5160  xpima1  5178  xpima2m  5179  elxp4  5219  unixp0im  5268  uniabio  5292  iotass  5299  cnvresid  5398  funimacnv  5400  fimadmfo  5562  f1o00  5613  dffv4g  5629  fv2prc  5671  fnrnfv  5685  feqresmpt  5693  dffn5imf  5694  funfvdm2f  5704  fvun1  5705  fvmpt2  5723  fndmin  5747  fmptcof  5807  fmptcos  5808  funopdmsn  5826  fvunsng  5840  fvpr1  5850  fnrnov  6160  offval  6235  ofrfval  6236  op1std  6303  op2ndd  6304  fmpoco  6373  tpostpos  6421  tfr0  6480  rdgival  6539  frec0g  6554  2oconcl  6598  om0  6617  oei0  6618  oasuc  6623  omv2  6624  nnm0r  6638  uniqs2  6755  en1  6964  en1bg  6965  fundmen  6972  mapsnen  6977  en2  6986  xpsnen  6993  xpcomco  6998  xpdom2  7003  xpmapenlem  7023  exmidpweq  7087  unsnfidcex  7098  fiintim  7109  ssfirab  7114  sbthlemi8  7147  elfi2  7155  fi0  7158  fieq0  7159  djudom  7276  ismkvnex  7338  nninfwlpoimlemg  7358  en2other2  7390  exmidfodomrlemim  7395  nq0m0r  7659  addpinq1  7667  genipv  7712  genpelvl  7715  genpelvu  7716  cauappcvgprlem1  7862  caucvgsrlemoffres  8003  addresr  8040  mulresr  8041  axcnre  8084  add20  8637  rimul  8748  rereim  8749  mulreim  8767  sup3exmid  9120  fv0p1e1  9241  div4p1lem1div2  9381  nnm1nn0  9426  znegcl  9493  peano2z  9498  nneoor  9565  nn0ind-raph  9580  xnegneg  10046  xltnegi  10048  xaddpnf1  10059  xnegid  10072  xnn0xadd0  10080  xnegdi  10081  xsubge0  10094  xposdif  10095  xlesubadd  10096  xleaddadd  10100  fz0to4untppr  10337  fzo0to2pr  10441  nninfdcex  10474  fldiv4p1lem1div2  10542  fldiv4lem1div2  10544  mulp1mod1  10604  frecfzennn  10665  iseqf1olemqk  10746  exp0  10782  expp1  10785  expnegap0  10786  1exp  10807  mulexp  10817  m1expeven  10825  sq0i  10870  bernneq  10899  facp1  10969  faclbnd3  10982  facubnd  10984  bcval5  11002  hashinfom  11017  hashsng  11037  hashxp  11066  resunimafz0  11071  zfz1iso  11081  hash2en  11083  lsw1  11139  s1rn  11171  eqs1  11181  ccat1st1st  11193  swrd00g  11202  swrdlend  11211  swrds1  11221  cats1lend  11320  cats2catd  11322  s2leng  11342  s2dmg  11343  imre  11383  reim0b  11394  rereb  11395  resqrexlemover  11542  resqrexlemcalc1  11546  abs00bd  11598  maxabslemlub  11739  xrmaxiflemcom  11781  xrmaxadd  11793  climconst  11822  isumz  11921  fsumf1o  11922  fsumcllem  11931  fsumadd  11938  fsumxp  11968  fsumcnv  11969  fsummulc2  11980  fsumconst  11986  fsumabs  11997  telfsumo  11998  fsumparts  12002  fsumrelem  12003  fsumiun  12009  binomlem  12015  binom  12016  binom11  12018  isumsplit  12023  arisum  12030  arisum2  12031  trireciplem  12032  georeclim  12045  cvgratnnlemseq  12058  prodfrecap  12078  prod1dc  12118  fprodf1o  12120  fprodcl2lem  12137  fprodcllem  12138  fprodfac  12147  fprod2d  12155  fprodxp  12156  fprodcnv  12157  fprodrec  12161  fprodmodd  12173  ef0lem  12192  ege2le3  12203  efaddlem  12206  efcan  12208  eft0val  12225  ef4p  12226  efgt1p2  12227  efi4p  12249  sincossq  12280  cos2tsin  12283  absefi  12301  demoivreALT  12306  p1modz1  12326  dvdsabseq  12379  odd2np1lem  12404  oddp1even  12408  opoe  12427  m1expo  12432  m1exp1  12433  nn0o1gt2  12437  bitsinv1  12494  gcddvds  12505  gcdcl  12508  gcdeq0  12519  gcd0id  12521  bezoutr1  12575  nnmindc  12576  nnminle  12577  eucalg  12602  lcm0val  12608  lcmid  12623  rpmul  12641  dfphi2  12763  phiprmpw  12765  hashgcdeq  12783  odzdvds  12789  nnnn0modprm0  12799  pythagtriplem4  12812  pythagtriplem12  12819  pcaddlem  12883  pcmpt  12887  pockthi  12902  4sqlem12  12946  2expltfac  12983  ennnfonelem0  12997  ennnfonelem1  12999  ennnfonelemhdmp1  13001  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemf1  13010  ctiunctlemfo  13031  setsresg  13091  strressid  13125  strle1g  13160  restid2  13302  prdsbas3  13341  gsumwmhm  13552  grplactcnv  13656  mulg0  13683  mulgnn0gsum  13686  mulgneg  13698  mulgneg2  13714  gsumfzconst  13899  gsumfzsnfd  13903  gsumfzfsumlem0  14571  zrhval2  14604  mpl0fi  14687  tgval2  14746  tgidm  14769  epttop  14785  tgrest  14864  restco  14869  restsn  14875  tgcn  14903  cnptopresti  14933  cnptoprest  14934  txbas  14953  upxp  14967  txrest  14971  txdis  14972  txhmeo  15014  txswaphmeolem  15015  xblss2ps  15099  xblss2  15100  qtopbasss  15216  fsumcncntop  15262  hoverb  15343  limcimolemlt  15359  dvcnp2cntop  15394  dvcoapbr  15402  dvexp  15406  dvexp2  15407  dvmptid  15411  dveflem  15421  dvef  15422  plymullem1  15443  plyadd  15446  plymul  15447  plycoeid3  15452  plycjlemc  15455  plycj  15456  sin0pilem1  15476  sin2kpi  15506  cos2kpi  15507  coseq0q4123  15529  coseq0negpitopi  15531  sincosq1eq  15534  sinkpi  15542  coskpi  15543  1cxp  15595  mpodvdsmulf1o  15685  lgslem2  15701  lgsfcl2  15706  lgs0  15713  lgs2  15717  lgsneg  15724  lgsdilem  15727  lgsdir2lem4  15731  lgsdir2lem5  15732  lgsne0  15738  lgssq  15740  lgssq2  15741  gausslemma2dlem3  15763  gausslemma2dlem4  15764  lgseisenlem1  15770  lgsquadlem2  15778  lgsquad2lem2  15782  lgsquad3  15784  m1lgs  15785  2lgslem1a2  15787  2lgsoddprmlem3  15811  2sqlem9  15824  2sqlem10  15825  edgiedgbg  15886  isuhgrm  15892  isushgrm  15893  uhgr0vb  15905  uhgrun  15907  isupgren  15916  isumgren  15926  umgrnloop0  15938  upgrun  15945  umgrun  15947  isuspgren  15976  isusgren  15977  usgrf1oedg  16024  usgredg3  16033  vtxdg0v  16080  vtxdgfi0e  16081  vtxdfifiun  16083  vtxdumgrfival  16084  wlkl1loop  16130  2wlklem  16146  upgr2wlkdc  16147  clwwlkn0  16177  clwwlkn1  16186  clwwlkn2  16189  umgr2cwwk2dif  16192  ex-ceil  16199  bj-intexr  16380  peano3nninf  16487  nninfall  16489  isomninnlem  16512  iswomni0  16533  ismkvnnlem  16534  nconstwlpolem0  16545