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  3808  ssprsseq  3829  preq12b  3847  intsng  3956  uniintsnr  3958  rint0  3961  riin0  4036  iununir  4048  intexr  4233  exmid1stab  4291  sucprc  4502  op1stbg  4569  elreldm  4949  xpeq0r  5150  xpdisj1  5152  xpdisj2  5153  resdisj  5156  xpima1  5174  xpima2m  5175  elxp4  5215  unixp0im  5264  uniabio  5288  iotass  5295  cnvresid  5394  funimacnv  5396  fimadmfo  5556  f1o00  5607  dffv4g  5623  fv2prc  5665  fnrnfv  5679  feqresmpt  5687  dffn5imf  5688  funfvdm2f  5698  fvun1  5699  fvmpt2  5717  fndmin  5741  fmptcof  5801  fmptcos  5802  funopdmsn  5818  fvunsng  5832  fvpr1  5842  fnrnov  6150  offval  6224  ofrfval  6225  op1std  6292  op2ndd  6293  fmpoco  6360  tpostpos  6408  tfr0  6467  rdgival  6526  frec0g  6541  2oconcl  6583  om0  6602  oei0  6603  oasuc  6608  omv2  6609  nnm0r  6623  uniqs2  6740  en1  6949  en1bg  6950  fundmen  6957  mapsnen  6962  en2  6971  xpsnen  6976  xpcomco  6981  xpdom2  6986  xpmapenlem  7006  exmidpweq  7067  unsnfidcex  7078  fiintim  7089  ssfirab  7094  sbthlemi8  7127  elfi2  7135  fi0  7138  fieq0  7139  djudom  7256  ismkvnex  7318  nninfwlpoimlemg  7338  en2other2  7370  exmidfodomrlemim  7375  nq0m0r  7639  addpinq1  7647  genipv  7692  genpelvl  7695  genpelvu  7696  cauappcvgprlem1  7842  caucvgsrlemoffres  7983  addresr  8020  mulresr  8021  axcnre  8064  add20  8617  rimul  8728  rereim  8729  mulreim  8747  sup3exmid  9100  fv0p1e1  9221  div4p1lem1div2  9361  nnm1nn0  9406  znegcl  9473  peano2z  9478  nneoor  9545  nn0ind-raph  9560  xnegneg  10025  xltnegi  10027  xaddpnf1  10038  xnegid  10051  xnn0xadd0  10059  xnegdi  10060  xsubge0  10073  xposdif  10074  xlesubadd  10075  xleaddadd  10079  fz0to4untppr  10316  fzo0to2pr  10419  nninfdcex  10452  fldiv4p1lem1div2  10520  fldiv4lem1div2  10522  mulp1mod1  10582  frecfzennn  10643  iseqf1olemqk  10724  exp0  10760  expp1  10763  expnegap0  10764  1exp  10785  mulexp  10795  m1expeven  10803  sq0i  10848  bernneq  10877  facp1  10947  faclbnd3  10960  facubnd  10962  bcval5  10980  hashinfom  10995  hashsng  11015  hashxp  11043  resunimafz0  11048  zfz1iso  11058  hash2en  11060  lsw1  11116  s1rn  11146  eqs1  11156  ccat1st1st  11167  swrd00g  11176  swrdlend  11185  swrds1  11195  cats1lend  11294  cats2catd  11296  s2leng  11316  s2dmg  11317  imre  11357  reim0b  11368  rereb  11369  resqrexlemover  11516  resqrexlemcalc1  11520  abs00bd  11572  maxabslemlub  11713  xrmaxiflemcom  11755  xrmaxadd  11767  climconst  11796  isumz  11895  fsumf1o  11896  fsumcllem  11905  fsumadd  11912  fsumxp  11942  fsumcnv  11943  fsummulc2  11954  fsumconst  11960  fsumabs  11971  telfsumo  11972  fsumparts  11976  fsumrelem  11977  fsumiun  11983  binomlem  11989  binom  11990  binom11  11992  isumsplit  11997  arisum  12004  arisum2  12005  trireciplem  12006  georeclim  12019  cvgratnnlemseq  12032  prodfrecap  12052  prod1dc  12092  fprodf1o  12094  fprodcl2lem  12111  fprodcllem  12112  fprodfac  12121  fprod2d  12129  fprodxp  12130  fprodcnv  12131  fprodrec  12135  fprodmodd  12147  ef0lem  12166  ege2le3  12177  efaddlem  12180  efcan  12182  eft0val  12199  ef4p  12200  efgt1p2  12201  efi4p  12223  sincossq  12254  cos2tsin  12257  absefi  12275  demoivreALT  12280  p1modz1  12300  dvdsabseq  12353  odd2np1lem  12378  oddp1even  12382  opoe  12401  m1expo  12406  m1exp1  12407  nn0o1gt2  12411  bitsinv1  12468  gcddvds  12479  gcdcl  12482  gcdeq0  12493  gcd0id  12495  bezoutr1  12549  nnmindc  12550  nnminle  12551  eucalg  12576  lcm0val  12582  lcmid  12597  rpmul  12615  dfphi2  12737  phiprmpw  12739  hashgcdeq  12757  odzdvds  12763  nnnn0modprm0  12773  pythagtriplem4  12786  pythagtriplem12  12793  pcaddlem  12857  pcmpt  12861  pockthi  12876  4sqlem12  12920  2expltfac  12957  ennnfonelem0  12971  ennnfonelem1  12973  ennnfonelemhdmp1  12975  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemf1  12984  ctiunctlemfo  13005  setsresg  13065  strressid  13099  strle1g  13134  restid2  13276  prdsbas3  13315  gsumwmhm  13526  grplactcnv  13630  mulg0  13657  mulgnn0gsum  13660  mulgneg  13672  mulgneg2  13688  gsumfzconst  13873  gsumfzsnfd  13877  gsumfzfsumlem0  14544  zrhval2  14577  mpl0fi  14660  tgval2  14719  tgidm  14742  epttop  14758  tgrest  14837  restco  14842  restsn  14848  tgcn  14876  cnptopresti  14906  cnptoprest  14907  txbas  14926  upxp  14940  txrest  14944  txdis  14945  txhmeo  14987  txswaphmeolem  14988  xblss2ps  15072  xblss2  15073  qtopbasss  15189  fsumcncntop  15235  hoverb  15316  limcimolemlt  15332  dvcnp2cntop  15367  dvcoapbr  15375  dvexp  15379  dvexp2  15380  dvmptid  15384  dveflem  15394  dvef  15395  plymullem1  15416  plyadd  15419  plymul  15420  plycoeid3  15425  plycjlemc  15428  plycj  15429  sin0pilem1  15449  sin2kpi  15479  cos2kpi  15480  coseq0q4123  15502  coseq0negpitopi  15504  sincosq1eq  15507  sinkpi  15515  coskpi  15516  1cxp  15568  mpodvdsmulf1o  15658  lgslem2  15674  lgsfcl2  15679  lgs0  15686  lgs2  15690  lgsneg  15697  lgsdilem  15700  lgsdir2lem4  15704  lgsdir2lem5  15705  lgsne0  15711  lgssq  15713  lgssq2  15714  gausslemma2dlem3  15736  gausslemma2dlem4  15737  lgseisenlem1  15743  lgsquadlem2  15751  lgsquad2lem2  15755  lgsquad3  15757  m1lgs  15758  2lgslem1a2  15760  2lgsoddprmlem3  15784  2sqlem9  15797  2sqlem10  15798  edgiedgbg  15859  isuhgrm  15865  isushgrm  15866  uhgr0vb  15878  uhgrun  15880  isupgren  15889  isumgren  15899  umgrnloop0  15911  upgrun  15918  umgrun  15920  isuspgren  15949  isusgren  15950  usgrf1oedg  15997  usgredg3  16006  ex-ceil  16048  bj-intexr  16229  peano3nninf  16332  nninfall  16334  isomninnlem  16357  iswomni0  16378  ismkvnnlem  16379  nconstwlpolem0  16390