Theorem eqtrdi 2245

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  eqtr2di  2246  eqtr4di  2247  3eqtr3g  2252  3eqtr4a  2255  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  csbprc  3496  un00  3497  disjssun  3514  disjpr2  3686  tppreq3  3725  diftpsn3  3763  preq12b  3800  intsng  3908  uniintsnr  3910  rint0  3913  riin0  3988  iununir  4000  intexr  4183  exmid1stab  4241  sucprc  4447  op1stbg  4514  elreldm  4892  xpeq0r  5092  xpdisj1  5094  xpdisj2  5095  resdisj  5098  xpima1  5116  xpima2m  5117  elxp4  5157  unixp0im  5206  uniabio  5229  iotass  5236  cnvresid  5332  funimacnv  5334  fimadmfo  5489  f1o00  5539  dffv4g  5555  fv2prc  5595  fnrnfv  5607  feqresmpt  5615  dffn5imf  5616  funfvdm2f  5626  fvun1  5627  fvmpt2  5645  fndmin  5669  fmptcof  5729  fmptcos  5730  fvunsng  5756  fvpr1  5766  fnrnov  6069  offval  6143  ofrfval  6144  op1std  6206  op2ndd  6207  fmpoco  6274  tpostpos  6322  tfr0  6381  rdgival  6440  frec0g  6455  2oconcl  6497  om0  6516  oei0  6517  oasuc  6522  omv2  6523  nnm0r  6537  uniqs2  6654  en1  6858  en1bg  6859  fundmen  6865  mapsnen  6870  xpsnen  6880  xpcomco  6885  xpdom2  6890  xpmapenlem  6910  exmidpweq  6970  unsnfidcex  6981  fiintim  6992  ssfirab  6997  sbthlemi8  7030  elfi2  7038  fi0  7041  fieq0  7042  djudom  7159  ismkvnex  7221  nninfwlpoimlemg  7241  en2other2  7263  exmidfodomrlemim  7268  nq0m0r  7523  addpinq1  7531  genipv  7576  genpelvl  7579  genpelvu  7580  cauappcvgprlem1  7726  caucvgsrlemoffres  7867  addresr  7904  mulresr  7905  axcnre  7948  add20  8501  rimul  8612  rereim  8613  mulreim  8631  sup3exmid  8984  fv0p1e1  9105  div4p1lem1div2  9245  nnm1nn0  9290  znegcl  9357  peano2z  9362  nneoor  9428  nn0ind-raph  9443  xnegneg  9908  xltnegi  9910  xaddpnf1  9921  xnegid  9934  xnn0xadd0  9942  xnegdi  9943  xsubge0  9956  xposdif  9957  xlesubadd  9958  xleaddadd  9962  fz0to4untppr  10199  fzo0to2pr  10294  nninfdcex  10327  fldiv4p1lem1div2  10395  fldiv4lem1div2  10397  mulp1mod1  10457  frecfzennn  10518  iseqf1olemqk  10599  exp0  10635  expp1  10638  expnegap0  10639  1exp  10660  mulexp  10670  m1expeven  10678  sq0i  10723  bernneq  10752  facp1  10822  faclbnd3  10835  facubnd  10837  bcval5  10855  hashinfom  10870  hashsng  10890  hashxp  10918  resunimafz0  10923  zfz1iso  10933  imre  11016  reim0b  11027  rereb  11028  resqrexlemover  11175  resqrexlemcalc1  11179  abs00bd  11231  maxabslemlub  11372  xrmaxiflemcom  11414  xrmaxadd  11426  climconst  11455  isumz  11554  fsumf1o  11555  fsumcllem  11564  fsumadd  11571  fsumxp  11601  fsumcnv  11602  fsummulc2  11613  fsumconst  11619  fsumabs  11630  telfsumo  11631  fsumparts  11635  fsumrelem  11636  fsumiun  11642  binomlem  11648  binom  11649  binom11  11651  isumsplit  11656  arisum  11663  arisum2  11664  trireciplem  11665  georeclim  11678  cvgratnnlemseq  11691  prodfrecap  11711  prod1dc  11751  fprodf1o  11753  fprodcl2lem  11770  fprodcllem  11771  fprodfac  11780  fprod2d  11788  fprodxp  11789  fprodcnv  11790  fprodrec  11794  fprodmodd  11806  ef0lem  11825  ege2le3  11836  efaddlem  11839  efcan  11841  eft0val  11858  ef4p  11859  efgt1p2  11860  efi4p  11882  sincossq  11913  cos2tsin  11916  absefi  11934  demoivreALT  11939  p1modz1  11959  dvdsabseq  12012  odd2np1lem  12037  oddp1even  12041  opoe  12060  m1expo  12065  m1exp1  12066  nn0o1gt2  12070  gcddvds  12130  gcdcl  12133  gcdeq0  12144  gcd0id  12146  bezoutr1  12200  nnmindc  12201  nnminle  12202  eucalg  12227  lcm0val  12233  lcmid  12248  rpmul  12266  dfphi2  12388  phiprmpw  12390  hashgcdeq  12408  odzdvds  12414  nnnn0modprm0  12424  pythagtriplem4  12437  pythagtriplem12  12444  pcaddlem  12508  pcmpt  12512  pockthi  12527  4sqlem12  12571  2expltfac  12608  ennnfonelem0  12622  ennnfonelem1  12624  ennnfonelemhdmp1  12626  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemf1  12635  ctiunctlemfo  12656  setsresg  12716  strressid  12749  strle1g  12784  restid2  12919  gsumwmhm  13130  grplactcnv  13234  mulg0  13255  mulgnn0gsum  13258  mulgneg  13270  mulgneg2  13286  gsumfzconst  13471  gsumfzsnfd  13475  gsumfzfsumlem0  14142  zrhval2  14175  tgval2  14287  tgidm  14310  epttop  14326  tgrest  14405  restco  14410  restsn  14416  tgcn  14444  cnptopresti  14474  cnptoprest  14475  txbas  14494  upxp  14508  txrest  14512  txdis  14513  txhmeo  14555  txswaphmeolem  14556  xblss2ps  14640  xblss2  14641  qtopbasss  14757  fsumcncntop  14803  hoverb  14884  limcimolemlt  14900  dvcnp2cntop  14935  dvcoapbr  14943  dvexp  14947  dvexp2  14948  dvmptid  14952  dveflem  14962  dvef  14963  plymullem1  14984  plyadd  14987  plymul  14988  plycoeid3  14993  plycjlemc  14996  plycj  14997  sin0pilem1  15017  sin2kpi  15047  cos2kpi  15048  coseq0q4123  15070  coseq0negpitopi  15072  sincosq1eq  15075  sinkpi  15083  coskpi  15084  1cxp  15136  mpodvdsmulf1o  15226  lgslem2  15242  lgsfcl2  15247  lgs0  15254  lgs2  15258  lgsneg  15265  lgsdilem  15268  lgsdir2lem4  15272  lgsdir2lem5  15273  lgsne0  15279  lgssq  15281  lgssq2  15282  gausslemma2dlem3  15304  gausslemma2dlem4  15305  lgseisenlem1  15311  lgsquadlem2  15319  lgsquad2lem2  15323  lgsquad3  15325  m1lgs  15326  2lgslem1a2  15328  2lgsoddprmlem3  15352  2sqlem9  15365  2sqlem10  15366  ex-ceil  15372  bj-intexr  15554  peano3nninf  15651  nninfall  15653  isomninnlem  15674  iswomni0  15695  ismkvnnlem  15696  nconstwlpolem0  15707