Theorem eqtrdi 2203

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

Syntax hints:   -> wi 4   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1487  ax-17 1503  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-cleq 2147

This theorem is referenced by:  eqtr2di  2204  eqtr4di  2205  3eqtr3g  2210  3eqtr4a  2213  cbvralcsf  3089  cbvrexcsf  3090  cbvreucsf  3091  cbvrabcsf  3092  csbprc  3435  un00  3436  disjssun  3453  disjpr2  3619  tppreq3  3658  diftpsn3  3693  preq12b  3729  intsng  3837  uniintsnr  3839  rint0  3842  riin0  3916  iununir  3928  intexr  4107  sucprc  4367  op1stbg  4433  elreldm  4805  xpeq0r  5001  xpdisj1  5003  xpdisj2  5004  resdisj  5007  xpima1  5025  xpima2m  5026  elxp4  5066  unixp0im  5115  uniabio  5138  iotass  5145  cnvresid  5237  funimacnv  5239  f1o00  5442  dffv4g  5458  fnrnfv  5508  feqresmpt  5515  dffn5imf  5516  funfvdm2f  5526  fvun1  5527  fvmpt2  5544  fndmin  5567  fmptcof  5627  fmptcos  5628  fvunsng  5654  fvpr1  5664  fnrnov  5956  offval  6029  ofrfval  6030  op1std  6086  op2ndd  6087  fmpoco  6153  tpostpos  6201  tfr0  6260  rdgival  6319  frec0g  6334  2oconcl  6376  om0  6394  oei0  6395  oasuc  6400  omv2  6401  nnm0r  6415  uniqs2  6529  en1  6733  en1bg  6734  fundmen  6740  mapsnen  6745  xpsnen  6755  xpcomco  6760  xpdom2  6765  xpmapenlem  6783  exmidpweq  6843  unsnfidcex  6853  fiintim  6862  ssfirab  6867  sbthlemi8  6897  elfi2  6905  fi0  6908  fieq0  6909  djudom  7023  ismkvnex  7077  en2other2  7110  exmidfodomrlemim  7115  nq0m0r  7355  addpinq1  7363  genipv  7408  genpelvl  7411  genpelvu  7412  cauappcvgprlem1  7558  caucvgsrlemoffres  7699  addresr  7736  mulresr  7737  axcnre  7780  add20  8328  rimul  8439  rereim  8440  mulreim  8458  sup3exmid  8807  fv0p1e1  8927  div4p1lem1div2  9065  nnm1nn0  9110  znegcl  9177  peano2z  9182  nneoor  9245  nn0ind-raph  9260  xnegneg  9715  xltnegi  9717  xaddpnf1  9728  xnegid  9741  xnn0xadd0  9749  xnegdi  9750  xsubge0  9763  xposdif  9764  xlesubadd  9765  xleaddadd  9769  fzo0to2pr  10095  fldiv4p1lem1div2  10182  mulp1mod1  10242  frecfzennn  10303  iseqf1olemqk  10371  exp0  10401  expp1  10404  expnegap0  10405  1exp  10426  mulexp  10436  m1expeven  10444  sq0i  10488  bernneq  10516  facp1  10581  faclbnd3  10594  facubnd  10596  bcval5  10614  hashinfom  10629  hashsng  10649  hashxp  10677  resunimafz0  10679  zfz1iso  10689  imre  10728  reim0b  10739  rereb  10740  resqrexlemover  10887  resqrexlemcalc1  10891  abs00bd  10943  maxabslemlub  11084  xrmaxiflemcom  11123  xrmaxadd  11135  climconst  11164  isumz  11263  fsumf1o  11264  fsumcllem  11273  fsumadd  11280  fsumxp  11310  fsumcnv  11311  fsummulc2  11322  fsumconst  11328  fsumabs  11339  telfsumo  11340  fsumparts  11344  fsumrelem  11345  fsumiun  11351  binomlem  11357  binom  11358  binom11  11360  isumsplit  11365  arisum  11372  arisum2  11373  trireciplem  11374  georeclim  11387  cvgratnnlemseq  11400  prodfrecap  11420  prod1dc  11460  fprodf1o  11462  fprodcl2lem  11479  fprodcllem  11480  fprodfac  11489  fprod2d  11497  fprodxp  11498  fprodcnv  11499  fprodrec  11503  fprodmodd  11515  ef0lem  11534  ege2le3  11545  efaddlem  11548  efcan  11550  eft0val  11567  ef4p  11568  efgt1p2  11569  efi4p  11591  sincossq  11622  cos2tsin  11625  absefi  11642  demoivreALT  11647  dvdsabseq  11712  odd2np1lem  11736  oddp1even  11740  opoe  11759  m1expo  11764  m1exp1  11765  nn0o1gt2  11769  gcddvds  11819  gcdcl  11822  gcdeq0  11832  gcd0id  11834  bezoutr1  11888  eucalg  11907  lcm0val  11913  lcmid  11928  rpmul  11946  dfphi2  12063  phiprmpw  12065  hashgcdeq  12071  ennnfonelem0  12085  ennnfonelem1  12087  ennnfonelemhdmp1  12089  ennnfonelemkh  12092  ennnfonelemhf1o  12093  ennnfonelemf1  12098  ctiunctlemfo  12119  setsresg  12167  strle1g  12219  restid2  12299  tgval2  12390  tgidm  12413  epttop  12429  tgrest  12508  restco  12513  restsn  12519  tgcn  12547  cnptopresti  12577  cnptoprest  12578  txbas  12597  upxp  12611  txrest  12615  txdis  12616  txhmeo  12658  txswaphmeolem  12659  xblss2ps  12743  xblss2  12744  qtopbasss  12860  fsumcncntop  12895  limcimolemlt  12972  dvcnp2cntop  13002  dvcoapbr  13010  dvexp  13014  dvexp2  13015  dveflem  13026  dvef  13027  sin0pilem1  13041  sin2kpi  13071  cos2kpi  13072  coseq0q4123  13094  coseq0negpitopi  13096  sincosq1eq  13099  sinkpi  13107  coskpi  13108  1cxp  13160  ex-ceil  13240  bj-intexr  13421  exmid1stab  13511  peano3nninf  13519  nninfall  13522  isomninnlem  13542  iswomni0  13563  ismkvnnlem  13564  nconstwlpolem0  13574