Theorem eqtrdi 2281

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  eqtr2di  2282  eqtr4di  2283  3eqtr3g  2288  3eqtr4a  2291  cbvralcsf  3200  cbvrexcsf  3201  cbvreucsf  3202  cbvrabcsf  3203  csbprc  3551  un00  3552  disjssun  3569  disjpr2  3746  tppreq3  3787  diftpsn3  3828  ssprsseq  3849  preq12b  3867  intsng  3976  uniintsnr  3978  rint0  3981  riin0  4056  iununir  4068  intexr  4254  exmid1stab  4313  sucprc  4524  op1stbg  4591  elreldm  4974  xpeq0r  5176  xpdisj1  5178  xpdisj2  5179  resdisj  5182  xpima1  5200  xpima2m  5201  elxp4  5241  unixp0im  5290  uniabio  5314  iotass  5321  cnvresid  5421  funimacnv  5423  fresaunres2disj  5536  fimadmfo  5590  f1o00  5642  dffv4g  5658  fv2prc  5700  fnrnfv  5714  feqresmpt  5722  dffn5imf  5723  funfvdm2f  5733  fvun1  5734  fvmpt2  5752  fndmin  5776  fmptcof  5835  fmptcos  5836  funopdmsn  5855  fvunsng  5869  fvpr1  5879  fnrnov  6191  offval  6265  ofrfval  6266  op1std  6333  op2ndd  6334  fmpoco  6403  suppsnopdc  6441  mptsuppdifd  6446  supp0cosupp0fn  6458  tpostpos  6486  tfr0  6545  rdgival  6604  frec0g  6619  2oconcl  6663  om0  6682  oei0  6683  oasuc  6688  omv2  6689  nnm0r  6703  uniqs2  6820  en1  7030  en1bg  7031  fundmen  7038  mapsnen  7044  en2  7056  xpsnen  7063  xpcomco  7068  xpdom2  7073  xpmapenlem  7093  exmidpweq  7160  unsnfidcex  7171  fiintim  7182  ssfirab  7188  sbthlemi8  7225  elfi2  7250  fi0  7253  fieq0  7254  djudom  7375  ismkvnex  7437  nninfwlpoimlemg  7457  en2other2  7490  exmidfodomrlemim  7495  nq0m0r  7759  addpinq1  7767  genipv  7812  genpelvl  7815  genpelvu  7816  cauappcvgprlem1  7962  caucvgsrlemoffres  8103  addresr  8140  mulresr  8141  axcnre  8184  add20  8736  rimul  8847  rereim  8848  mulreim  8866  sup3exmid  9219  fv0p1e1  9340  div4p1lem1div2  9480  nnm1nn0  9525  znegcl  9594  peano2z  9599  nneoor  9666  nn0ind-raph  9681  xnegneg  10152  xltnegi  10154  xaddpnf1  10165  xnegid  10178  xnn0xadd0  10186  xnegdi  10187  xsubge0  10200  xposdif  10201  xlesubadd  10202  xleaddadd  10206  fz0to4untppr  10444  fzo0to2pr  10549  nninfdcex  10583  fldiv4p1lem1div2  10651  fldiv4lem1div2  10653  mulp1mod1  10713  frecfzennn  10774  iseqf1olemqk  10855  exp0  10891  expp1  10894  expnegap0  10895  1exp  10916  mulexp  10926  m1expeven  10934  sq0i  10979  bernneq  11008  facp1  11078  faclbnd3  11091  facubnd  11093  bcval5  11111  hashinfom  11126  hashsng  11146  hashxp  11176  resunimafz0  11181  zfz1iso  11191  hash2en  11193  hashtpgim  11195  lsw1  11252  s1rn  11284  eqs1  11294  ccat1st1st  11307  swrd00g  11319  swrdlend  11328  swrds1  11338  cats1lend  11437  cats2catd  11439  s2leng  11459  s2dmg  11460  imre  11514  reim0b  11525  rereb  11526  resqrexlemover  11673  resqrexlemcalc1  11677  abs00bd  11729  maxabslemlub  11870  xrmaxiflemcom  11912  xrmaxadd  11924  climconst  11953  fzf1o  12039  isumz  12053  fsumf1o  12054  fsumcllem  12063  fsumadd  12070  fsumxp  12100  fsumcnv  12101  fsummulc2  12112  fsumconst  12118  fsumabs  12129  telfsumo  12130  fsumparts  12134  fsumrelem  12135  fsumiun  12141  binomlem  12147  binom  12148  binom11  12150  isumsplit  12155  arisum  12162  arisum2  12163  trireciplem  12164  georeclim  12177  cvgratnnlemseq  12190  prodfrecap  12210  prod1dc  12250  fprodf1o  12252  fprodcl2lem  12269  fprodcllem  12270  fprodfac  12279  fprod2d  12287  fprodxp  12288  fprodcnv  12289  fprodrec  12293  fprodmodd  12305  ef0lem  12324  ege2le3  12335  efaddlem  12338  efcan  12340  eft0val  12357  ef4p  12358  efgt1p2  12359  efi4p  12381  sincossq  12412  cos2tsin  12415  absefi  12433  demoivreALT  12438  p1modz1  12458  dvdsabseq  12511  odd2np1lem  12536  oddp1even  12540  opoe  12559  m1expo  12564  m1exp1  12565  nn0o1gt2  12569  bitsinv1  12626  gcddvds  12637  gcdcl  12640  gcdeq0  12651  gcd0id  12653  bezoutr1  12707  nnmindc  12708  nnminle  12709  eucalg  12734  lcm0val  12740  lcmid  12755  rpmul  12773  dfphi2  12895  phiprmpw  12897  hashgcdeq  12915  odzdvds  12921  nnnn0modprm0  12931  pythagtriplem4  12944  pythagtriplem12  12951  pcaddlem  13015  pcmpt  13019  pockthi  13034  4sqlem12  13078  2expltfac  13115  ennnfonelem0  13130  ennnfonelem1  13132  ennnfonelemhdmp1  13134  ennnfonelemkh  13137  ennnfonelemhf1o  13138  ennnfonelemf1  13143  ctiunctlemfo  13164  setsresg  13224  strressid  13258  strle1g  13293  restid2  13435  prdsbas3  13474  gsumwmhm  13685  grplactcnv  13789  mulg0  13816  mulgnn0gsum  13819  mulgneg  13831  mulgneg2  13847  gsumfzconst  14032  gsumfzsnfd  14036  gsumsplit0  14037  gsumfzfsumlem0  14706  zrhval2  14739  mpl0fi  14827  tgval2  14886  tgidm  14909  epttop  14925  tgrest  15004  restco  15009  restsn  15015  tgcn  15043  cnptopresti  15073  cnptoprest  15074  txbas  15093  upxp  15107  txrest  15111  txdis  15112  txhmeo  15154  txswaphmeolem  15155  xblss2ps  15239  xblss2  15240  qtopbasss  15356  fsumcncntop  15402  hoverb  15483  limcimolemlt  15499  dvcnp2cntop  15534  dvcoapbr  15542  dvexp  15546  dvexp2  15547  dvmptid  15551  dveflem  15561  dvef  15562  plymullem1  15583  plyadd  15586  plymul  15587  plycoeid3  15592  plycjlemc  15595  plycj  15596  sin0pilem1  15616  sin2kpi  15646  cos2kpi  15647  coseq0q4123  15669  coseq0negpitopi  15671  sincosq1eq  15674  sinkpi  15682  coskpi  15683  1cxp  15735  mpodvdsmulf1o  15828  lgslem2  15844  lgsfcl2  15849  lgs0  15856  lgs2  15860  lgsneg  15867  lgsdilem  15870  lgsdir2lem4  15874  lgsdir2lem5  15875  lgsne0  15881  lgssq  15883  lgssq2  15884  gausslemma2dlem3  15906  gausslemma2dlem4  15907  lgseisenlem1  15913  lgsquadlem2  15921  lgsquad2lem2  15925  lgsquad3  15927  m1lgs  15928  2lgslem1a2  15930  2lgsoddprmlem3  15954  2sqlem9  15967  2sqlem10  15968  edgiedgbg  16030  isuhgrm  16036  isushgrm  16037  uhgr0vb  16049  uhgrun  16051  isupgren  16060  isumgren  16070  umgrnloop0  16082  upgrun  16091  umgrun  16093  isuspgren  16122  isusgren  16123  usgrf1oedg  16170  usgredg3  16179  egrsubgr  16228  0uhgrsubgr  16230  uhgrspansubgrlem  16241  vtxdg0v  16259  vtxdgfi0e  16260  vtxdfifiun  16262  vtxdumgrfival  16263  1loopgrvd2fi  16270  vdegp1cid  16281  wlkl1loop  16323  2wlklem  16341  upgr2wlkdc  16342  clwwlkn0  16373  clwwlkn1  16383  clwwlkn2  16386  umgr2cwwk2dif  16389  clwwlk0on0  16396  clwwlknonel  16397  clwwlknonex2lem1  16402  trlsegvdeglem4  16428  eupthvdres  16440  eupth2lembfi  16442  konigsberglem1  16453  konigsberglem2  16454  konigsberglem3  16455  ex-ceil  16464  bj-intexr  16648  peano3nninf  16755  nninfall  16757  isomninnlem  16784  iswomni0  16806  ismkvnnlem  16807  nconstwlpolem0  16818  gfsumval  16831  gfsumsn  16836  gfsump1  16837