Theorem eqtrdi 2280

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqtr2di  2281  eqtr4di  2282  3eqtr3g  2287  3eqtr4a  2290  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  csbprc  3540  un00  3541  disjssun  3558  disjpr2  3733  tppreq3  3774  diftpsn3  3814  ssprsseq  3835  preq12b  3853  intsng  3962  uniintsnr  3964  rint0  3967  riin0  4042  iununir  4054  intexr  4240  exmid1stab  4298  sucprc  4509  op1stbg  4576  elreldm  4958  xpeq0r  5159  xpdisj1  5161  xpdisj2  5162  resdisj  5165  xpima1  5183  xpima2m  5184  elxp4  5224  unixp0im  5273  uniabio  5297  iotass  5304  cnvresid  5404  funimacnv  5406  fimadmfo  5568  f1o00  5620  dffv4g  5636  fv2prc  5678  fnrnfv  5692  feqresmpt  5700  dffn5imf  5701  funfvdm2f  5711  fvun1  5712  fvmpt2  5730  fndmin  5754  fmptcof  5814  fmptcos  5815  funopdmsn  5834  fvunsng  5848  fvpr1  5858  fnrnov  6168  offval  6243  ofrfval  6244  op1std  6311  op2ndd  6312  fmpoco  6381  tpostpos  6430  tfr0  6489  rdgival  6548  frec0g  6563  2oconcl  6607  om0  6626  oei0  6627  oasuc  6632  omv2  6633  nnm0r  6647  uniqs2  6764  en1  6973  en1bg  6974  fundmen  6981  mapsnen  6986  en2  6998  xpsnen  7005  xpcomco  7010  xpdom2  7015  xpmapenlem  7035  exmidpweq  7101  unsnfidcex  7112  fiintim  7123  ssfirab  7129  sbthlemi8  7163  elfi2  7171  fi0  7174  fieq0  7175  djudom  7292  ismkvnex  7354  nninfwlpoimlemg  7374  en2other2  7407  exmidfodomrlemim  7412  nq0m0r  7676  addpinq1  7684  genipv  7729  genpelvl  7732  genpelvu  7733  cauappcvgprlem1  7879  caucvgsrlemoffres  8020  addresr  8057  mulresr  8058  axcnre  8101  add20  8654  rimul  8765  rereim  8766  mulreim  8784  sup3exmid  9137  fv0p1e1  9258  div4p1lem1div2  9398  nnm1nn0  9443  znegcl  9510  peano2z  9515  nneoor  9582  nn0ind-raph  9597  xnegneg  10068  xltnegi  10070  xaddpnf1  10081  xnegid  10094  xnn0xadd0  10102  xnegdi  10103  xsubge0  10116  xposdif  10117  xlesubadd  10118  xleaddadd  10122  fz0to4untppr  10359  fzo0to2pr  10464  nninfdcex  10498  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  mulp1mod1  10628  frecfzennn  10689  iseqf1olemqk  10770  exp0  10806  expp1  10809  expnegap0  10810  1exp  10831  mulexp  10841  m1expeven  10849  sq0i  10894  bernneq  10923  facp1  10993  faclbnd3  11006  facubnd  11008  bcval5  11026  hashinfom  11041  hashsng  11061  hashxp  11091  resunimafz0  11096  zfz1iso  11106  hash2en  11108  hashtpgim  11110  lsw1  11167  s1rn  11199  eqs1  11209  ccat1st1st  11222  swrd00g  11234  swrdlend  11243  swrds1  11253  cats1lend  11352  cats2catd  11354  s2leng  11374  s2dmg  11375  imre  11416  reim0b  11427  rereb  11428  resqrexlemover  11575  resqrexlemcalc1  11579  abs00bd  11631  maxabslemlub  11772  xrmaxiflemcom  11814  xrmaxadd  11826  climconst  11855  fzf1o  11941  isumz  11955  fsumf1o  11956  fsumcllem  11965  fsumadd  11972  fsumxp  12002  fsumcnv  12003  fsummulc2  12014  fsumconst  12020  fsumabs  12031  telfsumo  12032  fsumparts  12036  fsumrelem  12037  fsumiun  12043  binomlem  12049  binom  12050  binom11  12052  isumsplit  12057  arisum  12064  arisum2  12065  trireciplem  12066  georeclim  12079  cvgratnnlemseq  12092  prodfrecap  12112  prod1dc  12152  fprodf1o  12154  fprodcl2lem  12171  fprodcllem  12172  fprodfac  12181  fprod2d  12189  fprodxp  12190  fprodcnv  12191  fprodrec  12195  fprodmodd  12207  ef0lem  12226  ege2le3  12237  efaddlem  12240  efcan  12242  eft0val  12259  ef4p  12260  efgt1p2  12261  efi4p  12283  sincossq  12314  cos2tsin  12317  absefi  12335  demoivreALT  12340  p1modz1  12360  dvdsabseq  12413  odd2np1lem  12438  oddp1even  12442  opoe  12461  m1expo  12466  m1exp1  12467  nn0o1gt2  12471  bitsinv1  12528  gcddvds  12539  gcdcl  12542  gcdeq0  12553  gcd0id  12555  bezoutr1  12609  nnmindc  12610  nnminle  12611  eucalg  12636  lcm0val  12642  lcmid  12657  rpmul  12675  dfphi2  12797  phiprmpw  12799  hashgcdeq  12817  odzdvds  12823  nnnn0modprm0  12833  pythagtriplem4  12846  pythagtriplem12  12853  pcaddlem  12917  pcmpt  12921  pockthi  12936  4sqlem12  12980  2expltfac  13017  ennnfonelem0  13031  ennnfonelem1  13033  ennnfonelemhdmp1  13035  ennnfonelemkh  13038  ennnfonelemhf1o  13039  ennnfonelemf1  13044  ctiunctlemfo  13065  setsresg  13125  strressid  13159  strle1g  13194  restid2  13336  prdsbas3  13375  gsumwmhm  13586  grplactcnv  13690  mulg0  13717  mulgnn0gsum  13720  mulgneg  13732  mulgneg2  13748  gsumfzconst  13933  gsumfzsnfd  13937  gsumsplit0  13938  gsumfzfsumlem0  14606  zrhval2  14639  mpl0fi  14722  tgval2  14781  tgidm  14804  epttop  14820  tgrest  14899  restco  14904  restsn  14910  tgcn  14938  cnptopresti  14968  cnptoprest  14969  txbas  14988  upxp  15002  txrest  15006  txdis  15007  txhmeo  15049  txswaphmeolem  15050  xblss2ps  15134  xblss2  15135  qtopbasss  15251  fsumcncntop  15297  hoverb  15378  limcimolemlt  15394  dvcnp2cntop  15429  dvcoapbr  15437  dvexp  15441  dvexp2  15442  dvmptid  15446  dveflem  15456  dvef  15457  plymullem1  15478  plyadd  15481  plymul  15482  plycoeid3  15487  plycjlemc  15490  plycj  15491  sin0pilem1  15511  sin2kpi  15541  cos2kpi  15542  coseq0q4123  15564  coseq0negpitopi  15566  sincosq1eq  15569  sinkpi  15577  coskpi  15578  1cxp  15630  mpodvdsmulf1o  15720  lgslem2  15736  lgsfcl2  15741  lgs0  15748  lgs2  15752  lgsneg  15759  lgsdilem  15762  lgsdir2lem4  15766  lgsdir2lem5  15767  lgsne0  15773  lgssq  15775  lgssq2  15776  gausslemma2dlem3  15798  gausslemma2dlem4  15799  lgseisenlem1  15805  lgsquadlem2  15813  lgsquad2lem2  15817  lgsquad3  15819  m1lgs  15820  2lgslem1a2  15822  2lgsoddprmlem3  15846  2sqlem9  15859  2sqlem10  15860  edgiedgbg  15922  isuhgrm  15928  isushgrm  15929  uhgr0vb  15941  uhgrun  15943  isupgren  15952  isumgren  15962  umgrnloop0  15974  upgrun  15983  umgrun  15985  isuspgren  16014  isusgren  16015  usgrf1oedg  16062  usgredg3  16071  egrsubgr  16120  0uhgrsubgr  16122  uhgrspansubgrlem  16133  vtxdg0v  16151  vtxdgfi0e  16152  vtxdfifiun  16154  vtxdumgrfival  16155  1loopgrvd2fi  16162  vdegp1cid  16173  wlkl1loop  16215  2wlklem  16233  upgr2wlkdc  16234  clwwlkn0  16265  clwwlkn1  16275  clwwlkn2  16278  umgr2cwwk2dif  16281  clwwlk0on0  16288  clwwlknonel  16289  clwwlknonex2lem1  16294  trlsegvdeglem4  16320  eupthvdres  16332  eupth2lembfi  16334  ex-ceil  16344  bj-intexr  16529  peano3nninf  16635  nninfall  16637  isomninnlem  16660  iswomni0  16682  ismkvnnlem  16683  nconstwlpolem0  16694  gfsumval  16707  gfsumsn  16712  gfsump1  16713