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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  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  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  csbprc  3542  un00  3543  disjssun  3560  disjpr2  3737  tppreq3  3778  diftpsn3  3819  ssprsseq  3840  preq12b  3858  intsng  3967  uniintsnr  3969  rint0  3972  riin0  4047  iununir  4059  intexr  4245  exmid1stab  4304  sucprc  4515  op1stbg  4582  elreldm  4964  xpeq0r  5166  xpdisj1  5168  xpdisj2  5169  resdisj  5172  xpima1  5190  xpima2m  5191  elxp4  5231  unixp0im  5280  uniabio  5304  iotass  5311  cnvresid  5411  funimacnv  5413  fimadmfo  5577  f1o00  5629  dffv4g  5645  fv2prc  5687  fnrnfv  5701  feqresmpt  5709  dffn5imf  5710  funfvdm2f  5720  fvun1  5721  fvmpt2  5739  fndmin  5763  fmptcof  5822  fmptcos  5823  funopdmsn  5842  fvunsng  5856  fvpr1  5866  fnrnov  6178  offval  6252  ofrfval  6253  op1std  6320  op2ndd  6321  fmpoco  6390  suppsnopdc  6428  mptsuppdifd  6433  supp0cosupp0fn  6445  tpostpos  6473  tfr0  6532  rdgival  6591  frec0g  6606  2oconcl  6650  om0  6669  oei0  6670  oasuc  6675  omv2  6676  nnm0r  6690  uniqs2  6807  en1  7016  en1bg  7017  fundmen  7024  mapsnen  7029  en2  7041  xpsnen  7048  xpcomco  7053  xpdom2  7058  xpmapenlem  7078  exmidpweq  7144  unsnfidcex  7155  fiintim  7166  ssfirab  7172  sbthlemi8  7206  elfi2  7214  fi0  7217  fieq0  7218  djudom  7335  ismkvnex  7397  nninfwlpoimlemg  7417  en2other2  7450  exmidfodomrlemim  7455  nq0m0r  7719  addpinq1  7727  genipv  7772  genpelvl  7775  genpelvu  7776  cauappcvgprlem1  7922  caucvgsrlemoffres  8063  addresr  8100  mulresr  8101  axcnre  8144  add20  8696  rimul  8807  rereim  8808  mulreim  8826  sup3exmid  9179  fv0p1e1  9300  div4p1lem1div2  9440  nnm1nn0  9485  znegcl  9554  peano2z  9559  nneoor  9626  nn0ind-raph  9641  xnegneg  10112  xltnegi  10114  xaddpnf1  10125  xnegid  10138  xnn0xadd0  10146  xnegdi  10147  xsubge0  10160  xposdif  10161  xlesubadd  10162  xleaddadd  10166  fz0to4untppr  10404  fzo0to2pr  10509  nninfdcex  10543  fldiv4p1lem1div2  10611  fldiv4lem1div2  10613  mulp1mod1  10673  frecfzennn  10734  iseqf1olemqk  10815  exp0  10851  expp1  10854  expnegap0  10855  1exp  10876  mulexp  10886  m1expeven  10894  sq0i  10939  bernneq  10968  facp1  11038  faclbnd3  11051  facubnd  11053  bcval5  11071  hashinfom  11086  hashsng  11106  hashxp  11136  resunimafz0  11141  zfz1iso  11151  hash2en  11153  hashtpgim  11155  lsw1  11212  s1rn  11244  eqs1  11254  ccat1st1st  11267  swrd00g  11279  swrdlend  11288  swrds1  11298  cats1lend  11397  cats2catd  11399  s2leng  11419  s2dmg  11420  imre  11474  reim0b  11485  rereb  11486  resqrexlemover  11633  resqrexlemcalc1  11637  abs00bd  11689  maxabslemlub  11830  xrmaxiflemcom  11872  xrmaxadd  11884  climconst  11913  fzf1o  11999  isumz  12013  fsumf1o  12014  fsumcllem  12023  fsumadd  12030  fsumxp  12060  fsumcnv  12061  fsummulc2  12072  fsumconst  12078  fsumabs  12089  telfsumo  12090  fsumparts  12094  fsumrelem  12095  fsumiun  12101  binomlem  12107  binom  12108  binom11  12110  isumsplit  12115  arisum  12122  arisum2  12123  trireciplem  12124  georeclim  12137  cvgratnnlemseq  12150  prodfrecap  12170  prod1dc  12210  fprodf1o  12212  fprodcl2lem  12229  fprodcllem  12230  fprodfac  12239  fprod2d  12247  fprodxp  12248  fprodcnv  12249  fprodrec  12253  fprodmodd  12265  ef0lem  12284  ege2le3  12295  efaddlem  12298  efcan  12300  eft0val  12317  ef4p  12318  efgt1p2  12319  efi4p  12341  sincossq  12372  cos2tsin  12375  absefi  12393  demoivreALT  12398  p1modz1  12418  dvdsabseq  12471  odd2np1lem  12496  oddp1even  12500  opoe  12519  m1expo  12524  m1exp1  12525  nn0o1gt2  12529  bitsinv1  12586  gcddvds  12597  gcdcl  12600  gcdeq0  12611  gcd0id  12613  bezoutr1  12667  nnmindc  12668  nnminle  12669  eucalg  12694  lcm0val  12700  lcmid  12715  rpmul  12733  dfphi2  12855  phiprmpw  12857  hashgcdeq  12875  odzdvds  12881  nnnn0modprm0  12891  pythagtriplem4  12904  pythagtriplem12  12911  pcaddlem  12975  pcmpt  12979  pockthi  12994  4sqlem12  13038  2expltfac  13075  ennnfonelem0  13089  ennnfonelem1  13091  ennnfonelemhdmp1  13093  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemf1  13102  ctiunctlemfo  13123  setsresg  13183  strressid  13217  strle1g  13252  restid2  13394  prdsbas3  13433  gsumwmhm  13644  grplactcnv  13748  mulg0  13775  mulgnn0gsum  13778  mulgneg  13790  mulgneg2  13806  gsumfzconst  13991  gsumfzsnfd  13995  gsumsplit0  13996  gsumfzfsumlem0  14665  zrhval2  14698  mpl0fi  14786  tgval2  14845  tgidm  14868  epttop  14884  tgrest  14963  restco  14968  restsn  14974  tgcn  15002  cnptopresti  15032  cnptoprest  15033  txbas  15052  upxp  15066  txrest  15070  txdis  15071  txhmeo  15113  txswaphmeolem  15114  xblss2ps  15198  xblss2  15199  qtopbasss  15315  fsumcncntop  15361  hoverb  15442  limcimolemlt  15458  dvcnp2cntop  15493  dvcoapbr  15501  dvexp  15505  dvexp2  15506  dvmptid  15510  dveflem  15520  dvef  15521  plymullem1  15542  plyadd  15545  plymul  15546  plycoeid3  15551  plycjlemc  15554  plycj  15555  sin0pilem1  15575  sin2kpi  15605  cos2kpi  15606  coseq0q4123  15628  coseq0negpitopi  15630  sincosq1eq  15633  sinkpi  15641  coskpi  15642  1cxp  15694  mpodvdsmulf1o  15787  lgslem2  15803  lgsfcl2  15808  lgs0  15815  lgs2  15819  lgsneg  15826  lgsdilem  15829  lgsdir2lem4  15833  lgsdir2lem5  15834  lgsne0  15840  lgssq  15842  lgssq2  15843  gausslemma2dlem3  15865  gausslemma2dlem4  15866  lgseisenlem1  15872  lgsquadlem2  15880  lgsquad2lem2  15884  lgsquad3  15886  m1lgs  15887  2lgslem1a2  15889  2lgsoddprmlem3  15913  2sqlem9  15926  2sqlem10  15927  edgiedgbg  15989  isuhgrm  15995  isushgrm  15996  uhgr0vb  16008  uhgrun  16010  isupgren  16019  isumgren  16029  umgrnloop0  16041  upgrun  16050  umgrun  16052  isuspgren  16081  isusgren  16082  usgrf1oedg  16129  usgredg3  16138  egrsubgr  16187  0uhgrsubgr  16189  uhgrspansubgrlem  16200  vtxdg0v  16218  vtxdgfi0e  16219  vtxdfifiun  16221  vtxdumgrfival  16222  1loopgrvd2fi  16229  vdegp1cid  16240  wlkl1loop  16282  2wlklem  16300  upgr2wlkdc  16301  clwwlkn0  16332  clwwlkn1  16342  clwwlkn2  16345  umgr2cwwk2dif  16348  clwwlk0on0  16355  clwwlknonel  16356  clwwlknonex2lem1  16361  trlsegvdeglem4  16387  eupthvdres  16399  eupth2lembfi  16401  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  ex-ceil  16423  bj-intexr  16607  peano3nninf  16716  nninfall  16718  isomninnlem  16745  iswomni0  16767  ismkvnnlem  16768  nconstwlpolem0  16779  gfsumval  16792  gfsumsn  16797  gfsump1  16798