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  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  csbprc  3468  un00  3469  disjssun  3486  disjpr2  3656  tppreq3  3695  diftpsn3  3733  preq12b  3770  intsng  3878  uniintsnr  3880  rint0  3883  riin0  3958  iununir  3970  intexr  4150  exmid1stab  4208  sucprc  4412  op1stbg  4479  elreldm  4853  xpeq0r  5051  xpdisj1  5053  xpdisj2  5054  resdisj  5057  xpima1  5075  xpima2m  5076  elxp4  5116  unixp0im  5165  uniabio  5188  iotass  5195  cnvresid  5290  funimacnv  5292  f1o00  5496  dffv4g  5512  fnrnfv  5562  feqresmpt  5570  dffn5imf  5571  funfvdm2f  5581  fvun1  5582  fvmpt2  5599  fndmin  5623  fmptcof  5683  fmptcos  5684  fvunsng  5710  fvpr1  5720  fnrnov  6019  offval  6089  ofrfval  6090  op1std  6148  op2ndd  6149  fmpoco  6216  tpostpos  6264  tfr0  6323  rdgival  6382  frec0g  6397  2oconcl  6439  om0  6458  oei0  6459  oasuc  6464  omv2  6465  nnm0r  6479  uniqs2  6594  en1  6798  en1bg  6799  fundmen  6805  mapsnen  6810  xpsnen  6820  xpcomco  6825  xpdom2  6830  xpmapenlem  6848  exmidpweq  6908  unsnfidcex  6918  fiintim  6927  ssfirab  6932  sbthlemi8  6962  elfi2  6970  fi0  6973  fieq0  6974  djudom  7091  ismkvnex  7152  nninfwlpoimlemg  7172  en2other2  7194  exmidfodomrlemim  7199  nq0m0r  7454  addpinq1  7462  genipv  7507  genpelvl  7510  genpelvu  7511  cauappcvgprlem1  7657  caucvgsrlemoffres  7798  addresr  7835  mulresr  7836  axcnre  7879  add20  8430  rimul  8541  rereim  8542  mulreim  8560  sup3exmid  8913  fv0p1e1  9033  div4p1lem1div2  9171  nnm1nn0  9216  znegcl  9283  peano2z  9288  nneoor  9354  nn0ind-raph  9369  xnegneg  9832  xltnegi  9834  xaddpnf1  9845  xnegid  9858  xnn0xadd0  9866  xnegdi  9867  xsubge0  9880  xposdif  9881  xlesubadd  9882  xleaddadd  9886  fz0to4untppr  10123  fzo0to2pr  10217  fldiv4p1lem1div2  10304  mulp1mod1  10364  frecfzennn  10425  iseqf1olemqk  10493  exp0  10523  expp1  10526  expnegap0  10527  1exp  10548  mulexp  10558  m1expeven  10566  sq0i  10611  bernneq  10640  facp1  10709  faclbnd3  10722  facubnd  10724  bcval5  10742  hashinfom  10757  hashsng  10777  hashxp  10805  resunimafz0  10810  zfz1iso  10820  imre  10859  reim0b  10870  rereb  10871  resqrexlemover  11018  resqrexlemcalc1  11022  abs00bd  11074  maxabslemlub  11215  xrmaxiflemcom  11256  xrmaxadd  11268  climconst  11297  isumz  11396  fsumf1o  11397  fsumcllem  11406  fsumadd  11413  fsumxp  11443  fsumcnv  11444  fsummulc2  11455  fsumconst  11461  fsumabs  11472  telfsumo  11473  fsumparts  11477  fsumrelem  11478  fsumiun  11484  binomlem  11490  binom  11491  binom11  11493  isumsplit  11498  arisum  11505  arisum2  11506  trireciplem  11507  georeclim  11520  cvgratnnlemseq  11533  prodfrecap  11553  prod1dc  11593  fprodf1o  11595  fprodcl2lem  11612  fprodcllem  11613  fprodfac  11622  fprod2d  11630  fprodxp  11631  fprodcnv  11632  fprodrec  11636  fprodmodd  11648  ef0lem  11667  ege2le3  11678  efaddlem  11681  efcan  11683  eft0val  11700  ef4p  11701  efgt1p2  11702  efi4p  11724  sincossq  11755  cos2tsin  11758  absefi  11775  demoivreALT  11780  p1modz1  11800  dvdsabseq  11852  odd2np1lem  11876  oddp1even  11880  opoe  11899  m1expo  11904  m1exp1  11905  nn0o1gt2  11909  nninfdcex  11953  gcddvds  11963  gcdcl  11966  gcdeq0  11977  gcd0id  11979  bezoutr1  12033  nnmindc  12034  nnminle  12035  eucalg  12058  lcm0val  12064  lcmid  12079  rpmul  12097  dfphi2  12219  phiprmpw  12221  hashgcdeq  12238  odzdvds  12244  nnnn0modprm0  12254  pythagtriplem4  12267  pythagtriplem12  12274  pcaddlem  12337  pcmpt  12340  pockthi  12355  ennnfonelem0  12405  ennnfonelem1  12407  ennnfonelemhdmp1  12409  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ennnfonelemf1  12418  ctiunctlemfo  12439  setsresg  12499  strressid  12529  strle1g  12564  restid2  12696  grplactcnv  12971  mulg0  12987  mulgneg  13000  mulgneg2  13015  tgval2  13521  tgidm  13544  epttop  13560  tgrest  13639  restco  13644  restsn  13650  tgcn  13678  cnptopresti  13708  cnptoprest  13709  txbas  13728  upxp  13742  txrest  13746  txdis  13747  txhmeo  13789  txswaphmeolem  13790  xblss2ps  13874  xblss2  13875  qtopbasss  13991  fsumcncntop  14026  limcimolemlt  14103  dvcnp2cntop  14133  dvcoapbr  14141  dvexp  14145  dvexp2  14146  dveflem  14157  dvef  14158  sin0pilem1  14172  sin2kpi  14202  cos2kpi  14203  coseq0q4123  14225  coseq0negpitopi  14227  sincosq1eq  14230  sinkpi  14238  coskpi  14239  1cxp  14291  lgslem2  14372  lgsfcl2  14377  lgs0  14384  lgs2  14388  lgsneg  14395  lgsdilem  14398  lgsdir2lem4  14402  lgsdir2lem5  14403  lgsne0  14409  lgssq  14411  lgssq2  14412  lgseisenlem1  14420  m1lgs  14422  2lgsoddprmlem3  14429  2sqlem9  14441  2sqlem10  14442  ex-ceil  14448  bj-intexr  14630  peano3nninf  14726  nninfall  14728  isomninnlem  14748  iswomni0  14769  ismkvnnlem  14770  nconstwlpolem0  14780