Theorem eqtrdi 2278

Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqtrdi.1	|- ( ph -> A = B )
eqtrdi.2	|- B = C

Assertion

Ref	Expression
eqtrdi	|- ( ph -> A = C )

Proof of Theorem eqtrdi

Step	Hyp	Ref	Expression
1		eqtrdi.1	. 2 |- ( ph -> A = B )
2		eqtrdi.2	. . 3 |- B = C
3	2	a1i 9	. 2 |- ( ph -> B = C )
4	1, 3	eqtrd 2262	1 |- ( ph -> A = C )

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  3809  ssprsseq  3830  preq12b  3848  intsng  3957  uniintsnr  3959  rint0  3962  riin0  4037  iununir  4049  intexr  4234  exmid1stab  4292  sucprc  4503  op1stbg  4570  elreldm  4950  xpeq0r  5151  xpdisj1  5153  xpdisj2  5154  resdisj  5157  xpima1  5175  xpima2m  5176  elxp4  5216  unixp0im  5265  uniabio  5289  iotass  5296  cnvresid  5395  funimacnv  5397  fimadmfo  5557  f1o00  5608  dffv4g  5624  fv2prc  5666  fnrnfv  5680  feqresmpt  5688  dffn5imf  5689  funfvdm2f  5699  fvun1  5700  fvmpt2  5718  fndmin  5742  fmptcof  5802  fmptcos  5803  funopdmsn  5819  fvunsng  5833  fvpr1  5843  fnrnov  6151  offval  6226  ofrfval  6227  op1std  6294  op2ndd  6295  fmpoco  6362  tpostpos  6410  tfr0  6469  rdgival  6528  frec0g  6543  2oconcl  6585  om0  6604  oei0  6605  oasuc  6610  omv2  6611  nnm0r  6625  uniqs2  6742  en1  6951  en1bg  6952  fundmen  6959  mapsnen  6964  en2  6973  xpsnen  6980  xpcomco  6985  xpdom2  6990  xpmapenlem  7010  exmidpweq  7071  unsnfidcex  7082  fiintim  7093  ssfirab  7098  sbthlemi8  7131  elfi2  7139  fi0  7142  fieq0  7143  djudom  7260  ismkvnex  7322  nninfwlpoimlemg  7342  en2other2  7374  exmidfodomrlemim  7379  nq0m0r  7643  addpinq1  7651  genipv  7696  genpelvl  7699  genpelvu  7700  cauappcvgprlem1  7846  caucvgsrlemoffres  7987  addresr  8024  mulresr  8025  axcnre  8068  add20  8621  rimul  8732  rereim  8733  mulreim  8751  sup3exmid  9104  fv0p1e1  9225  div4p1lem1div2  9365  nnm1nn0  9410  znegcl  9477  peano2z  9482  nneoor  9549  nn0ind-raph  9564  xnegneg  10029  xltnegi  10031  xaddpnf1  10042  xnegid  10055  xnn0xadd0  10063  xnegdi  10064  xsubge0  10077  xposdif  10078  xlesubadd  10079  xleaddadd  10083  fz0to4untppr  10320  fzo0to2pr  10424  nninfdcex  10457  fldiv4p1lem1div2  10525  fldiv4lem1div2  10527  mulp1mod1  10587  frecfzennn  10648  iseqf1olemqk  10729  exp0  10765  expp1  10768  expnegap0  10769  1exp  10790  mulexp  10800  m1expeven  10808  sq0i  10853  bernneq  10882  facp1  10952  faclbnd3  10965  facubnd  10967  bcval5  10985  hashinfom  11000  hashsng  11020  hashxp  11048  resunimafz0  11053  zfz1iso  11063  hash2en  11065  lsw1  11121  s1rn  11151  eqs1  11161  ccat1st1st  11172  swrd00g  11181  swrdlend  11190  swrds1  11200  cats1lend  11299  cats2catd  11301  s2leng  11321  s2dmg  11322  imre  11362  reim0b  11373  rereb  11374  resqrexlemover  11521  resqrexlemcalc1  11525  abs00bd  11577  maxabslemlub  11718  xrmaxiflemcom  11760  xrmaxadd  11772  climconst  11801  isumz  11900  fsumf1o  11901  fsumcllem  11910  fsumadd  11917  fsumxp  11947  fsumcnv  11948  fsummulc2  11959  fsumconst  11965  fsumabs  11976  telfsumo  11977  fsumparts  11981  fsumrelem  11982  fsumiun  11988  binomlem  11994  binom  11995  binom11  11997  isumsplit  12002  arisum  12009  arisum2  12010  trireciplem  12011  georeclim  12024  cvgratnnlemseq  12037  prodfrecap  12057  prod1dc  12097  fprodf1o  12099  fprodcl2lem  12116  fprodcllem  12117  fprodfac  12126  fprod2d  12134  fprodxp  12135  fprodcnv  12136  fprodrec  12140  fprodmodd  12152  ef0lem  12171  ege2le3  12182  efaddlem  12185  efcan  12187  eft0val  12204  ef4p  12205  efgt1p2  12206  efi4p  12228  sincossq  12259  cos2tsin  12262  absefi  12280  demoivreALT  12285  p1modz1  12305  dvdsabseq  12358  odd2np1lem  12383  oddp1even  12387  opoe  12406  m1expo  12411  m1exp1  12412  nn0o1gt2  12416  bitsinv1  12473  gcddvds  12484  gcdcl  12487  gcdeq0  12498  gcd0id  12500  bezoutr1  12554  nnmindc  12555  nnminle  12556  eucalg  12581  lcm0val  12587  lcmid  12602  rpmul  12620  dfphi2  12742  phiprmpw  12744  hashgcdeq  12762  odzdvds  12768  nnnn0modprm0  12778  pythagtriplem4  12791  pythagtriplem12  12798  pcaddlem  12862  pcmpt  12866  pockthi  12881  4sqlem12  12925  2expltfac  12962  ennnfonelem0  12976  ennnfonelem1  12978  ennnfonelemhdmp1  12980  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ennnfonelemf1  12989  ctiunctlemfo  13010  setsresg  13070  strressid  13104  strle1g  13139  restid2  13281  prdsbas3  13320  gsumwmhm  13531  grplactcnv  13635  mulg0  13662  mulgnn0gsum  13665  mulgneg  13677  mulgneg2  13693  gsumfzconst  13878  gsumfzsnfd  13882  gsumfzfsumlem0  14550  zrhval2  14583  mpl0fi  14666  tgval2  14725  tgidm  14748  epttop  14764  tgrest  14843  restco  14848  restsn  14854  tgcn  14882  cnptopresti  14912  cnptoprest  14913  txbas  14932  upxp  14946  txrest  14950  txdis  14951  txhmeo  14993  txswaphmeolem  14994  xblss2ps  15078  xblss2  15079  qtopbasss  15195  fsumcncntop  15241  hoverb  15322  limcimolemlt  15338  dvcnp2cntop  15373  dvcoapbr  15381  dvexp  15385  dvexp2  15386  dvmptid  15390  dveflem  15400  dvef  15401  plymullem1  15422  plyadd  15425  plymul  15426  plycoeid3  15431  plycjlemc  15434  plycj  15435  sin0pilem1  15455  sin2kpi  15485  cos2kpi  15486  coseq0q4123  15508  coseq0negpitopi  15510  sincosq1eq  15513  sinkpi  15521  coskpi  15522  1cxp  15574  mpodvdsmulf1o  15664  lgslem2  15680  lgsfcl2  15685  lgs0  15692  lgs2  15696  lgsneg  15703  lgsdilem  15706  lgsdir2lem4  15710  lgsdir2lem5  15711  lgsne0  15717  lgssq  15719  lgssq2  15720  gausslemma2dlem3  15742  gausslemma2dlem4  15743  lgseisenlem1  15749  lgsquadlem2  15757  lgsquad2lem2  15761  lgsquad3  15763  m1lgs  15764  2lgslem1a2  15766  2lgsoddprmlem3  15790  2sqlem9  15803  2sqlem10  15804  edgiedgbg  15865  isuhgrm  15871  isushgrm  15872  uhgr0vb  15884  uhgrun  15886  isupgren  15895  isumgren  15905  umgrnloop0  15917  upgrun  15924  umgrun  15926  isuspgren  15955  isusgren  15956  usgrf1oedg  16003  usgredg3  16012  wlkl1loop  16069  ex-ceil  16090  bj-intexr  16271  peano3nninf  16373  nninfall  16375  isomninnlem  16398  iswomni0  16419  ismkvnnlem  16420  nconstwlpolem0  16431