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  5559  f1o00  5610  dffv4g  5626  fv2prc  5668  fnrnfv  5682  feqresmpt  5690  dffn5imf  5691  funfvdm2f  5701  fvun1  5702  fvmpt2  5720  fndmin  5744  fmptcof  5804  fmptcos  5805  funopdmsn  5823  fvunsng  5837  fvpr1  5847  fnrnov  6157  offval  6232  ofrfval  6233  op1std  6300  op2ndd  6301  fmpoco  6368  tpostpos  6416  tfr0  6475  rdgival  6534  frec0g  6549  2oconcl  6593  om0  6612  oei0  6613  oasuc  6618  omv2  6619  nnm0r  6633  uniqs2  6750  en1  6959  en1bg  6960  fundmen  6967  mapsnen  6972  en2  6981  xpsnen  6988  xpcomco  6993  xpdom2  6998  xpmapenlem  7018  exmidpweq  7082  unsnfidcex  7093  fiintim  7104  ssfirab  7109  sbthlemi8  7142  elfi2  7150  fi0  7153  fieq0  7154  djudom  7271  ismkvnex  7333  nninfwlpoimlemg  7353  en2other2  7385  exmidfodomrlemim  7390  nq0m0r  7654  addpinq1  7662  genipv  7707  genpelvl  7710  genpelvu  7711  cauappcvgprlem1  7857  caucvgsrlemoffres  7998  addresr  8035  mulresr  8036  axcnre  8079  add20  8632  rimul  8743  rereim  8744  mulreim  8762  sup3exmid  9115  fv0p1e1  9236  div4p1lem1div2  9376  nnm1nn0  9421  znegcl  9488  peano2z  9493  nneoor  9560  nn0ind-raph  9575  xnegneg  10041  xltnegi  10043  xaddpnf1  10054  xnegid  10067  xnn0xadd0  10075  xnegdi  10076  xsubge0  10089  xposdif  10090  xlesubadd  10091  xleaddadd  10095  fz0to4untppr  10332  fzo0to2pr  10436  nninfdcex  10469  fldiv4p1lem1div2  10537  fldiv4lem1div2  10539  mulp1mod1  10599  frecfzennn  10660  iseqf1olemqk  10741  exp0  10777  expp1  10780  expnegap0  10781  1exp  10802  mulexp  10812  m1expeven  10820  sq0i  10865  bernneq  10894  facp1  10964  faclbnd3  10977  facubnd  10979  bcval5  10997  hashinfom  11012  hashsng  11032  hashxp  11061  resunimafz0  11066  zfz1iso  11076  hash2en  11078  lsw1  11134  s1rn  11166  eqs1  11176  ccat1st1st  11188  swrd00g  11197  swrdlend  11206  swrds1  11216  cats1lend  11315  cats2catd  11317  s2leng  11337  s2dmg  11338  imre  11378  reim0b  11389  rereb  11390  resqrexlemover  11537  resqrexlemcalc1  11541  abs00bd  11593  maxabslemlub  11734  xrmaxiflemcom  11776  xrmaxadd  11788  climconst  11817  isumz  11916  fsumf1o  11917  fsumcllem  11926  fsumadd  11933  fsumxp  11963  fsumcnv  11964  fsummulc2  11975  fsumconst  11981  fsumabs  11992  telfsumo  11993  fsumparts  11997  fsumrelem  11998  fsumiun  12004  binomlem  12010  binom  12011  binom11  12013  isumsplit  12018  arisum  12025  arisum2  12026  trireciplem  12027  georeclim  12040  cvgratnnlemseq  12053  prodfrecap  12073  prod1dc  12113  fprodf1o  12115  fprodcl2lem  12132  fprodcllem  12133  fprodfac  12142  fprod2d  12150  fprodxp  12151  fprodcnv  12152  fprodrec  12156  fprodmodd  12168  ef0lem  12187  ege2le3  12198  efaddlem  12201  efcan  12203  eft0val  12220  ef4p  12221  efgt1p2  12222  efi4p  12244  sincossq  12275  cos2tsin  12278  absefi  12296  demoivreALT  12301  p1modz1  12321  dvdsabseq  12374  odd2np1lem  12399  oddp1even  12403  opoe  12422  m1expo  12427  m1exp1  12428  nn0o1gt2  12432  bitsinv1  12489  gcddvds  12500  gcdcl  12503  gcdeq0  12514  gcd0id  12516  bezoutr1  12570  nnmindc  12571  nnminle  12572  eucalg  12597  lcm0val  12603  lcmid  12618  rpmul  12636  dfphi2  12758  phiprmpw  12760  hashgcdeq  12778  odzdvds  12784  nnnn0modprm0  12794  pythagtriplem4  12807  pythagtriplem12  12814  pcaddlem  12878  pcmpt  12882  pockthi  12897  4sqlem12  12941  2expltfac  12978  ennnfonelem0  12992  ennnfonelem1  12994  ennnfonelemhdmp1  12996  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ennnfonelemf1  13005  ctiunctlemfo  13026  setsresg  13086  strressid  13120  strle1g  13155  restid2  13297  prdsbas3  13336  gsumwmhm  13547  grplactcnv  13651  mulg0  13678  mulgnn0gsum  13681  mulgneg  13693  mulgneg2  13709  gsumfzconst  13894  gsumfzsnfd  13898  gsumfzfsumlem0  14566  zrhval2  14599  mpl0fi  14682  tgval2  14741  tgidm  14764  epttop  14780  tgrest  14859  restco  14864  restsn  14870  tgcn  14898  cnptopresti  14928  cnptoprest  14929  txbas  14948  upxp  14962  txrest  14966  txdis  14967  txhmeo  15009  txswaphmeolem  15010  xblss2ps  15094  xblss2  15095  qtopbasss  15211  fsumcncntop  15257  hoverb  15338  limcimolemlt  15354  dvcnp2cntop  15389  dvcoapbr  15397  dvexp  15401  dvexp2  15402  dvmptid  15406  dveflem  15416  dvef  15417  plymullem1  15438  plyadd  15441  plymul  15442  plycoeid3  15447  plycjlemc  15450  plycj  15451  sin0pilem1  15471  sin2kpi  15501  cos2kpi  15502  coseq0q4123  15524  coseq0negpitopi  15526  sincosq1eq  15529  sinkpi  15537  coskpi  15538  1cxp  15590  mpodvdsmulf1o  15680  lgslem2  15696  lgsfcl2  15701  lgs0  15708  lgs2  15712  lgsneg  15719  lgsdilem  15722  lgsdir2lem4  15726  lgsdir2lem5  15727  lgsne0  15733  lgssq  15735  lgssq2  15736  gausslemma2dlem3  15758  gausslemma2dlem4  15759  lgseisenlem1  15765  lgsquadlem2  15773  lgsquad2lem2  15777  lgsquad3  15779  m1lgs  15780  2lgslem1a2  15782  2lgsoddprmlem3  15806  2sqlem9  15819  2sqlem10  15820  edgiedgbg  15881  isuhgrm  15887  isushgrm  15888  uhgr0vb  15900  uhgrun  15902  isupgren  15911  isumgren  15921  umgrnloop0  15933  upgrun  15940  umgrun  15942  isuspgren  15971  isusgren  15972  usgrf1oedg  16019  usgredg3  16028  vtxdg0v  16054  vtxdgfi0e  16055  vtxdfifiun  16057  vtxdumgrfival  16058  wlkl1loop  16104  2wlklem  16120  upgr2wlkdc  16121  clwwlkn0  16151  clwwlkn1  16160  clwwlkn2  16163  umgr2cwwk2dif  16166  ex-ceil  16173  bj-intexr  16354  peano3nninf  16461  nninfall  16463  isomninnlem  16486  iswomni0  16507  ismkvnnlem  16508  nconstwlpolem0  16519