Theorem eqtrdi 2283

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  eqtr2di  2284  eqtr4di  2285  3eqtr3g  2290  3eqtr4a  2293  cbvralcsf  3203  cbvrexcsf  3204  cbvreucsf  3205  cbvrabcsf  3206  csbprc  3556  un00  3557  disjssun  3574  disjpr2  3755  tppreq3  3796  diftpsn3  3837  ssprsseq  3858  preq12b  3876  intsng  3985  uniintsnr  3987  rint0  3990  riin0  4065  iununir  4077  intexr  4264  exmid1stab  4323  sucprc  4535  op1stbg  4602  elreldm  4985  xpeq0r  5187  xpdisj1  5189  xpdisj2  5190  resdisj  5193  xpima1  5211  xpima2m  5212  elxp4  5252  unixp0im  5301  uniabio  5325  iotass  5332  cnvresid  5432  funimacnv  5434  fresaunres2disj  5547  fimadmfo  5601  f1o00  5653  dffv4g  5669  fv2prc  5711  fnrnfv  5725  feqresmpt  5733  dffn5imf  5734  funfvdm2f  5744  fvun1  5745  fvmpt2  5763  fndmin  5787  fmptcof  5846  fmptcos  5847  funopdmsn  5866  fvunsng  5880  fvpr1  5890  fnrnov  6202  offval  6276  ofrfval  6277  op1std  6344  op2ndd  6345  fmpoco  6414  suppsnopdc  6452  mptsuppdifd  6457  supp0cosupp0fn  6469  tpostpos  6497  tfr0  6556  rdgival  6615  frec0g  6630  2oconcl  6674  om0  6693  oei0  6694  oasuc  6699  omv2  6700  nnm0r  6714  uniqs2  6831  en1  7041  en1bg  7042  fundmen  7049  mapsnen  7055  en2  7067  xpsnen  7074  xpcomco  7079  xpdom2  7084  xpmapenlem  7104  exmidpweq  7171  unsnfidcex  7182  fiintim  7193  ssfirab  7199  sbthlemi8  7236  elfi2  7261  fi0  7264  fieq0  7265  djudom  7386  ismkvnex  7448  nninfwlpoimlemg  7468  en2other2  7501  exmidfodomrlemim  7506  nq0m0r  7773  addpinq1  7781  genipv  7826  genpelvl  7829  genpelvu  7830  cauappcvgprlem1  7976  caucvgsrlemoffres  8117  addresr  8154  mulresr  8155  axcnre  8198  add20  8750  rimul  8861  rereim  8862  mulreim  8880  sup3exmid  9233  fv0p1e1  9354  div4p1lem1div2  9494  nnm1nn0  9539  znegcl  9610  peano2z  9615  nneoor  9683  nn0ind-raph  9698  xnegneg  10169  xltnegi  10171  xaddpnf1  10182  xnegid  10195  xnn0xadd0  10203  xnegdi  10204  xsubge0  10217  xposdif  10218  xlesubadd  10219  xleaddadd  10223  fz0to4untppr  10462  fzo0to2pr  10567  nninfdcex  10601  fldiv4p1lem1div2  10669  fldiv4lem1div2  10671  mulp1mod1  10731  frecfzennn  10792  iseqf1olemqk  10873  exp0  10909  expp1  10912  expnegap0  10913  1exp  10934  mulexp  10944  m1expeven  10952  sq0i  10997  bernneq  11026  facp1  11096  faclbnd3  11109  facubnd  11111  bcval5  11129  hashinfom  11145  hashsng  11165  hashxp  11195  hashpwfi  11197  resunimafz0  11202  ssenneg  11208  hashfibclem  11210  hashfibc  11211  zfz1iso  11217  hash2en  11219  hashtpgim  11221  lsw1  11278  s1rn  11310  eqs1  11320  ccat1st1st  11333  swrd00g  11345  swrdlend  11354  swrds1  11364  cats1lend  11463  cats2catd  11465  s2leng  11485  s2dmg  11486  imre  11540  reim0b  11551  rereb  11552  resqrexlemover  11699  resqrexlemcalc1  11703  abs00bd  11755  maxabslemlub  11896  xrmaxiflemcom  11938  xrmaxadd  11950  climconst  11979  fzf1o  12065  isumz  12079  fsumf1o  12080  fsumcllem  12089  fsumadd  12096  fsumxp  12126  fsumcnv  12127  fsummulc2  12138  fsumconst  12144  fsumabs  12155  telfsumo  12156  fsumparts  12160  fsumrelem  12161  fsumiun  12167  binomlem  12173  binom  12174  binom11  12176  isumsplit  12181  arisum  12188  arisum2  12189  trireciplem  12190  georeclim  12203  cvgratnnlemseq  12216  prodfrecap  12236  prod1dc  12276  fprodf1o  12278  fprodcl2lem  12295  fprodcllem  12296  fprodfac  12305  fprod2d  12313  fprodxp  12314  fprodcnv  12315  fprodrec  12319  fprodmodd  12331  ef0lem  12350  ege2le3  12361  efaddlem  12364  efcan  12366  eft0val  12383  ef4p  12384  efgt1p2  12385  efi4p  12407  sincossq  12438  cos2tsin  12441  absefi  12459  demoivreALT  12464  p1modz1  12484  dvdsabseq  12537  odd2np1lem  12562  oddp1even  12566  opoe  12585  m1expo  12590  m1exp1  12591  nn0o1gt2  12595  bitsinv1  12652  gcddvds  12663  gcdcl  12666  gcdeq0  12677  gcd0id  12679  bezoutr1  12733  nnmindc  12734  nnminle  12735  eucalg  12760  lcm0val  12766  lcmid  12781  rpmul  12799  dfphi2  12921  phiprmpw  12923  hashgcdeq  12941  odzdvds  12947  nnnn0modprm0  12957  pythagtriplem4  12970  pythagtriplem12  12977  pcaddlem  13041  pcmpt  13045  pockthi  13060  4sqlem12  13104  2expltfac  13141  ballotfilemfp1  13152  ballotfilemfval0  13156  ennnfonelem0  13173  ennnfonelem1  13175  ennnfonelemhdmp1  13177  ennnfonelemkh  13180  ennnfonelemhf1o  13181  ennnfonelemf1  13186  ctiunctlemfo  13207  setsresg  13267  strressid  13301  strle1g  13336  restid2  13478  prdsbas3  13517  gsumwmhm  13728  grplactcnv  13832  mulg0  13859  mulgnn0gsum  13862  mulgneg  13874  mulgneg2  13890  gsumfzconst  14075  gsumfzsnfd  14079  gsumsplit0  14080  gsumfzfsumlem0  14751  zrhval2  14784  mpl0fi  14874  tgval2  14933  tgidm  14956  epttop  14972  tgrest  15051  restco  15056  restsn  15062  tgcn  15090  cnptopresti  15120  cnptoprest  15121  txbas  15140  upxp  15154  txrest  15158  txdis  15159  txhmeo  15201  txswaphmeolem  15202  xblss2ps  15286  xblss2  15287  qtopbasss  15403  fsumcncntop  15449  hoverb  15530  limcimolemlt  15546  dvcnp2cntop  15581  dvcoapbr  15589  dvexp  15593  dvexp2  15594  dvmptid  15598  dveflem  15608  dvef  15609  plymullem1  15630  plyadd  15633  plymul  15634  plycoeid3  15639  plycjlemc  15642  plycj  15643  sin0pilem1  15663  sin2kpi  15693  cos2kpi  15694  coseq0q4123  15716  coseq0negpitopi  15718  sincosq1eq  15721  sinkpi  15729  coskpi  15730  1cxp  15782  mpodvdsmulf1o  15875  lgslem2  15891  lgsfcl2  15896  lgs0  15903  lgs2  15907  lgsneg  15914  lgsdilem  15917  lgsdir2lem4  15921  lgsdir2lem5  15922  lgsne0  15928  lgssq  15930  lgssq2  15931  gausslemma2dlem3  15953  gausslemma2dlem4  15954  lgseisenlem1  15960  lgsquadlem2  15968  lgsquad2lem2  15972  lgsquad3  15974  m1lgs  15975  2lgslem1a2  15977  2lgsoddprmlem3  16001  2sqlem9  16014  2sqlem10  16015  edgiedgbg  16077  isuhgrm  16083  isushgrm  16084  uhgr0vb  16096  uhgrun  16098  isupgren  16107  isumgren  16117  umgrnloop0  16129  upgrun  16138  umgrun  16140  isuspgren  16169  isusgren  16170  usgrf1oedg  16217  usgredg3  16226  egrsubgr  16275  0uhgrsubgr  16277  uhgrspansubgrlem  16288  vtxdg0v  16306  vtxdgfi0e  16307  vtxdfifiun  16309  vtxdumgrfival  16310  1loopgrvd2fi  16317  vdegp1cid  16328  wlkl1loop  16370  2wlklem  16388  upgr2wlkdc  16389  clwwlkn0  16420  clwwlkn1  16430  clwwlkn2  16433  umgr2cwwk2dif  16436  clwwlk0on0  16443  clwwlknonel  16444  clwwlknonex2lem1  16449  trlsegvdeglem4  16475  eupthvdres  16487  eupth2lembfi  16489  konigsberglem1  16500  konigsberglem2  16501  konigsberglem3  16502  ex-ceil  16511  bj-intexr  16695  peano3nninf  16802  nninfall  16804  isomninnlem  16831  iswomni0  16853  ismkvnnlem  16854  nconstwlpolem0  16866  gfsumval  16879  gfsumsn  16884  gfsump1  16885