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 )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used 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  3773  tppreq3  3814  diftpsn3  3856  ssprsseq  3877  preq12b  3895  intsng  4004  uniintsnr  4006  rint0  4009  riin0  4084  iununir  4096  intexr  4286  exmid1stab  4345  sucprc  4557  op1stbg  4625  elreldm  5008  xpeq0r  5210  xpdisj1  5212  xpdisj2  5213  resdisj  5216  xpima1  5234  xpima2m  5235  elxp4  5275  unixp0im  5324  uniabio  5348  iotass  5355  cnvresid  5455  funimacnv  5457  fresaunres2disj  5570  fimadmfo  5624  f1o00  5676  dffv4g  5692  fv2prc  5735  fnrnfv  5749  feqresmpt  5757  dffn5imf  5758  funfvdm2f  5768  fvun1  5769  fvmpt2  5789  fndmin  5816  fmptcof  5875  fmptcos  5876  funopdmsn  5895  fvunsng  5909  fvpr1  5919  dfimafnf  5955  fnrnov  6235  f1o3d  6298  offval  6310  ofrfval  6311  op1std  6382  op2ndd  6383  fmpoco  6452  suppsnopdc  6490  mptsuppdifd  6495  supp0cosupp0fn  6507  tpostpos  6535  tfr0  6594  rdgival  6653  frec0g  6668  2oconcl  6712  om0  6731  oei0  6732  oasuc  6737  omv2  6738  nnm0r  6752  uniqs2  6869  en1  7086  en1bg  7087  fundmen  7094  mapsnen  7100  en2  7112  xpsnen  7119  xpcomco  7124  xpdom2  7129  xpmapenlem  7149  exmidpweq  7216  unsnfidcex  7227  fiintim  7238  ssfirab  7244  sbthlemi8  7281  elfi2  7306  fi0  7309  fieq0  7310  djudom  7433  ismkvnex  7495  nninfwlpoimlemg  7515  en2other2  7548  exmidfodomrlemim  7553  nq0m0r  7823  addpinq1  7831  genipv  7876  genpelvl  7879  genpelvu  7880  cauappcvgprlem1  8026  caucvgsrlemoffres  8167  addresr  8204  mulresr  8205  axcnre  8248  add20  8803  rimul  8915  rereim  8916  mulreim  8934  sup3exmid  9289  fv0p1e1  9421  div4p1lem1div2  9563  nnm1nn0  9608  znegcl  9679  peano2z  9684  nneoor  9752  nn0ind-raph  9767  xnegneg  10245  xltnegi  10247  xaddpnf1  10258  xnegid  10271  xnn0xadd0  10279  xnegdi  10280  xsubge0  10293  xposdif  10294  xlesubadd  10295  xleaddadd  10299  fz0to4untppr  10541  fzo0to2pr  10646  nninfdcex  10682  fldiv4p1lem1div2  10753  fldiv4lem1div2  10755  mulp1mod1  10815  frecfzennn  10876  iseqf1olemqk  10957  exp0  10993  expp1  10996  expnegap0  10997  1exp  11018  mulexp  11028  m1expeven  11036  sq0i  11081  bernneq  11111  facp1  11182  faclbnd3  11195  facubnd  11197  bcval5  11215  hashinfom  11231  hashsng  11251  hashxp  11281  hashpwfi  11283  resunimafz0  11288  ssenneg  11294  hashfibclem  11296  hashfibc  11297  hashf1lem2  11300  hashf1  11301  zfz1iso  11307  hash2en  11309  hashtpgim  11311  lsw1  11368  s1rn  11400  eqs1  11410  ccat1st1st  11423  swrd00g  11435  swrdlend  11444  swrds1  11454  cats1lend  11553  cats2catd  11555  s2leng  11575  s2dmg  11576  imre  11630  reim0b  11641  rereb  11642  sq01  11674  resqrexlemover  11790  resqrexlemcalc1  11794  abs00bd  11846  maxabslemlub  11988  xrmaxiflemcom  12031  xrmaxadd  12043  climconst  12072  fzf1o  12158  isumz  12172  fsumf1o  12173  fsumcllem  12182  fsumadd  12189  fsumxp  12219  fsumcnv  12220  fsummulc2  12231  fsumconst  12237  fsumabs  12248  telfsumo  12249  fsumparts  12253  fsumrelem  12254  fsumiun  12260  binomlem  12266  binom  12267  binom11  12269  isumsplit  12274  arisum  12281  arisum2  12282  trireciplem  12283  georeclim  12296  cvgratnnlemseq  12309  prodfrecap  12329  prod1dc  12369  fprodf1o  12371  fprodcl2lem  12388  fprodcllem  12389  fprodfac  12398  fprod2d  12406  fprodxp  12407  fprodcnv  12408  fprodrec  12412  fprodmodd  12424  ef0lem  12443  ege2le3  12454  efaddlem  12457  efcan  12459  eft0val  12476  ef4p  12477  efgt1p2  12478  efi4p  12500  sincossq  12531  cos2tsin  12534  absefi  12552  demoivreALT  12557  p1modz1  12577  dvdsabseq  12630  odd2np1lem  12655  oddp1even  12659  opoe  12678  m1expo  12683  m1exp1  12684  nn0o1gt2  12688  bitsinv1  12745  gcddvds  12756  gcdcl  12759  gcdeq0  12770  gcd0id  12772  bezoutr1  12826  nnmindc  12827  nnminle  12828  eucalg  12853  lcm0val  12859  lcmid  12874  rpmul  12892  dfphi2  13018  phiprmpw  13020  hashgcdeq  13038  odzdvds  13044  nnnn0modprm0  13054  pythagtriplem4  13067  pythagtriplem12  13074  pcaddlem  13138  pcmpt  13142  pockthi  13157  4sqlem12  13201  2expltfac  13239  prmlem0  13240  ballotfilemfp1  13280  ballotfilemfval0  13284  ballotfilemsv  13302  ennnfonelem0  13345  ennnfonelem1  13347  ennnfonelemhdmp1  13349  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemf1  13358  ctiunctlemfo  13379  setsresg  13439  strressid  13474  strle1g  13509  restid2  13651  gzsumwmhm  13852  grplactcnv  13956  mulg0  13977  mulgnn0gzsum  13980  mulgneg  13992  mulgneg2  14008  gzsumconst  14192  gzsumsnfd  14196  gzsumsplit0  14197  gsumvalfi  14201  gsumsncmn  14205  gsump1  14206  gsummptfidmadd  14210  gsummhmfi  14213  prdsbas3  14236  zrhval2  15003  assamulgscmlem2  15091  mpl0fi  15142  tgval2  15201  tgidm  15224  epttop  15240  tgrest  15319  restco  15324  restsn  15330  tgcn  15358  cnptopresti  15388  cnptoprest  15389  txbas  15408  upxp  15422  txrest  15426  txdis  15427  txhmeo  15469  txswaphmeolem  15470  xblss2ps  15554  xblss2  15555  qtopbasss  15671  fsumcncntop  15717  hoverb  15798  limcimolemlt  15814  dvcnp2cntop  15849  dvcoapbr  15857  dvexp  15861  dvexp2  15862  dvmptid  15866  dveflem  15876  dvef  15877  plymullem1  15898  plyadd  15901  plymul  15902  plycoeid3  15907  plycjlemc  15910  plycj  15911  sin0pilem1  15932  sin2kpi  15962  cos2kpi  15963  coseq0q4123  15985  coseq0negpitopi  15987  sincosq1eq  15990  sinkpi  15998  coskpi  15999  logfac  16048  1cxp  16055  birthdaylem2  16145  birthdaylem3  16146  ppiprm  16170  ppidif  16175  ppiqltx  16183  mpodvdsmulf1o  16185  bclbnd  16205  bposlem1  16209  bposlem2  16210  bposlem5  16213  lgslem2  16218  lgsfcl2  16223  lgs0  16230  lgs2  16234  lgsneg  16241  lgsdilem  16244  lgsdir2lem4  16248  lgsdir2lem5  16249  lgsne0  16255  lgssq  16257  lgssq2  16258  gausslemma2dlem3  16280  gausslemma2dlem4  16281  lgseisenlem1  16287  lgsquadlem2  16295  lgsquad2lem2  16299  lgsquad3  16301  m1lgs  16302  2lgslem1a2  16304  2lgsoddprmlem3  16328  2sqlem9  16341  2sqlem10  16342  edgiedgbg  16404  isuhgrm  16410  isushgrm  16411  uhgr0vb  16423  uhgrun  16425  isupgren  16434  isumgren  16444  umgrnloop0  16456  upgrun  16465  umgrun  16467  isuspgren  16496  isusgren  16497  usgrf1oedg  16544  usgredg3  16553  egrsubgr  16602  0uhgrsubgr  16604  uhgrspansubgrlem  16615  vtxdg0v  16633  vtxdgfi0e  16634  vtxdfifiun  16636  vtxdumgrfival  16637  1loopgrvd2fi  16644  vdegp1cid  16655  wlkl1loop  16697  2wlklem  16715  upgr2wlkdc  16716  clwwlkn0  16747  clwwlkn1  16757  clwwlkn2  16760  umgr2cwwk2dif  16763  clwwlk0on0  16770  clwwlknonel  16771  clwwlknonex2lem1  16776  trlsegvdeglem4  16802  eupthvdres  16814  eupth2lembfi  16816  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  ex-ceil  16838  bj-intexr  17032  wexmiddiffilem  17141  wexmiddifxylem  17143  peano3nninf  17148  nninfall  17150  isomninnlem  17177  iswomni0  17199  ismkvnnlem  17200  nconstwlpolem0  17211