Theorem eqtrdi 2287

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr2di  2288  eqtr4di  2289  3eqtr3g  2294  3eqtr4a  2297  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  un00  3567  vvin  3569  csbprc  3572  disjssun  3588  disjpr2  3773  tppreq3  3814  diftpsn3  3856  ssprsseq  3877  preq12b  3895  intsng  4004  uniintsnr  4006  rint0  4009  riin0  4084  iununir  4096  intexr  4286  exmid1stab  4345  sucprc  4557  op1stbg  4625  elreldm  5008  xpeq0r  5210  xpdisj1  5212  xpdisj2  5213  resdisj  5216  xpima1  5234  xpima2m  5235  elxp4  5275  unixp0im  5324  uniabio  5348  iotass  5355  cnvresid  5455  funimacnv  5457  fresaunres2disj  5570  fimadmfo  5624  f1o00  5676  dffv4g  5692  fv2prc  5735  fnrnfv  5749  feqresmpt  5757  dffn5imf  5758  funfvdm2f  5768  fvun1  5769  fvmpt2  5789  fndmin  5816  fmptcof  5875  fmptcos  5876  funopdmsn  5895  fvunsng  5909  fvpr1  5919  dfimafnf  5955  fnrnov  6235  f1o3d  6298  offval  6310  ofrfval  6311  op1std  6382  op2ndd  6383  fmpoco  6452  suppsnopdc  6490  mptsuppdifd  6495  supp0cosupp0fn  6507  tpostpos  6535  tfr0  6594  rdgival  6653  frec0g  6668  2oconcl  6712  om0  6731  oei0  6732  oasuc  6737  omv2  6738  nnm0r  6752  uniqs2  6869  en1  7086  en1bg  7087  fundmen  7094  mapsnen  7100  en2  7112  xpsnen  7119  xpcomco  7124  xpdom2  7129  xpmapenlem  7149  exmidpweq  7216  unsnfidcex  7227  fiintim  7238  ssfirab  7244  sbthlemi8  7281  elfi2  7306  fi0  7309  fieq0  7310  djudom  7433  ismkvnex  7495  nninfwlpoimlemg  7515  en2other2  7548  exmidfodomrlemim  7553  nq0m0r  7823  addpinq1  7831  genipv  7876  genpelvl  7879  genpelvu  7880  cauappcvgprlem1  8026  caucvgsrlemoffres  8167  addresr  8204  mulresr  8205  axcnre  8248  add20  8802  rimul  8913  rereim  8914  mulreim  8932  sup3exmid  9287  fv0p1e1  9419  div4p1lem1div2  9559  nnm1nn0  9604  znegcl  9675  peano2z  9680  nneoor  9748  nn0ind-raph  9763  xnegneg  10235  xltnegi  10237  xaddpnf1  10248  xnegid  10261  xnn0xadd0  10269  xnegdi  10270  xsubge0  10283  xposdif  10284  xlesubadd  10285  xleaddadd  10289  fz0to4untppr  10531  fzo0to2pr  10636  nninfdcex  10672  fldiv4p1lem1div2  10740  fldiv4lem1div2  10742  mulp1mod1  10802  frecfzennn  10863  iseqf1olemqk  10944  exp0  10980  expp1  10983  expnegap0  10984  1exp  11005  mulexp  11015  m1expeven  11023  sq0i  11068  bernneq  11098  facp1  11168  faclbnd3  11181  facubnd  11183  bcval5  11201  hashinfom  11217  hashsng  11237  hashxp  11267  hashpwfi  11269  resunimafz0  11274  ssenneg  11280  hashfibclem  11282  hashfibc  11283  hashf1lem2  11286  hashf1  11287  zfz1iso  11293  hash2en  11295  hashtpgim  11297  lsw1  11354  s1rn  11386  eqs1  11396  ccat1st1st  11409  swrd00g  11421  swrdlend  11430  swrds1  11440  cats1lend  11539  cats2catd  11541  s2leng  11561  s2dmg  11562  imre  11616  reim0b  11627  rereb  11628  sq01  11660  resqrexlemover  11776  resqrexlemcalc1  11780  abs00bd  11832  maxabslemlub  11973  xrmaxiflemcom  12015  xrmaxadd  12027  climconst  12056  fzf1o  12142  isumz  12156  fsumf1o  12157  fsumcllem  12166  fsumadd  12173  fsumxp  12203  fsumcnv  12204  fsummulc2  12215  fsumconst  12221  fsumabs  12232  telfsumo  12233  fsumparts  12237  fsumrelem  12238  fsumiun  12244  binomlem  12250  binom  12251  binom11  12253  isumsplit  12258  arisum  12265  arisum2  12266  trireciplem  12267  georeclim  12280  cvgratnnlemseq  12293  prodfrecap  12313  prod1dc  12353  fprodf1o  12355  fprodcl2lem  12372  fprodcllem  12373  fprodfac  12382  fprod2d  12390  fprodxp  12391  fprodcnv  12392  fprodrec  12396  fprodmodd  12408  ef0lem  12427  ege2le3  12438  efaddlem  12441  efcan  12443  eft0val  12460  ef4p  12461  efgt1p2  12462  efi4p  12484  sincossq  12515  cos2tsin  12518  absefi  12536  demoivreALT  12541  p1modz1  12561  dvdsabseq  12614  odd2np1lem  12639  oddp1even  12643  opoe  12662  m1expo  12667  m1exp1  12668  nn0o1gt2  12672  bitsinv1  12729  gcddvds  12740  gcdcl  12743  gcdeq0  12754  gcd0id  12756  bezoutr1  12810  nnmindc  12811  nnminle  12812  eucalg  12837  lcm0val  12843  lcmid  12858  rpmul  12876  dfphi2  12998  phiprmpw  13000  hashgcdeq  13018  odzdvds  13024  nnnn0modprm0  13034  pythagtriplem4  13047  pythagtriplem12  13054  pcaddlem  13118  pcmpt  13122  pockthi  13137  4sqlem12  13181  2expltfac  13218  ballotfilemfp1  13231  ballotfilemfval0  13235  ballotfilemsv  13253  ennnfonelem0  13296  ennnfonelem1  13298  ennnfonelemhdmp1  13300  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemf1  13309  ctiunctlemfo  13330  setsresg  13390  strressid  13425  strle1g  13460  restid2  13602  gzsumwmhm  13803  grplactcnv  13907  mulg0  13928  mulgnn0gzsum  13931  mulgneg  13943  mulgneg2  13959  gzsumconst  14143  gzsumsnfd  14147  gzsumsplit0  14148  gsumvalfi  14152  gsumsncmn  14156  gsump1  14157  gsummptfidmadd  14161  gsummhmfi  14164  prdsbas3  14187  zrhval2  14954  assamulgscmlem2  15042  mpl0fi  15093  tgval2  15152  tgidm  15175  epttop  15191  tgrest  15270  restco  15275  restsn  15281  tgcn  15309  cnptopresti  15339  cnptoprest  15340  txbas  15359  upxp  15373  txrest  15377  txdis  15378  txhmeo  15420  txswaphmeolem  15421  xblss2ps  15505  xblss2  15506  qtopbasss  15622  fsumcncntop  15668  hoverb  15749  limcimolemlt  15765  dvcnp2cntop  15800  dvcoapbr  15808  dvexp  15812  dvexp2  15813  dvmptid  15817  dveflem  15827  dvef  15828  plymullem1  15849  plyadd  15852  plymul  15853  plycoeid3  15858  plycjlemc  15861  plycj  15862  sin0pilem1  15882  sin2kpi  15912  cos2kpi  15913  coseq0q4123  15935  coseq0negpitopi  15937  sincosq1eq  15940  sinkpi  15948  coskpi  15949  logfac  15995  1cxp  16002  birthdaylem2  16088  birthdaylem3  16089  mpodvdsmulf1o  16104  lgslem2  16120  lgsfcl2  16125  lgs0  16132  lgs2  16136  lgsneg  16143  lgsdilem  16146  lgsdir2lem4  16150  lgsdir2lem5  16151  lgsne0  16157  lgssq  16159  lgssq2  16160  gausslemma2dlem3  16182  gausslemma2dlem4  16183  lgseisenlem1  16189  lgsquadlem2  16197  lgsquad2lem2  16201  lgsquad3  16203  m1lgs  16204  2lgslem1a2  16206  2lgsoddprmlem3  16230  2sqlem9  16243  2sqlem10  16244  edgiedgbg  16306  isuhgrm  16312  isushgrm  16313  uhgr0vb  16325  uhgrun  16327  isupgren  16336  isumgren  16346  umgrnloop0  16358  upgrun  16367  umgrun  16369  isuspgren  16398  isusgren  16399  usgrf1oedg  16446  usgredg3  16455  egrsubgr  16504  0uhgrsubgr  16506  uhgrspansubgrlem  16517  vtxdg0v  16535  vtxdgfi0e  16536  vtxdfifiun  16538  vtxdumgrfival  16539  1loopgrvd2fi  16546  vdegp1cid  16557  wlkl1loop  16599  2wlklem  16617  upgr2wlkdc  16618  clwwlkn0  16649  clwwlkn1  16659  clwwlkn2  16662  umgr2cwwk2dif  16665  clwwlk0on0  16672  clwwlknonel  16673  clwwlknonex2lem1  16678  trlsegvdeglem4  16704  eupthvdres  16716  eupth2lembfi  16718  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  ex-ceil  16740  bj-intexr  16934  wexmiddiffilem  17043  wexmiddifxylem  17045  peano3nninf  17050  nninfall  17052  isomninnlem  17079  iswomni0  17101  ismkvnnlem  17102  nconstwlpolem0  17113