Theorem eqtrdi 2254

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

Syntax hints:   -> wi 4   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  eqtr2di  2255  eqtr4di  2256  3eqtr3g  2261  3eqtr4a  2264  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  csbprc  3506  un00  3507  disjssun  3524  disjpr2  3697  tppreq3  3736  diftpsn3  3774  preq12b  3811  intsng  3919  uniintsnr  3921  rint0  3924  riin0  3999  iununir  4011  intexr  4194  exmid1stab  4252  sucprc  4459  op1stbg  4526  elreldm  4904  xpeq0r  5105  xpdisj1  5107  xpdisj2  5108  resdisj  5111  xpima1  5129  xpima2m  5130  elxp4  5170  unixp0im  5219  uniabio  5242  iotass  5249  cnvresid  5348  funimacnv  5350  fimadmfo  5507  f1o00  5557  dffv4g  5573  fv2prc  5613  fnrnfv  5625  feqresmpt  5633  dffn5imf  5634  funfvdm2f  5644  fvun1  5645  fvmpt2  5663  fndmin  5687  fmptcof  5747  fmptcos  5748  funopdmsn  5764  fvunsng  5778  fvpr1  5788  fnrnov  6092  offval  6166  ofrfval  6167  op1std  6234  op2ndd  6235  fmpoco  6302  tpostpos  6350  tfr0  6409  rdgival  6468  frec0g  6483  2oconcl  6525  om0  6544  oei0  6545  oasuc  6550  omv2  6551  nnm0r  6565  uniqs2  6682  en1  6891  en1bg  6892  fundmen  6898  mapsnen  6903  en2  6912  xpsnen  6916  xpcomco  6921  xpdom2  6926  xpmapenlem  6946  exmidpweq  7006  unsnfidcex  7017  fiintim  7028  ssfirab  7033  sbthlemi8  7066  elfi2  7074  fi0  7077  fieq0  7078  djudom  7195  ismkvnex  7257  nninfwlpoimlemg  7277  en2other2  7304  exmidfodomrlemim  7309  nq0m0r  7569  addpinq1  7577  genipv  7622  genpelvl  7625  genpelvu  7626  cauappcvgprlem1  7772  caucvgsrlemoffres  7913  addresr  7950  mulresr  7951  axcnre  7994  add20  8547  rimul  8658  rereim  8659  mulreim  8677  sup3exmid  9030  fv0p1e1  9151  div4p1lem1div2  9291  nnm1nn0  9336  znegcl  9403  peano2z  9408  nneoor  9475  nn0ind-raph  9490  xnegneg  9955  xltnegi  9957  xaddpnf1  9968  xnegid  9981  xnn0xadd0  9989  xnegdi  9990  xsubge0  10003  xposdif  10004  xlesubadd  10005  xleaddadd  10009  fz0to4untppr  10246  fzo0to2pr  10347  nninfdcex  10380  fldiv4p1lem1div2  10448  fldiv4lem1div2  10450  mulp1mod1  10510  frecfzennn  10571  iseqf1olemqk  10652  exp0  10688  expp1  10691  expnegap0  10692  1exp  10713  mulexp  10723  m1expeven  10731  sq0i  10776  bernneq  10805  facp1  10875  faclbnd3  10888  facubnd  10890  bcval5  10908  hashinfom  10923  hashsng  10943  hashxp  10971  resunimafz0  10976  zfz1iso  10986  hash2en  10988  lsw1  11043  s1rn  11072  eqs1  11082  ccat1st1st  11093  swrd00g  11102  swrdlend  11111  swrds1  11121  imre  11162  reim0b  11173  rereb  11174  resqrexlemover  11321  resqrexlemcalc1  11325  abs00bd  11377  maxabslemlub  11518  xrmaxiflemcom  11560  xrmaxadd  11572  climconst  11601  isumz  11700  fsumf1o  11701  fsumcllem  11710  fsumadd  11717  fsumxp  11747  fsumcnv  11748  fsummulc2  11759  fsumconst  11765  fsumabs  11776  telfsumo  11777  fsumparts  11781  fsumrelem  11782  fsumiun  11788  binomlem  11794  binom  11795  binom11  11797  isumsplit  11802  arisum  11809  arisum2  11810  trireciplem  11811  georeclim  11824  cvgratnnlemseq  11837  prodfrecap  11857  prod1dc  11897  fprodf1o  11899  fprodcl2lem  11916  fprodcllem  11917  fprodfac  11926  fprod2d  11934  fprodxp  11935  fprodcnv  11936  fprodrec  11940  fprodmodd  11952  ef0lem  11971  ege2le3  11982  efaddlem  11985  efcan  11987  eft0val  12004  ef4p  12005  efgt1p2  12006  efi4p  12028  sincossq  12059  cos2tsin  12062  absefi  12080  demoivreALT  12085  p1modz1  12105  dvdsabseq  12158  odd2np1lem  12183  oddp1even  12187  opoe  12206  m1expo  12211  m1exp1  12212  nn0o1gt2  12216  bitsinv1  12273  gcddvds  12284  gcdcl  12287  gcdeq0  12298  gcd0id  12300  bezoutr1  12354  nnmindc  12355  nnminle  12356  eucalg  12381  lcm0val  12387  lcmid  12402  rpmul  12420  dfphi2  12542  phiprmpw  12544  hashgcdeq  12562  odzdvds  12568  nnnn0modprm0  12578  pythagtriplem4  12591  pythagtriplem12  12598  pcaddlem  12662  pcmpt  12666  pockthi  12681  4sqlem12  12725  2expltfac  12762  ennnfonelem0  12776  ennnfonelem1  12778  ennnfonelemhdmp1  12780  ennnfonelemkh  12783  ennnfonelemhf1o  12784  ennnfonelemf1  12789  ctiunctlemfo  12810  setsresg  12870  strressid  12903  strle1g  12938  restid2  13080  prdsbas3  13119  gsumwmhm  13330  grplactcnv  13434  mulg0  13461  mulgnn0gsum  13464  mulgneg  13476  mulgneg2  13492  gsumfzconst  13677  gsumfzsnfd  13681  gsumfzfsumlem0  14348  zrhval2  14381  mpl0fi  14464  tgval2  14523  tgidm  14546  epttop  14562  tgrest  14641  restco  14646  restsn  14652  tgcn  14680  cnptopresti  14710  cnptoprest  14711  txbas  14730  upxp  14744  txrest  14748  txdis  14749  txhmeo  14791  txswaphmeolem  14792  xblss2ps  14876  xblss2  14877  qtopbasss  14993  fsumcncntop  15039  hoverb  15120  limcimolemlt  15136  dvcnp2cntop  15171  dvcoapbr  15179  dvexp  15183  dvexp2  15184  dvmptid  15188  dveflem  15198  dvef  15199  plymullem1  15220  plyadd  15223  plymul  15224  plycoeid3  15229  plycjlemc  15232  plycj  15233  sin0pilem1  15253  sin2kpi  15283  cos2kpi  15284  coseq0q4123  15306  coseq0negpitopi  15308  sincosq1eq  15311  sinkpi  15319  coskpi  15320  1cxp  15372  mpodvdsmulf1o  15462  lgslem2  15478  lgsfcl2  15483  lgs0  15490  lgs2  15494  lgsneg  15501  lgsdilem  15504  lgsdir2lem4  15508  lgsdir2lem5  15509  lgsne0  15515  lgssq  15517  lgssq2  15518  gausslemma2dlem3  15540  gausslemma2dlem4  15541  lgseisenlem1  15547  lgsquadlem2  15555  lgsquad2lem2  15559  lgsquad3  15561  m1lgs  15562  2lgslem1a2  15564  2lgsoddprmlem3  15588  2sqlem9  15601  2sqlem10  15602  ex-ceil  15662  bj-intexr  15844  peano3nninf  15944  nninfall  15946  isomninnlem  15969  iswomni0  15990  ismkvnnlem  15991  nconstwlpolem0  16002