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  4234  exmid1stab  4292  sucprc  4503  op1stbg  4570  elreldm  4950  xpeq0r  5151  xpdisj1  5153  xpdisj2  5154  resdisj  5157  xpima1  5175  xpima2m  5176  elxp4  5216  unixp0im  5265  uniabio  5289  iotass  5296  cnvresid  5395  funimacnv  5397  fimadmfo  5559  f1o00  5610  dffv4g  5626  fv2prc  5668  fnrnfv  5682  feqresmpt  5690  dffn5imf  5691  funfvdm2f  5701  fvun1  5702  fvmpt2  5720  fndmin  5744  fmptcof  5804  fmptcos  5805  funopdmsn  5823  fvunsng  5837  fvpr1  5847  fnrnov  6157  offval  6232  ofrfval  6233  op1std  6300  op2ndd  6301  fmpoco  6368  tpostpos  6416  tfr0  6475  rdgival  6534  frec0g  6549  2oconcl  6593  om0  6612  oei0  6613  oasuc  6618  omv2  6619  nnm0r  6633  uniqs2  6750  en1  6959  en1bg  6960  fundmen  6967  mapsnen  6972  en2  6981  xpsnen  6988  xpcomco  6993  xpdom2  6998  xpmapenlem  7018  exmidpweq  7082  unsnfidcex  7093  fiintim  7104  ssfirab  7109  sbthlemi8  7142  elfi2  7150  fi0  7153  fieq0  7154  djudom  7271  ismkvnex  7333  nninfwlpoimlemg  7353  en2other2  7385  exmidfodomrlemim  7390  nq0m0r  7654  addpinq1  7662  genipv  7707  genpelvl  7710  genpelvu  7711  cauappcvgprlem1  7857  caucvgsrlemoffres  7998  addresr  8035  mulresr  8036  axcnre  8079  add20  8632  rimul  8743  rereim  8744  mulreim  8762  sup3exmid  9115  fv0p1e1  9236  div4p1lem1div2  9376  nnm1nn0  9421  znegcl  9488  peano2z  9493  nneoor  9560  nn0ind-raph  9575  xnegneg  10041  xltnegi  10043  xaddpnf1  10054  xnegid  10067  xnn0xadd0  10075  xnegdi  10076  xsubge0  10089  xposdif  10090  xlesubadd  10091  xleaddadd  10095  fz0to4untppr  10332  fzo0to2pr  10436  nninfdcex  10469  fldiv4p1lem1div2  10537  fldiv4lem1div2  10539  mulp1mod1  10599  frecfzennn  10660  iseqf1olemqk  10741  exp0  10777  expp1  10780  expnegap0  10781  1exp  10802  mulexp  10812  m1expeven  10820  sq0i  10865  bernneq  10894  facp1  10964  faclbnd3  10977  facubnd  10979  bcval5  10997  hashinfom  11012  hashsng  11032  hashxp  11061  resunimafz0  11066  zfz1iso  11076  hash2en  11078  lsw1  11134  s1rn  11166  eqs1  11176  ccat1st1st  11187  swrd00g  11196  swrdlend  11205  swrds1  11215  cats1lend  11314  cats2catd  11316  s2leng  11336  s2dmg  11337  imre  11377  reim0b  11388  rereb  11389  resqrexlemover  11536  resqrexlemcalc1  11540  abs00bd  11592  maxabslemlub  11733  xrmaxiflemcom  11775  xrmaxadd  11787  climconst  11816  isumz  11915  fsumf1o  11916  fsumcllem  11925  fsumadd  11932  fsumxp  11962  fsumcnv  11963  fsummulc2  11974  fsumconst  11980  fsumabs  11991  telfsumo  11992  fsumparts  11996  fsumrelem  11997  fsumiun  12003  binomlem  12009  binom  12010  binom11  12012  isumsplit  12017  arisum  12024  arisum2  12025  trireciplem  12026  georeclim  12039  cvgratnnlemseq  12052  prodfrecap  12072  prod1dc  12112  fprodf1o  12114  fprodcl2lem  12131  fprodcllem  12132  fprodfac  12141  fprod2d  12149  fprodxp  12150  fprodcnv  12151  fprodrec  12155  fprodmodd  12167  ef0lem  12186  ege2le3  12197  efaddlem  12200  efcan  12202  eft0val  12219  ef4p  12220  efgt1p2  12221  efi4p  12243  sincossq  12274  cos2tsin  12277  absefi  12295  demoivreALT  12300  p1modz1  12320  dvdsabseq  12373  odd2np1lem  12398  oddp1even  12402  opoe  12421  m1expo  12426  m1exp1  12427  nn0o1gt2  12431  bitsinv1  12488  gcddvds  12499  gcdcl  12502  gcdeq0  12513  gcd0id  12515  bezoutr1  12569  nnmindc  12570  nnminle  12571  eucalg  12596  lcm0val  12602  lcmid  12617  rpmul  12635  dfphi2  12757  phiprmpw  12759  hashgcdeq  12777  odzdvds  12783  nnnn0modprm0  12793  pythagtriplem4  12806  pythagtriplem12  12813  pcaddlem  12877  pcmpt  12881  pockthi  12896  4sqlem12  12940  2expltfac  12977  ennnfonelem0  12991  ennnfonelem1  12993  ennnfonelemhdmp1  12995  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemf1  13004  ctiunctlemfo  13025  setsresg  13085  strressid  13119  strle1g  13154  restid2  13296  prdsbas3  13335  gsumwmhm  13546  grplactcnv  13650  mulg0  13677  mulgnn0gsum  13680  mulgneg  13692  mulgneg2  13708  gsumfzconst  13893  gsumfzsnfd  13897  gsumfzfsumlem0  14565  zrhval2  14598  mpl0fi  14681  tgval2  14740  tgidm  14763  epttop  14779  tgrest  14858  restco  14863  restsn  14869  tgcn  14897  cnptopresti  14927  cnptoprest  14928  txbas  14947  upxp  14961  txrest  14965  txdis  14966  txhmeo  15008  txswaphmeolem  15009  xblss2ps  15093  xblss2  15094  qtopbasss  15210  fsumcncntop  15256  hoverb  15337  limcimolemlt  15353  dvcnp2cntop  15388  dvcoapbr  15396  dvexp  15400  dvexp2  15401  dvmptid  15405  dveflem  15415  dvef  15416  plymullem1  15437  plyadd  15440  plymul  15441  plycoeid3  15446  plycjlemc  15449  plycj  15450  sin0pilem1  15470  sin2kpi  15500  cos2kpi  15501  coseq0q4123  15523  coseq0negpitopi  15525  sincosq1eq  15528  sinkpi  15536  coskpi  15537  1cxp  15589  mpodvdsmulf1o  15679  lgslem2  15695  lgsfcl2  15700  lgs0  15707  lgs2  15711  lgsneg  15718  lgsdilem  15721  lgsdir2lem4  15725  lgsdir2lem5  15726  lgsne0  15732  lgssq  15734  lgssq2  15735  gausslemma2dlem3  15757  gausslemma2dlem4  15758  lgseisenlem1  15764  lgsquadlem2  15772  lgsquad2lem2  15776  lgsquad3  15778  m1lgs  15779  2lgslem1a2  15781  2lgsoddprmlem3  15805  2sqlem9  15818  2sqlem10  15819  edgiedgbg  15880  isuhgrm  15886  isushgrm  15887  uhgr0vb  15899  uhgrun  15901  isupgren  15910  isumgren  15920  umgrnloop0  15932  upgrun  15939  umgrun  15941  isuspgren  15970  isusgren  15971  usgrf1oedg  16018  usgredg3  16027  vtxdg0v  16053  vtxdgfi0e  16054  vtxdfifiun  16056  vtxdumgrfival  16057  wlkl1loop  16099  2wlklem  16115  upgr2wlkdc  16116  ex-ceil  16145  bj-intexr  16326  peano3nninf  16433  nninfall  16435  isomninnlem  16458  iswomni0  16479  ismkvnnlem  16480  nconstwlpolem0  16491