Theorem eqtrdi 2287

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

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqtr2di  2288  eqtr4di  2289  3eqtr3g  2294  3eqtr4a  2297  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  un00  3567  vvin  3569  csbprc  3572  disjssun  3588  disjpr2  3772  tppreq3  3813  diftpsn3  3854  ssprsseq  3875  preq12b  3893  intsng  4002  uniintsnr  4004  rint0  4007  riin0  4082  iununir  4094  intexr  4284  exmid1stab  4343  sucprc  4555  op1stbg  4623  elreldm  5006  xpeq0r  5208  xpdisj1  5210  xpdisj2  5211  resdisj  5214  xpima1  5232  xpima2m  5233  elxp4  5273  unixp0im  5322  uniabio  5346  iotass  5353  cnvresid  5453  funimacnv  5455  fresaunres2disj  5568  fimadmfo  5622  f1o00  5674  dffv4g  5690  fv2prc  5732  fnrnfv  5746  feqresmpt  5754  dffn5imf  5755  funfvdm2f  5765  fvun1  5766  fvmpt2  5786  fndmin  5810  fmptcof  5869  fmptcos  5870  funopdmsn  5889  fvunsng  5903  fvpr1  5913  dfimafnf  5948  fnrnov  6228  f1o3d  6291  offval  6303  ofrfval  6304  op1std  6375  op2ndd  6376  fmpoco  6445  suppsnopdc  6483  mptsuppdifd  6488  supp0cosupp0fn  6500  tpostpos  6528  tfr0  6587  rdgival  6646  frec0g  6661  2oconcl  6705  om0  6724  oei0  6725  oasuc  6730  omv2  6731  nnm0r  6745  uniqs2  6862  en1  7079  en1bg  7080  fundmen  7087  mapsnen  7093  en2  7105  xpsnen  7112  xpcomco  7117  xpdom2  7122  xpmapenlem  7142  exmidpweq  7209  unsnfidcex  7220  fiintim  7231  ssfirab  7237  sbthlemi8  7274  elfi2  7299  fi0  7302  fieq0  7303  djudom  7426  ismkvnex  7488  nninfwlpoimlemg  7508  en2other2  7541  exmidfodomrlemim  7546  nq0m0r  7816  addpinq1  7824  genipv  7869  genpelvl  7872  genpelvu  7873  cauappcvgprlem1  8019  caucvgsrlemoffres  8160  addresr  8197  mulresr  8198  axcnre  8241  add20  8795  rimul  8906  rereim  8907  mulreim  8925  sup3exmid  9280  fv0p1e1  9401  div4p1lem1div2  9541  nnm1nn0  9586  znegcl  9657  peano2z  9662  nneoor  9730  nn0ind-raph  9745  xnegneg  10217  xltnegi  10219  xaddpnf1  10230  xnegid  10243  xnn0xadd0  10251  xnegdi  10252  xsubge0  10265  xposdif  10266  xlesubadd  10267  xleaddadd  10271  fz0to4untppr  10512  fzo0to2pr  10617  nninfdcex  10653  fldiv4p1lem1div2  10721  fldiv4lem1div2  10723  mulp1mod1  10783  frecfzennn  10844  iseqf1olemqk  10925  exp0  10961  expp1  10964  expnegap0  10965  1exp  10986  mulexp  10996  m1expeven  11004  sq0i  11049  bernneq  11079  facp1  11149  faclbnd3  11162  facubnd  11164  bcval5  11182  hashinfom  11198  hashsng  11218  hashxp  11248  hashpwfi  11250  resunimafz0  11255  ssenneg  11261  hashfibclem  11263  hashfibc  11264  hashf1lem2  11267  hashf1  11268  zfz1iso  11274  hash2en  11276  hashtpgim  11278  lsw1  11335  s1rn  11367  eqs1  11377  ccat1st1st  11390  swrd00g  11402  swrdlend  11411  swrds1  11421  cats1lend  11520  cats2catd  11522  s2leng  11542  s2dmg  11543  imre  11597  reim0b  11608  rereb  11609  sq01  11641  resqrexlemover  11757  resqrexlemcalc1  11761  abs00bd  11813  maxabslemlub  11954  xrmaxiflemcom  11996  xrmaxadd  12008  climconst  12037  fzf1o  12123  isumz  12137  fsumf1o  12138  fsumcllem  12147  fsumadd  12154  fsumxp  12184  fsumcnv  12185  fsummulc2  12196  fsumconst  12202  fsumabs  12213  telfsumo  12214  fsumparts  12218  fsumrelem  12219  fsumiun  12225  binomlem  12231  binom  12232  binom11  12234  isumsplit  12239  arisum  12246  arisum2  12247  trireciplem  12248  georeclim  12261  cvgratnnlemseq  12274  prodfrecap  12294  prod1dc  12334  fprodf1o  12336  fprodcl2lem  12353  fprodcllem  12354  fprodfac  12363  fprod2d  12371  fprodxp  12372  fprodcnv  12373  fprodrec  12377  fprodmodd  12389  ef0lem  12408  ege2le3  12419  efaddlem  12422  efcan  12424  eft0val  12441  ef4p  12442  efgt1p2  12443  efi4p  12465  sincossq  12496  cos2tsin  12499  absefi  12517  demoivreALT  12522  p1modz1  12542  dvdsabseq  12595  odd2np1lem  12620  oddp1even  12624  opoe  12643  m1expo  12648  m1exp1  12649  nn0o1gt2  12653  bitsinv1  12710  gcddvds  12721  gcdcl  12724  gcdeq0  12735  gcd0id  12737  bezoutr1  12791  nnmindc  12792  nnminle  12793  eucalg  12818  lcm0val  12824  lcmid  12839  rpmul  12857  dfphi2  12979  phiprmpw  12981  hashgcdeq  12999  odzdvds  13005  nnnn0modprm0  13015  pythagtriplem4  13028  pythagtriplem12  13035  pcaddlem  13099  pcmpt  13103  pockthi  13118  4sqlem12  13162  2expltfac  13199  ballotfilemfp1  13212  ballotfilemfval0  13216  ballotfilemsv  13234  ennnfonelem0  13277  ennnfonelem1  13279  ennnfonelemhdmp1  13281  ennnfonelemkh  13284  ennnfonelemhf1o  13285  ennnfonelemf1  13290  ctiunctlemfo  13311  setsresg  13371  strressid  13405  strle1g  13440  restid2  13582  gzsumwmhm  13783  grplactcnv  13887  mulg0  13908  mulgnn0gzsum  13911  mulgneg  13923  mulgneg2  13939  gzsumconst  14123  gzsumsnfd  14127  gzsumsplit0  14128  gsumvalfi  14132  gsumsncmn  14136  gsump1  14137  gsummptfidmadd  14141  gsummhmfi  14144  prdsbas3  14167  zrhval2  14929  mpl0fi  15019  tgval2  15078  tgidm  15101  epttop  15117  tgrest  15196  restco  15201  restsn  15207  tgcn  15235  cnptopresti  15265  cnptoprest  15266  txbas  15285  upxp  15299  txrest  15303  txdis  15304  txhmeo  15346  txswaphmeolem  15347  xblss2ps  15431  xblss2  15432  qtopbasss  15548  fsumcncntop  15594  hoverb  15675  limcimolemlt  15691  dvcnp2cntop  15726  dvcoapbr  15734  dvexp  15738  dvexp2  15739  dvmptid  15743  dveflem  15753  dvef  15754  plymullem1  15775  plyadd  15778  plymul  15779  plycoeid3  15784  plycjlemc  15787  plycj  15788  sin0pilem1  15808  sin2kpi  15838  cos2kpi  15839  coseq0q4123  15861  coseq0negpitopi  15863  sincosq1eq  15866  sinkpi  15874  coskpi  15875  logfac  15921  1cxp  15928  mpodvdsmulf1o  16021  lgslem2  16037  lgsfcl2  16042  lgs0  16049  lgs2  16053  lgsneg  16060  lgsdilem  16063  lgsdir2lem4  16067  lgsdir2lem5  16068  lgsne0  16074  lgssq  16076  lgssq2  16077  gausslemma2dlem3  16099  gausslemma2dlem4  16100  lgseisenlem1  16106  lgsquadlem2  16114  lgsquad2lem2  16118  lgsquad3  16120  m1lgs  16121  2lgslem1a2  16123  2lgsoddprmlem3  16147  2sqlem9  16160  2sqlem10  16161  edgiedgbg  16223  isuhgrm  16229  isushgrm  16230  uhgr0vb  16242  uhgrun  16244  isupgren  16253  isumgren  16263  umgrnloop0  16275  upgrun  16284  umgrun  16286  isuspgren  16315  isusgren  16316  usgrf1oedg  16363  usgredg3  16372  egrsubgr  16421  0uhgrsubgr  16423  uhgrspansubgrlem  16434  vtxdg0v  16452  vtxdgfi0e  16453  vtxdfifiun  16455  vtxdumgrfival  16456  1loopgrvd2fi  16463  vdegp1cid  16474  wlkl1loop  16516  2wlklem  16534  upgr2wlkdc  16535  clwwlkn0  16566  clwwlkn1  16576  clwwlkn2  16579  umgr2cwwk2dif  16582  clwwlk0on0  16589  clwwlknonel  16590  clwwlknonex2lem1  16595  trlsegvdeglem4  16621  eupthvdres  16633  eupth2lembfi  16635  konigsberglem1  16646  konigsberglem2  16647  konigsberglem3  16648  ex-ceil  16657  bj-intexr  16851  peano3nninf  16958  nninfall  16960  isomninnlem  16987  iswomni0  17009  ismkvnnlem  17010  nconstwlpolem0  17021