Theorem eqtrdi 2256

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 2240	1 |- ( ph -> A = C )

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 2189

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

This theorem is referenced by:  eqtr2di  2257  eqtr4di  2258  3eqtr3g  2263  3eqtr4a  2266  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  csbprc  3514  un00  3515  disjssun  3532  disjpr2  3707  tppreq3  3746  diftpsn3  3785  ssprsseq  3806  preq12b  3824  intsng  3933  uniintsnr  3935  rint0  3938  riin0  4013  iununir  4025  intexr  4210  exmid1stab  4268  sucprc  4477  op1stbg  4544  elreldm  4923  xpeq0r  5124  xpdisj1  5126  xpdisj2  5127  resdisj  5130  xpima1  5148  xpima2m  5149  elxp4  5189  unixp0im  5238  uniabio  5261  iotass  5268  cnvresid  5367  funimacnv  5369  fimadmfo  5529  f1o00  5580  dffv4g  5596  fv2prc  5636  fnrnfv  5648  feqresmpt  5656  dffn5imf  5657  funfvdm2f  5667  fvun1  5668  fvmpt2  5686  fndmin  5710  fmptcof  5770  fmptcos  5771  funopdmsn  5787  fvunsng  5801  fvpr1  5811  fnrnov  6115  offval  6189  ofrfval  6190  op1std  6257  op2ndd  6258  fmpoco  6325  tpostpos  6373  tfr0  6432  rdgival  6491  frec0g  6506  2oconcl  6548  om0  6567  oei0  6568  oasuc  6573  omv2  6574  nnm0r  6588  uniqs2  6705  en1  6914  en1bg  6915  fundmen  6922  mapsnen  6927  en2  6936  xpsnen  6941  xpcomco  6946  xpdom2  6951  xpmapenlem  6971  exmidpweq  7032  unsnfidcex  7043  fiintim  7054  ssfirab  7059  sbthlemi8  7092  elfi2  7100  fi0  7103  fieq0  7104  djudom  7221  ismkvnex  7283  nninfwlpoimlemg  7303  en2other2  7335  exmidfodomrlemim  7340  nq0m0r  7604  addpinq1  7612  genipv  7657  genpelvl  7660  genpelvu  7661  cauappcvgprlem1  7807  caucvgsrlemoffres  7948  addresr  7985  mulresr  7986  axcnre  8029  add20  8582  rimul  8693  rereim  8694  mulreim  8712  sup3exmid  9065  fv0p1e1  9186  div4p1lem1div2  9326  nnm1nn0  9371  znegcl  9438  peano2z  9443  nneoor  9510  nn0ind-raph  9525  xnegneg  9990  xltnegi  9992  xaddpnf1  10003  xnegid  10016  xnn0xadd0  10024  xnegdi  10025  xsubge0  10038  xposdif  10039  xlesubadd  10040  xleaddadd  10044  fz0to4untppr  10281  fzo0to2pr  10384  nninfdcex  10417  fldiv4p1lem1div2  10485  fldiv4lem1div2  10487  mulp1mod1  10547  frecfzennn  10608  iseqf1olemqk  10689  exp0  10725  expp1  10728  expnegap0  10729  1exp  10750  mulexp  10760  m1expeven  10768  sq0i  10813  bernneq  10842  facp1  10912  faclbnd3  10925  facubnd  10927  bcval5  10945  hashinfom  10960  hashsng  10980  hashxp  11008  resunimafz0  11013  zfz1iso  11023  hash2en  11025  lsw1  11080  s1rn  11110  eqs1  11120  ccat1st1st  11131  swrd00g  11140  swrdlend  11149  swrds1  11159  imre  11277  reim0b  11288  rereb  11289  resqrexlemover  11436  resqrexlemcalc1  11440  abs00bd  11492  maxabslemlub  11633  xrmaxiflemcom  11675  xrmaxadd  11687  climconst  11716  isumz  11815  fsumf1o  11816  fsumcllem  11825  fsumadd  11832  fsumxp  11862  fsumcnv  11863  fsummulc2  11874  fsumconst  11880  fsumabs  11891  telfsumo  11892  fsumparts  11896  fsumrelem  11897  fsumiun  11903  binomlem  11909  binom  11910  binom11  11912  isumsplit  11917  arisum  11924  arisum2  11925  trireciplem  11926  georeclim  11939  cvgratnnlemseq  11952  prodfrecap  11972  prod1dc  12012  fprodf1o  12014  fprodcl2lem  12031  fprodcllem  12032  fprodfac  12041  fprod2d  12049  fprodxp  12050  fprodcnv  12051  fprodrec  12055  fprodmodd  12067  ef0lem  12086  ege2le3  12097  efaddlem  12100  efcan  12102  eft0val  12119  ef4p  12120  efgt1p2  12121  efi4p  12143  sincossq  12174  cos2tsin  12177  absefi  12195  demoivreALT  12200  p1modz1  12220  dvdsabseq  12273  odd2np1lem  12298  oddp1even  12302  opoe  12321  m1expo  12326  m1exp1  12327  nn0o1gt2  12331  bitsinv1  12388  gcddvds  12399  gcdcl  12402  gcdeq0  12413  gcd0id  12415  bezoutr1  12469  nnmindc  12470  nnminle  12471  eucalg  12496  lcm0val  12502  lcmid  12517  rpmul  12535  dfphi2  12657  phiprmpw  12659  hashgcdeq  12677  odzdvds  12683  nnnn0modprm0  12693  pythagtriplem4  12706  pythagtriplem12  12713  pcaddlem  12777  pcmpt  12781  pockthi  12796  4sqlem12  12840  2expltfac  12877  ennnfonelem0  12891  ennnfonelem1  12893  ennnfonelemhdmp1  12895  ennnfonelemkh  12898  ennnfonelemhf1o  12899  ennnfonelemf1  12904  ctiunctlemfo  12925  setsresg  12985  strressid  13018  strle1g  13053  restid2  13195  prdsbas3  13234  gsumwmhm  13445  grplactcnv  13549  mulg0  13576  mulgnn0gsum  13579  mulgneg  13591  mulgneg2  13607  gsumfzconst  13792  gsumfzsnfd  13796  gsumfzfsumlem0  14463  zrhval2  14496  mpl0fi  14579  tgval2  14638  tgidm  14661  epttop  14677  tgrest  14756  restco  14761  restsn  14767  tgcn  14795  cnptopresti  14825  cnptoprest  14826  txbas  14845  upxp  14859  txrest  14863  txdis  14864  txhmeo  14906  txswaphmeolem  14907  xblss2ps  14991  xblss2  14992  qtopbasss  15108  fsumcncntop  15154  hoverb  15235  limcimolemlt  15251  dvcnp2cntop  15286  dvcoapbr  15294  dvexp  15298  dvexp2  15299  dvmptid  15303  dveflem  15313  dvef  15314  plymullem1  15335  plyadd  15338  plymul  15339  plycoeid3  15344  plycjlemc  15347  plycj  15348  sin0pilem1  15368  sin2kpi  15398  cos2kpi  15399  coseq0q4123  15421  coseq0negpitopi  15423  sincosq1eq  15426  sinkpi  15434  coskpi  15435  1cxp  15487  mpodvdsmulf1o  15577  lgslem2  15593  lgsfcl2  15598  lgs0  15605  lgs2  15609  lgsneg  15616  lgsdilem  15619  lgsdir2lem4  15623  lgsdir2lem5  15624  lgsne0  15630  lgssq  15632  lgssq2  15633  gausslemma2dlem3  15655  gausslemma2dlem4  15656  lgseisenlem1  15662  lgsquadlem2  15670  lgsquad2lem2  15674  lgsquad3  15676  m1lgs  15677  2lgslem1a2  15679  2lgsoddprmlem3  15703  2sqlem9  15716  2sqlem10  15717  edgiedgbg  15776  isuhgrm  15782  isushgrm  15783  uhgr0vb  15795  uhgrun  15797  isupgren  15806  isumgren  15816  upgrun  15832  umgrun  15834  ex-ceil  15862  bj-intexr  16043  peano3nninf  16146  nninfall  16148  isomninnlem  16171  iswomni0  16192  ismkvnnlem  16193  nconstwlpolem0  16204