Theorem eqtrdi 2280

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

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  eqtr2di  2281  eqtr4di  2282  3eqtr3g  2287  3eqtr4a  2290  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  csbprc  3540  un00  3541  disjssun  3558  disjpr2  3733  tppreq3  3774  diftpsn3  3814  ssprsseq  3835  preq12b  3853  intsng  3962  uniintsnr  3964  rint0  3967  riin0  4042  iununir  4054  intexr  4240  exmid1stab  4298  sucprc  4509  op1stbg  4576  elreldm  4958  xpeq0r  5159  xpdisj1  5161  xpdisj2  5162  resdisj  5165  xpima1  5183  xpima2m  5184  elxp4  5224  unixp0im  5273  uniabio  5297  iotass  5304  cnvresid  5404  funimacnv  5406  fimadmfo  5569  f1o00  5621  dffv4g  5637  fv2prc  5679  fnrnfv  5693  feqresmpt  5701  dffn5imf  5702  funfvdm2f  5712  fvun1  5713  fvmpt2  5731  fndmin  5755  fmptcof  5815  fmptcos  5816  funopdmsn  5835  fvunsng  5849  fvpr1  5859  fnrnov  6171  offval  6246  ofrfval  6247  op1std  6314  op2ndd  6315  fmpoco  6384  tpostpos  6433  tfr0  6492  rdgival  6551  frec0g  6566  2oconcl  6610  om0  6629  oei0  6630  oasuc  6635  omv2  6636  nnm0r  6650  uniqs2  6767  en1  6976  en1bg  6977  fundmen  6984  mapsnen  6989  en2  7001  xpsnen  7008  xpcomco  7013  xpdom2  7018  xpmapenlem  7038  exmidpweq  7104  unsnfidcex  7115  fiintim  7126  ssfirab  7132  sbthlemi8  7166  elfi2  7174  fi0  7177  fieq0  7178  djudom  7295  ismkvnex  7357  nninfwlpoimlemg  7377  en2other2  7410  exmidfodomrlemim  7415  nq0m0r  7679  addpinq1  7687  genipv  7732  genpelvl  7735  genpelvu  7736  cauappcvgprlem1  7882  caucvgsrlemoffres  8023  addresr  8060  mulresr  8061  axcnre  8104  add20  8657  rimul  8768  rereim  8769  mulreim  8787  sup3exmid  9140  fv0p1e1  9261  div4p1lem1div2  9401  nnm1nn0  9446  znegcl  9513  peano2z  9518  nneoor  9585  nn0ind-raph  9600  xnegneg  10071  xltnegi  10073  xaddpnf1  10084  xnegid  10097  xnn0xadd0  10105  xnegdi  10106  xsubge0  10119  xposdif  10120  xlesubadd  10121  xleaddadd  10125  fz0to4untppr  10362  fzo0to2pr  10467  nninfdcex  10501  fldiv4p1lem1div2  10569  fldiv4lem1div2  10571  mulp1mod1  10631  frecfzennn  10692  iseqf1olemqk  10773  exp0  10809  expp1  10812  expnegap0  10813  1exp  10834  mulexp  10844  m1expeven  10852  sq0i  10897  bernneq  10926  facp1  10996  faclbnd3  11009  facubnd  11011  bcval5  11029  hashinfom  11044  hashsng  11064  hashxp  11094  resunimafz0  11099  zfz1iso  11109  hash2en  11111  hashtpgim  11113  lsw1  11170  s1rn  11202  eqs1  11212  ccat1st1st  11225  swrd00g  11237  swrdlend  11246  swrds1  11256  cats1lend  11355  cats2catd  11357  s2leng  11377  s2dmg  11378  imre  11432  reim0b  11443  rereb  11444  resqrexlemover  11591  resqrexlemcalc1  11595  abs00bd  11647  maxabslemlub  11788  xrmaxiflemcom  11830  xrmaxadd  11842  climconst  11871  fzf1o  11957  isumz  11971  fsumf1o  11972  fsumcllem  11981  fsumadd  11988  fsumxp  12018  fsumcnv  12019  fsummulc2  12030  fsumconst  12036  fsumabs  12047  telfsumo  12048  fsumparts  12052  fsumrelem  12053  fsumiun  12059  binomlem  12065  binom  12066  binom11  12068  isumsplit  12073  arisum  12080  arisum2  12081  trireciplem  12082  georeclim  12095  cvgratnnlemseq  12108  prodfrecap  12128  prod1dc  12168  fprodf1o  12170  fprodcl2lem  12187  fprodcllem  12188  fprodfac  12197  fprod2d  12205  fprodxp  12206  fprodcnv  12207  fprodrec  12211  fprodmodd  12223  ef0lem  12242  ege2le3  12253  efaddlem  12256  efcan  12258  eft0val  12275  ef4p  12276  efgt1p2  12277  efi4p  12299  sincossq  12330  cos2tsin  12333  absefi  12351  demoivreALT  12356  p1modz1  12376  dvdsabseq  12429  odd2np1lem  12454  oddp1even  12458  opoe  12477  m1expo  12482  m1exp1  12483  nn0o1gt2  12487  bitsinv1  12544  gcddvds  12555  gcdcl  12558  gcdeq0  12569  gcd0id  12571  bezoutr1  12625  nnmindc  12626  nnminle  12627  eucalg  12652  lcm0val  12658  lcmid  12673  rpmul  12691  dfphi2  12813  phiprmpw  12815  hashgcdeq  12833  odzdvds  12839  nnnn0modprm0  12849  pythagtriplem4  12862  pythagtriplem12  12869  pcaddlem  12933  pcmpt  12937  pockthi  12952  4sqlem12  12996  2expltfac  13033  ennnfonelem0  13047  ennnfonelem1  13049  ennnfonelemhdmp1  13051  ennnfonelemkh  13054  ennnfonelemhf1o  13055  ennnfonelemf1  13060  ctiunctlemfo  13081  setsresg  13141  strressid  13175  strle1g  13210  restid2  13352  prdsbas3  13391  gsumwmhm  13602  grplactcnv  13706  mulg0  13733  mulgnn0gsum  13736  mulgneg  13748  mulgneg2  13764  gsumfzconst  13949  gsumfzsnfd  13953  gsumsplit0  13954  gsumfzfsumlem0  14622  zrhval2  14655  mpl0fi  14743  tgval2  14802  tgidm  14825  epttop  14841  tgrest  14920  restco  14925  restsn  14931  tgcn  14959  cnptopresti  14989  cnptoprest  14990  txbas  15009  upxp  15023  txrest  15027  txdis  15028  txhmeo  15070  txswaphmeolem  15071  xblss2ps  15155  xblss2  15156  qtopbasss  15272  fsumcncntop  15318  hoverb  15399  limcimolemlt  15415  dvcnp2cntop  15450  dvcoapbr  15458  dvexp  15462  dvexp2  15463  dvmptid  15467  dveflem  15477  dvef  15478  plymullem1  15499  plyadd  15502  plymul  15503  plycoeid3  15508  plycjlemc  15511  plycj  15512  sin0pilem1  15532  sin2kpi  15562  cos2kpi  15563  coseq0q4123  15585  coseq0negpitopi  15587  sincosq1eq  15590  sinkpi  15598  coskpi  15599  1cxp  15651  mpodvdsmulf1o  15741  lgslem2  15757  lgsfcl2  15762  lgs0  15769  lgs2  15773  lgsneg  15780  lgsdilem  15783  lgsdir2lem4  15787  lgsdir2lem5  15788  lgsne0  15794  lgssq  15796  lgssq2  15797  gausslemma2dlem3  15819  gausslemma2dlem4  15820  lgseisenlem1  15826  lgsquadlem2  15834  lgsquad2lem2  15838  lgsquad3  15840  m1lgs  15841  2lgslem1a2  15843  2lgsoddprmlem3  15867  2sqlem9  15880  2sqlem10  15881  edgiedgbg  15943  isuhgrm  15949  isushgrm  15950  uhgr0vb  15962  uhgrun  15964  isupgren  15973  isumgren  15983  umgrnloop0  15995  upgrun  16004  umgrun  16006  isuspgren  16035  isusgren  16036  usgrf1oedg  16083  usgredg3  16092  egrsubgr  16141  0uhgrsubgr  16143  uhgrspansubgrlem  16154  vtxdg0v  16172  vtxdgfi0e  16173  vtxdfifiun  16175  vtxdumgrfival  16176  1loopgrvd2fi  16183  vdegp1cid  16194  wlkl1loop  16236  2wlklem  16254  upgr2wlkdc  16255  clwwlkn0  16286  clwwlkn1  16296  clwwlkn2  16299  umgr2cwwk2dif  16302  clwwlk0on0  16309  clwwlknonel  16310  clwwlknonex2lem1  16315  trlsegvdeglem4  16341  eupthvdres  16353  eupth2lembfi  16355  konigsberglem1  16366  konigsberglem2  16367  konigsberglem3  16368  ex-ceil  16377  bj-intexr  16562  peano3nninf  16668  nninfall  16670  isomninnlem  16693  iswomni0  16715  ismkvnnlem  16716  nconstwlpolem0  16727  gfsumval  16740  gfsumsn  16745  gfsump1  16746