Theorem eqtrdi 2236

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

Syntax hints:   -> wi 4   = wceq 1363

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 1457  ax-gen 1459  ax-4 1520  ax-17 1536  ax-ext 2169

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

This theorem is referenced by:  eqtr2di  2237  eqtr4di  2238  3eqtr3g  2243  3eqtr4a  2246  cbvralcsf  3131  cbvrexcsf  3132  cbvreucsf  3133  cbvrabcsf  3134  csbprc  3480  un00  3481  disjssun  3498  disjpr2  3668  tppreq3  3707  diftpsn3  3745  preq12b  3782  intsng  3890  uniintsnr  3892  rint0  3895  riin0  3970  iununir  3982  intexr  4162  exmid1stab  4220  sucprc  4424  op1stbg  4491  elreldm  4865  xpeq0r  5063  xpdisj1  5065  xpdisj2  5066  resdisj  5069  xpima1  5087  xpima2m  5088  elxp4  5128  unixp0im  5177  uniabio  5200  iotass  5207  cnvresid  5302  funimacnv  5304  f1o00  5508  dffv4g  5524  fv2prc  5563  fnrnfv  5575  feqresmpt  5583  dffn5imf  5584  funfvdm2f  5594  fvun1  5595  fvmpt2  5612  fndmin  5636  fmptcof  5696  fmptcos  5697  fvunsng  5723  fvpr1  5733  fnrnov  6034  offval  6104  ofrfval  6105  op1std  6163  op2ndd  6164  fmpoco  6231  tpostpos  6279  tfr0  6338  rdgival  6397  frec0g  6412  2oconcl  6454  om0  6473  oei0  6474  oasuc  6479  omv2  6480  nnm0r  6494  uniqs2  6609  en1  6813  en1bg  6814  fundmen  6820  mapsnen  6825  xpsnen  6835  xpcomco  6840  xpdom2  6845  xpmapenlem  6863  exmidpweq  6923  unsnfidcex  6933  fiintim  6942  ssfirab  6947  sbthlemi8  6977  elfi2  6985  fi0  6988  fieq0  6989  djudom  7106  ismkvnex  7167  nninfwlpoimlemg  7187  en2other2  7209  exmidfodomrlemim  7214  nq0m0r  7469  addpinq1  7477  genipv  7522  genpelvl  7525  genpelvu  7526  cauappcvgprlem1  7672  caucvgsrlemoffres  7813  addresr  7850  mulresr  7851  axcnre  7894  add20  8445  rimul  8556  rereim  8557  mulreim  8575  sup3exmid  8928  fv0p1e1  9048  div4p1lem1div2  9186  nnm1nn0  9231  znegcl  9298  peano2z  9303  nneoor  9369  nn0ind-raph  9384  xnegneg  9847  xltnegi  9849  xaddpnf1  9860  xnegid  9873  xnn0xadd0  9881  xnegdi  9882  xsubge0  9895  xposdif  9896  xlesubadd  9897  xleaddadd  9901  fz0to4untppr  10138  fzo0to2pr  10232  fldiv4p1lem1div2  10319  mulp1mod1  10379  frecfzennn  10440  iseqf1olemqk  10508  exp0  10538  expp1  10541  expnegap0  10542  1exp  10563  mulexp  10573  m1expeven  10581  sq0i  10626  bernneq  10655  facp1  10724  faclbnd3  10737  facubnd  10739  bcval5  10757  hashinfom  10772  hashsng  10792  hashxp  10820  resunimafz0  10825  zfz1iso  10835  imre  10874  reim0b  10885  rereb  10886  resqrexlemover  11033  resqrexlemcalc1  11037  abs00bd  11089  maxabslemlub  11230  xrmaxiflemcom  11271  xrmaxadd  11283  climconst  11312  isumz  11411  fsumf1o  11412  fsumcllem  11421  fsumadd  11428  fsumxp  11458  fsumcnv  11459  fsummulc2  11470  fsumconst  11476  fsumabs  11487  telfsumo  11488  fsumparts  11492  fsumrelem  11493  fsumiun  11499  binomlem  11505  binom  11506  binom11  11508  isumsplit  11513  arisum  11520  arisum2  11521  trireciplem  11522  georeclim  11535  cvgratnnlemseq  11548  prodfrecap  11568  prod1dc  11608  fprodf1o  11610  fprodcl2lem  11627  fprodcllem  11628  fprodfac  11637  fprod2d  11645  fprodxp  11646  fprodcnv  11647  fprodrec  11651  fprodmodd  11663  ef0lem  11682  ege2le3  11693  efaddlem  11696  efcan  11698  eft0val  11715  ef4p  11716  efgt1p2  11717  efi4p  11739  sincossq  11770  cos2tsin  11773  absefi  11790  demoivreALT  11795  p1modz1  11815  dvdsabseq  11867  odd2np1lem  11891  oddp1even  11895  opoe  11914  m1expo  11919  m1exp1  11920  nn0o1gt2  11924  nninfdcex  11968  gcddvds  11978  gcdcl  11981  gcdeq0  11992  gcd0id  11994  bezoutr1  12048  nnmindc  12049  nnminle  12050  eucalg  12073  lcm0val  12079  lcmid  12094  rpmul  12112  dfphi2  12234  phiprmpw  12236  hashgcdeq  12253  odzdvds  12259  nnnn0modprm0  12269  pythagtriplem4  12282  pythagtriplem12  12289  pcaddlem  12352  pcmpt  12355  pockthi  12370  ennnfonelem0  12420  ennnfonelem1  12422  ennnfonelemhdmp1  12424  ennnfonelemkh  12427  ennnfonelemhf1o  12428  ennnfonelemf1  12433  ctiunctlemfo  12454  setsresg  12514  strressid  12545  strle1g  12580  restid2  12715  grplactcnv  13007  mulg0  13028  mulgneg  13041  mulgneg2  13057  tgval2  13904  tgidm  13927  epttop  13943  tgrest  14022  restco  14027  restsn  14033  tgcn  14061  cnptopresti  14091  cnptoprest  14092  txbas  14111  upxp  14125  txrest  14129  txdis  14130  txhmeo  14172  txswaphmeolem  14173  xblss2ps  14257  xblss2  14258  qtopbasss  14374  fsumcncntop  14409  limcimolemlt  14486  dvcnp2cntop  14516  dvcoapbr  14524  dvexp  14528  dvexp2  14529  dveflem  14540  dvef  14541  sin0pilem1  14555  sin2kpi  14585  cos2kpi  14586  coseq0q4123  14608  coseq0negpitopi  14610  sincosq1eq  14613  sinkpi  14621  coskpi  14622  1cxp  14674  lgslem2  14755  lgsfcl2  14760  lgs0  14767  lgs2  14771  lgsneg  14778  lgsdilem  14781  lgsdir2lem4  14785  lgsdir2lem5  14786  lgsne0  14792  lgssq  14794  lgssq2  14795  lgseisenlem1  14803  m1lgs  14805  2lgsoddprmlem3  14812  2sqlem9  14824  2sqlem10  14825  ex-ceil  14831  bj-intexr  15013  peano3nninf  15110  nninfall  15112  isomninnlem  15132  iswomni0  15153  ismkvnnlem  15154  nconstwlpolem0  15165