Theorem eqtrdi 2255

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  eqtr2di  2256  eqtr4di  2257  3eqtr3g  2262  3eqtr4a  2265  cbvralcsf  3160  cbvrexcsf  3161  cbvreucsf  3162  cbvrabcsf  3163  csbprc  3510  un00  3511  disjssun  3528  disjpr2  3702  tppreq3  3741  diftpsn3  3780  preq12b  3817  intsng  3925  uniintsnr  3927  rint0  3930  riin0  4005  iununir  4017  intexr  4202  exmid1stab  4260  sucprc  4467  op1stbg  4534  elreldm  4913  xpeq0r  5114  xpdisj1  5116  xpdisj2  5117  resdisj  5120  xpima1  5138  xpima2m  5139  elxp4  5179  unixp0im  5228  uniabio  5251  iotass  5258  cnvresid  5357  funimacnv  5359  fimadmfo  5519  f1o00  5570  dffv4g  5586  fv2prc  5626  fnrnfv  5638  feqresmpt  5646  dffn5imf  5647  funfvdm2f  5657  fvun1  5658  fvmpt2  5676  fndmin  5700  fmptcof  5760  fmptcos  5761  funopdmsn  5777  fvunsng  5791  fvpr1  5801  fnrnov  6105  offval  6179  ofrfval  6180  op1std  6247  op2ndd  6248  fmpoco  6315  tpostpos  6363  tfr0  6422  rdgival  6481  frec0g  6496  2oconcl  6538  om0  6557  oei0  6558  oasuc  6563  omv2  6564  nnm0r  6578  uniqs2  6695  en1  6904  en1bg  6905  fundmen  6912  mapsnen  6917  en2  6926  xpsnen  6931  xpcomco  6936  xpdom2  6941  xpmapenlem  6961  exmidpweq  7021  unsnfidcex  7032  fiintim  7043  ssfirab  7048  sbthlemi8  7081  elfi2  7089  fi0  7092  fieq0  7093  djudom  7210  ismkvnex  7272  nninfwlpoimlemg  7292  en2other2  7320  exmidfodomrlemim  7325  nq0m0r  7589  addpinq1  7597  genipv  7642  genpelvl  7645  genpelvu  7646  cauappcvgprlem1  7792  caucvgsrlemoffres  7933  addresr  7970  mulresr  7971  axcnre  8014  add20  8567  rimul  8678  rereim  8679  mulreim  8697  sup3exmid  9050  fv0p1e1  9171  div4p1lem1div2  9311  nnm1nn0  9356  znegcl  9423  peano2z  9428  nneoor  9495  nn0ind-raph  9510  xnegneg  9975  xltnegi  9977  xaddpnf1  9988  xnegid  10001  xnn0xadd0  10009  xnegdi  10010  xsubge0  10023  xposdif  10024  xlesubadd  10025  xleaddadd  10029  fz0to4untppr  10266  fzo0to2pr  10369  nninfdcex  10402  fldiv4p1lem1div2  10470  fldiv4lem1div2  10472  mulp1mod1  10532  frecfzennn  10593  iseqf1olemqk  10674  exp0  10710  expp1  10713  expnegap0  10714  1exp  10735  mulexp  10745  m1expeven  10753  sq0i  10798  bernneq  10827  facp1  10897  faclbnd3  10910  facubnd  10912  bcval5  10930  hashinfom  10945  hashsng  10965  hashxp  10993  resunimafz0  10998  zfz1iso  11008  hash2en  11010  lsw1  11065  s1rn  11095  eqs1  11105  ccat1st1st  11116  swrd00g  11125  swrdlend  11134  swrds1  11144  imre  11237  reim0b  11248  rereb  11249  resqrexlemover  11396  resqrexlemcalc1  11400  abs00bd  11452  maxabslemlub  11593  xrmaxiflemcom  11635  xrmaxadd  11647  climconst  11676  isumz  11775  fsumf1o  11776  fsumcllem  11785  fsumadd  11792  fsumxp  11822  fsumcnv  11823  fsummulc2  11834  fsumconst  11840  fsumabs  11851  telfsumo  11852  fsumparts  11856  fsumrelem  11857  fsumiun  11863  binomlem  11869  binom  11870  binom11  11872  isumsplit  11877  arisum  11884  arisum2  11885  trireciplem  11886  georeclim  11899  cvgratnnlemseq  11912  prodfrecap  11932  prod1dc  11972  fprodf1o  11974  fprodcl2lem  11991  fprodcllem  11992  fprodfac  12001  fprod2d  12009  fprodxp  12010  fprodcnv  12011  fprodrec  12015  fprodmodd  12027  ef0lem  12046  ege2le3  12057  efaddlem  12060  efcan  12062  eft0val  12079  ef4p  12080  efgt1p2  12081  efi4p  12103  sincossq  12134  cos2tsin  12137  absefi  12155  demoivreALT  12160  p1modz1  12180  dvdsabseq  12233  odd2np1lem  12258  oddp1even  12262  opoe  12281  m1expo  12286  m1exp1  12287  nn0o1gt2  12291  bitsinv1  12348  gcddvds  12359  gcdcl  12362  gcdeq0  12373  gcd0id  12375  bezoutr1  12429  nnmindc  12430  nnminle  12431  eucalg  12456  lcm0val  12462  lcmid  12477  rpmul  12495  dfphi2  12617  phiprmpw  12619  hashgcdeq  12637  odzdvds  12643  nnnn0modprm0  12653  pythagtriplem4  12666  pythagtriplem12  12673  pcaddlem  12737  pcmpt  12741  pockthi  12756  4sqlem12  12800  2expltfac  12837  ennnfonelem0  12851  ennnfonelem1  12853  ennnfonelemhdmp1  12855  ennnfonelemkh  12858  ennnfonelemhf1o  12859  ennnfonelemf1  12864  ctiunctlemfo  12885  setsresg  12945  strressid  12978  strle1g  13013  restid2  13155  prdsbas3  13194  gsumwmhm  13405  grplactcnv  13509  mulg0  13536  mulgnn0gsum  13539  mulgneg  13551  mulgneg2  13567  gsumfzconst  13752  gsumfzsnfd  13756  gsumfzfsumlem0  14423  zrhval2  14456  mpl0fi  14539  tgval2  14598  tgidm  14621  epttop  14637  tgrest  14716  restco  14721  restsn  14727  tgcn  14755  cnptopresti  14785  cnptoprest  14786  txbas  14805  upxp  14819  txrest  14823  txdis  14824  txhmeo  14866  txswaphmeolem  14867  xblss2ps  14951  xblss2  14952  qtopbasss  15068  fsumcncntop  15114  hoverb  15195  limcimolemlt  15211  dvcnp2cntop  15246  dvcoapbr  15254  dvexp  15258  dvexp2  15259  dvmptid  15263  dveflem  15273  dvef  15274  plymullem1  15295  plyadd  15298  plymul  15299  plycoeid3  15304  plycjlemc  15307  plycj  15308  sin0pilem1  15328  sin2kpi  15358  cos2kpi  15359  coseq0q4123  15381  coseq0negpitopi  15383  sincosq1eq  15386  sinkpi  15394  coskpi  15395  1cxp  15447  mpodvdsmulf1o  15537  lgslem2  15553  lgsfcl2  15558  lgs0  15565  lgs2  15569  lgsneg  15576  lgsdilem  15579  lgsdir2lem4  15583  lgsdir2lem5  15584  lgsne0  15590  lgssq  15592  lgssq2  15593  gausslemma2dlem3  15615  gausslemma2dlem4  15616  lgseisenlem1  15622  lgsquadlem2  15630  lgsquad2lem2  15634  lgsquad3  15636  m1lgs  15637  2lgslem1a2  15639  2lgsoddprmlem3  15663  2sqlem9  15676  2sqlem10  15677  edgiedgbg  15736  isuhgrm  15742  isushgrm  15743  uhgr0vb  15755  uhgrun  15757  isupgren  15766  isumgren  15776  upgrun  15792  umgrun  15794  ex-ceil  15801  bj-intexr  15982  peano3nninf  16085  nninfall  16087  isomninnlem  16110  iswomni0  16131  ismkvnnlem  16132  nconstwlpolem0  16143