Theorem eqtrdi 2226

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqtr2di  2227  eqtr4di  2228  3eqtr3g  2233  3eqtr4a  2236  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  csbprc  3469  un00  3470  disjssun  3487  disjpr2  3657  tppreq3  3696  diftpsn3  3734  preq12b  3771  intsng  3879  uniintsnr  3881  rint0  3884  riin0  3959  iununir  3971  intexr  4151  exmid1stab  4209  sucprc  4413  op1stbg  4480  elreldm  4854  xpeq0r  5052  xpdisj1  5054  xpdisj2  5055  resdisj  5058  xpima1  5076  xpima2m  5077  elxp4  5117  unixp0im  5166  uniabio  5189  iotass  5196  cnvresid  5291  funimacnv  5293  f1o00  5497  dffv4g  5513  fnrnfv  5563  feqresmpt  5571  dffn5imf  5572  funfvdm2f  5582  fvun1  5583  fvmpt2  5600  fndmin  5624  fmptcof  5684  fmptcos  5685  fvunsng  5711  fvpr1  5721  fnrnov  6020  offval  6090  ofrfval  6091  op1std  6149  op2ndd  6150  fmpoco  6217  tpostpos  6265  tfr0  6324  rdgival  6383  frec0g  6398  2oconcl  6440  om0  6459  oei0  6460  oasuc  6465  omv2  6466  nnm0r  6480  uniqs2  6595  en1  6799  en1bg  6800  fundmen  6806  mapsnen  6811  xpsnen  6821  xpcomco  6826  xpdom2  6831  xpmapenlem  6849  exmidpweq  6909  unsnfidcex  6919  fiintim  6928  ssfirab  6933  sbthlemi8  6963  elfi2  6971  fi0  6974  fieq0  6975  djudom  7092  ismkvnex  7153  nninfwlpoimlemg  7173  en2other2  7195  exmidfodomrlemim  7200  nq0m0r  7455  addpinq1  7463  genipv  7508  genpelvl  7511  genpelvu  7512  cauappcvgprlem1  7658  caucvgsrlemoffres  7799  addresr  7836  mulresr  7837  axcnre  7880  add20  8431  rimul  8542  rereim  8543  mulreim  8561  sup3exmid  8914  fv0p1e1  9034  div4p1lem1div2  9172  nnm1nn0  9217  znegcl  9284  peano2z  9289  nneoor  9355  nn0ind-raph  9370  xnegneg  9833  xltnegi  9835  xaddpnf1  9846  xnegid  9859  xnn0xadd0  9867  xnegdi  9868  xsubge0  9881  xposdif  9882  xlesubadd  9883  xleaddadd  9887  fz0to4untppr  10124  fzo0to2pr  10218  fldiv4p1lem1div2  10305  mulp1mod1  10365  frecfzennn  10426  iseqf1olemqk  10494  exp0  10524  expp1  10527  expnegap0  10528  1exp  10549  mulexp  10559  m1expeven  10567  sq0i  10612  bernneq  10641  facp1  10710  faclbnd3  10723  facubnd  10725  bcval5  10743  hashinfom  10758  hashsng  10778  hashxp  10806  resunimafz0  10811  zfz1iso  10821  imre  10860  reim0b  10871  rereb  10872  resqrexlemover  11019  resqrexlemcalc1  11023  abs00bd  11075  maxabslemlub  11216  xrmaxiflemcom  11257  xrmaxadd  11269  climconst  11298  isumz  11397  fsumf1o  11398  fsumcllem  11407  fsumadd  11414  fsumxp  11444  fsumcnv  11445  fsummulc2  11456  fsumconst  11462  fsumabs  11473  telfsumo  11474  fsumparts  11478  fsumrelem  11479  fsumiun  11485  binomlem  11491  binom  11492  binom11  11494  isumsplit  11499  arisum  11506  arisum2  11507  trireciplem  11508  georeclim  11521  cvgratnnlemseq  11534  prodfrecap  11554  prod1dc  11594  fprodf1o  11596  fprodcl2lem  11613  fprodcllem  11614  fprodfac  11623  fprod2d  11631  fprodxp  11632  fprodcnv  11633  fprodrec  11637  fprodmodd  11649  ef0lem  11668  ege2le3  11679  efaddlem  11682  efcan  11684  eft0val  11701  ef4p  11702  efgt1p2  11703  efi4p  11725  sincossq  11756  cos2tsin  11759  absefi  11776  demoivreALT  11781  p1modz1  11801  dvdsabseq  11853  odd2np1lem  11877  oddp1even  11881  opoe  11900  m1expo  11905  m1exp1  11906  nn0o1gt2  11910  nninfdcex  11954  gcddvds  11964  gcdcl  11967  gcdeq0  11978  gcd0id  11980  bezoutr1  12034  nnmindc  12035  nnminle  12036  eucalg  12059  lcm0val  12065  lcmid  12080  rpmul  12098  dfphi2  12220  phiprmpw  12222  hashgcdeq  12239  odzdvds  12245  nnnn0modprm0  12255  pythagtriplem4  12268  pythagtriplem12  12275  pcaddlem  12338  pcmpt  12341  pockthi  12356  ennnfonelem0  12406  ennnfonelem1  12408  ennnfonelemhdmp1  12410  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemf1  12419  ctiunctlemfo  12440  setsresg  12500  strressid  12530  strle1g  12565  restid2  12697  grplactcnv  12972  mulg0  12988  mulgneg  13001  mulgneg2  13017  tgval2  13554  tgidm  13577  epttop  13593  tgrest  13672  restco  13677  restsn  13683  tgcn  13711  cnptopresti  13741  cnptoprest  13742  txbas  13761  upxp  13775  txrest  13779  txdis  13780  txhmeo  13822  txswaphmeolem  13823  xblss2ps  13907  xblss2  13908  qtopbasss  14024  fsumcncntop  14059  limcimolemlt  14136  dvcnp2cntop  14166  dvcoapbr  14174  dvexp  14178  dvexp2  14179  dveflem  14190  dvef  14191  sin0pilem1  14205  sin2kpi  14235  cos2kpi  14236  coseq0q4123  14258  coseq0negpitopi  14260  sincosq1eq  14263  sinkpi  14271  coskpi  14272  1cxp  14324  lgslem2  14405  lgsfcl2  14410  lgs0  14417  lgs2  14421  lgsneg  14428  lgsdilem  14431  lgsdir2lem4  14435  lgsdir2lem5  14436  lgsne0  14442  lgssq  14444  lgssq2  14445  lgseisenlem1  14453  m1lgs  14455  2lgsoddprmlem3  14462  2sqlem9  14474  2sqlem10  14475  ex-ceil  14481  bj-intexr  14663  peano3nninf  14759  nninfall  14761  isomninnlem  14781  iswomni0  14802  ismkvnnlem  14803  nconstwlpolem0  14813