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  5833  fvunsng  5847  fvpr1  5857  fnrnov  6167  offval  6242  ofrfval  6243  op1std  6310  op2ndd  6311  fmpoco  6380  tpostpos  6429  tfr0  6488  rdgival  6547  frec0g  6562  2oconcl  6606  om0  6625  oei0  6626  oasuc  6631  omv2  6632  nnm0r  6646  uniqs2  6763  en1  6972  en1bg  6973  fundmen  6980  mapsnen  6985  en2  6997  xpsnen  7004  xpcomco  7009  xpdom2  7014  xpmapenlem  7034  exmidpweq  7100  unsnfidcex  7111  fiintim  7122  ssfirab  7128  sbthlemi8  7162  elfi2  7170  fi0  7173  fieq0  7174  djudom  7291  ismkvnex  7353  nninfwlpoimlemg  7373  en2other2  7406  exmidfodomrlemim  7411  nq0m0r  7675  addpinq1  7683  genipv  7728  genpelvl  7731  genpelvu  7732  cauappcvgprlem1  7878  caucvgsrlemoffres  8019  addresr  8056  mulresr  8057  axcnre  8100  add20  8653  rimul  8764  rereim  8765  mulreim  8783  sup3exmid  9136  fv0p1e1  9257  div4p1lem1div2  9397  nnm1nn0  9442  znegcl  9509  peano2z  9514  nneoor  9581  nn0ind-raph  9596  xnegneg  10067  xltnegi  10069  xaddpnf1  10080  xnegid  10093  xnn0xadd0  10101  xnegdi  10102  xsubge0  10115  xposdif  10116  xlesubadd  10117  xleaddadd  10121  fz0to4untppr  10358  fzo0to2pr  10462  nninfdcex  10496  fldiv4p1lem1div2  10564  fldiv4lem1div2  10566  mulp1mod1  10626  frecfzennn  10687  iseqf1olemqk  10768  exp0  10804  expp1  10807  expnegap0  10808  1exp  10829  mulexp  10839  m1expeven  10847  sq0i  10892  bernneq  10921  facp1  10991  faclbnd3  11004  facubnd  11006  bcval5  11024  hashinfom  11039  hashsng  11059  hashxp  11089  resunimafz0  11094  zfz1iso  11104  hash2en  11106  lsw1  11162  s1rn  11194  eqs1  11204  ccat1st1st  11217  swrd00g  11229  swrdlend  11238  swrds1  11248  cats1lend  11347  cats2catd  11349  s2leng  11369  s2dmg  11370  imre  11411  reim0b  11422  rereb  11423  resqrexlemover  11570  resqrexlemcalc1  11574  abs00bd  11626  maxabslemlub  11767  xrmaxiflemcom  11809  xrmaxadd  11821  climconst  11850  isumz  11949  fsumf1o  11950  fsumcllem  11959  fsumadd  11966  fsumxp  11996  fsumcnv  11997  fsummulc2  12008  fsumconst  12014  fsumabs  12025  telfsumo  12026  fsumparts  12030  fsumrelem  12031  fsumiun  12037  binomlem  12043  binom  12044  binom11  12046  isumsplit  12051  arisum  12058  arisum2  12059  trireciplem  12060  georeclim  12073  cvgratnnlemseq  12086  prodfrecap  12106  prod1dc  12146  fprodf1o  12148  fprodcl2lem  12165  fprodcllem  12166  fprodfac  12175  fprod2d  12183  fprodxp  12184  fprodcnv  12185  fprodrec  12189  fprodmodd  12201  ef0lem  12220  ege2le3  12231  efaddlem  12234  efcan  12236  eft0val  12253  ef4p  12254  efgt1p2  12255  efi4p  12277  sincossq  12308  cos2tsin  12311  absefi  12329  demoivreALT  12334  p1modz1  12354  dvdsabseq  12407  odd2np1lem  12432  oddp1even  12436  opoe  12455  m1expo  12460  m1exp1  12461  nn0o1gt2  12465  bitsinv1  12522  gcddvds  12533  gcdcl  12536  gcdeq0  12547  gcd0id  12549  bezoutr1  12603  nnmindc  12604  nnminle  12605  eucalg  12630  lcm0val  12636  lcmid  12651  rpmul  12669  dfphi2  12791  phiprmpw  12793  hashgcdeq  12811  odzdvds  12817  nnnn0modprm0  12827  pythagtriplem4  12840  pythagtriplem12  12847  pcaddlem  12911  pcmpt  12915  pockthi  12930  4sqlem12  12974  2expltfac  13011  ennnfonelem0  13025  ennnfonelem1  13027  ennnfonelemhdmp1  13029  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemf1  13038  ctiunctlemfo  13059  setsresg  13119  strressid  13153  strle1g  13188  restid2  13330  prdsbas3  13369  gsumwmhm  13580  grplactcnv  13684  mulg0  13711  mulgnn0gsum  13714  mulgneg  13726  mulgneg2  13742  gsumfzconst  13927  gsumfzsnfd  13931  gsumfzfsumlem0  14599  zrhval2  14632  mpl0fi  14715  tgval2  14774  tgidm  14797  epttop  14813  tgrest  14892  restco  14897  restsn  14903  tgcn  14931  cnptopresti  14961  cnptoprest  14962  txbas  14981  upxp  14995  txrest  14999  txdis  15000  txhmeo  15042  txswaphmeolem  15043  xblss2ps  15127  xblss2  15128  qtopbasss  15244  fsumcncntop  15290  hoverb  15371  limcimolemlt  15387  dvcnp2cntop  15422  dvcoapbr  15430  dvexp  15434  dvexp2  15435  dvmptid  15439  dveflem  15449  dvef  15450  plymullem1  15471  plyadd  15474  plymul  15475  plycoeid3  15480  plycjlemc  15483  plycj  15484  sin0pilem1  15504  sin2kpi  15534  cos2kpi  15535  coseq0q4123  15557  coseq0negpitopi  15559  sincosq1eq  15562  sinkpi  15570  coskpi  15571  1cxp  15623  mpodvdsmulf1o  15713  lgslem2  15729  lgsfcl2  15734  lgs0  15741  lgs2  15745  lgsneg  15752  lgsdilem  15755  lgsdir2lem4  15759  lgsdir2lem5  15760  lgsne0  15766  lgssq  15768  lgssq2  15769  gausslemma2dlem3  15791  gausslemma2dlem4  15792  lgseisenlem1  15798  lgsquadlem2  15806  lgsquad2lem2  15810  lgsquad3  15812  m1lgs  15813  2lgslem1a2  15815  2lgsoddprmlem3  15839  2sqlem9  15852  2sqlem10  15853  edgiedgbg  15915  isuhgrm  15921  isushgrm  15922  uhgr0vb  15934  uhgrun  15936  isupgren  15945  isumgren  15955  umgrnloop0  15967  upgrun  15976  umgrun  15978  isuspgren  16007  isusgren  16008  usgrf1oedg  16055  usgredg3  16064  egrsubgr  16113  0uhgrsubgr  16115  uhgrspansubgrlem  16126  vtxdg0v  16144  vtxdgfi0e  16145  vtxdfifiun  16147  vtxdumgrfival  16148  1loopgrvd2fi  16155  vdegp1cid  16166  wlkl1loop  16208  2wlklem  16226  upgr2wlkdc  16227  clwwlkn0  16258  clwwlkn1  16268  clwwlkn2  16271  umgr2cwwk2dif  16274  clwwlk0on0  16281  clwwlknonel  16282  clwwlknonex2lem1  16287  trlsegvdeglem4  16313  ex-ceil  16322  bj-intexr  16503  peano3nninf  16609  nninfall  16611  isomninnlem  16634  iswomni0  16655  ismkvnnlem  16656  nconstwlpolem0  16667  gfsumval  16680