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  5568  f1o00  5620  dffv4g  5636  fv2prc  5678  fnrnfv  5692  feqresmpt  5700  dffn5imf  5701  funfvdm2f  5711  fvun1  5712  fvmpt2  5730  fndmin  5754  fmptcof  5814  fmptcos  5815  funopdmsn  5834  fvunsng  5848  fvpr1  5858  fnrnov  6168  offval  6243  ofrfval  6244  op1std  6311  op2ndd  6312  fmpoco  6381  tpostpos  6430  tfr0  6489  rdgival  6548  frec0g  6563  2oconcl  6607  om0  6626  oei0  6627  oasuc  6632  omv2  6633  nnm0r  6647  uniqs2  6764  en1  6973  en1bg  6974  fundmen  6981  mapsnen  6986  en2  6998  xpsnen  7005  xpcomco  7010  xpdom2  7015  xpmapenlem  7035  exmidpweq  7101  unsnfidcex  7112  fiintim  7123  ssfirab  7129  sbthlemi8  7163  elfi2  7171  fi0  7174  fieq0  7175  djudom  7292  ismkvnex  7354  nninfwlpoimlemg  7374  en2other2  7407  exmidfodomrlemim  7412  nq0m0r  7676  addpinq1  7684  genipv  7729  genpelvl  7732  genpelvu  7733  cauappcvgprlem1  7879  caucvgsrlemoffres  8020  addresr  8057  mulresr  8058  axcnre  8101  add20  8654  rimul  8765  rereim  8766  mulreim  8784  sup3exmid  9137  fv0p1e1  9258  div4p1lem1div2  9398  nnm1nn0  9443  znegcl  9510  peano2z  9515  nneoor  9582  nn0ind-raph  9597  xnegneg  10068  xltnegi  10070  xaddpnf1  10081  xnegid  10094  xnn0xadd0  10102  xnegdi  10103  xsubge0  10116  xposdif  10117  xlesubadd  10118  xleaddadd  10122  fz0to4untppr  10359  fzo0to2pr  10463  nninfdcex  10497  fldiv4p1lem1div2  10565  fldiv4lem1div2  10567  mulp1mod1  10627  frecfzennn  10688  iseqf1olemqk  10769  exp0  10805  expp1  10808  expnegap0  10809  1exp  10830  mulexp  10840  m1expeven  10848  sq0i  10893  bernneq  10922  facp1  10992  faclbnd3  11005  facubnd  11007  bcval5  11025  hashinfom  11040  hashsng  11060  hashxp  11090  resunimafz0  11095  zfz1iso  11105  hash2en  11107  lsw1  11163  s1rn  11195  eqs1  11205  ccat1st1st  11218  swrd00g  11230  swrdlend  11239  swrds1  11249  cats1lend  11348  cats2catd  11350  s2leng  11370  s2dmg  11371  imre  11412  reim0b  11423  rereb  11424  resqrexlemover  11571  resqrexlemcalc1  11575  abs00bd  11627  maxabslemlub  11768  xrmaxiflemcom  11810  xrmaxadd  11822  climconst  11851  fzf1o  11937  isumz  11951  fsumf1o  11952  fsumcllem  11961  fsumadd  11968  fsumxp  11998  fsumcnv  11999  fsummulc2  12010  fsumconst  12016  fsumabs  12027  telfsumo  12028  fsumparts  12032  fsumrelem  12033  fsumiun  12039  binomlem  12045  binom  12046  binom11  12048  isumsplit  12053  arisum  12060  arisum2  12061  trireciplem  12062  georeclim  12075  cvgratnnlemseq  12088  prodfrecap  12108  prod1dc  12148  fprodf1o  12150  fprodcl2lem  12167  fprodcllem  12168  fprodfac  12177  fprod2d  12185  fprodxp  12186  fprodcnv  12187  fprodrec  12191  fprodmodd  12203  ef0lem  12222  ege2le3  12233  efaddlem  12236  efcan  12238  eft0val  12255  ef4p  12256  efgt1p2  12257  efi4p  12279  sincossq  12310  cos2tsin  12313  absefi  12331  demoivreALT  12336  p1modz1  12356  dvdsabseq  12409  odd2np1lem  12434  oddp1even  12438  opoe  12457  m1expo  12462  m1exp1  12463  nn0o1gt2  12467  bitsinv1  12524  gcddvds  12535  gcdcl  12538  gcdeq0  12549  gcd0id  12551  bezoutr1  12605  nnmindc  12606  nnminle  12607  eucalg  12632  lcm0val  12638  lcmid  12653  rpmul  12671  dfphi2  12793  phiprmpw  12795  hashgcdeq  12813  odzdvds  12819  nnnn0modprm0  12829  pythagtriplem4  12842  pythagtriplem12  12849  pcaddlem  12913  pcmpt  12917  pockthi  12932  4sqlem12  12976  2expltfac  13013  ennnfonelem0  13027  ennnfonelem1  13029  ennnfonelemhdmp1  13031  ennnfonelemkh  13034  ennnfonelemhf1o  13035  ennnfonelemf1  13040  ctiunctlemfo  13061  setsresg  13121  strressid  13155  strle1g  13190  restid2  13332  prdsbas3  13371  gsumwmhm  13582  grplactcnv  13686  mulg0  13713  mulgnn0gsum  13716  mulgneg  13728  mulgneg2  13744  gsumfzconst  13929  gsumfzsnfd  13933  gsumsplit0  13934  gsumfzfsumlem0  14602  zrhval2  14635  mpl0fi  14718  tgval2  14777  tgidm  14800  epttop  14816  tgrest  14895  restco  14900  restsn  14906  tgcn  14934  cnptopresti  14964  cnptoprest  14965  txbas  14984  upxp  14998  txrest  15002  txdis  15003  txhmeo  15045  txswaphmeolem  15046  xblss2ps  15130  xblss2  15131  qtopbasss  15247  fsumcncntop  15293  hoverb  15374  limcimolemlt  15390  dvcnp2cntop  15425  dvcoapbr  15433  dvexp  15437  dvexp2  15438  dvmptid  15442  dveflem  15452  dvef  15453  plymullem1  15474  plyadd  15477  plymul  15478  plycoeid3  15483  plycjlemc  15486  plycj  15487  sin0pilem1  15507  sin2kpi  15537  cos2kpi  15538  coseq0q4123  15560  coseq0negpitopi  15562  sincosq1eq  15565  sinkpi  15573  coskpi  15574  1cxp  15626  mpodvdsmulf1o  15716  lgslem2  15732  lgsfcl2  15737  lgs0  15744  lgs2  15748  lgsneg  15755  lgsdilem  15758  lgsdir2lem4  15762  lgsdir2lem5  15763  lgsne0  15769  lgssq  15771  lgssq2  15772  gausslemma2dlem3  15794  gausslemma2dlem4  15795  lgseisenlem1  15801  lgsquadlem2  15809  lgsquad2lem2  15813  lgsquad3  15815  m1lgs  15816  2lgslem1a2  15818  2lgsoddprmlem3  15842  2sqlem9  15855  2sqlem10  15856  edgiedgbg  15918  isuhgrm  15924  isushgrm  15925  uhgr0vb  15937  uhgrun  15939  isupgren  15948  isumgren  15958  umgrnloop0  15970  upgrun  15979  umgrun  15981  isuspgren  16010  isusgren  16011  usgrf1oedg  16058  usgredg3  16067  egrsubgr  16116  0uhgrsubgr  16118  uhgrspansubgrlem  16129  vtxdg0v  16147  vtxdgfi0e  16148  vtxdfifiun  16150  vtxdumgrfival  16151  1loopgrvd2fi  16158  vdegp1cid  16169  wlkl1loop  16211  2wlklem  16229  upgr2wlkdc  16230  clwwlkn0  16261  clwwlkn1  16271  clwwlkn2  16274  umgr2cwwk2dif  16277  clwwlk0on0  16284  clwwlknonel  16285  clwwlknonex2lem1  16290  trlsegvdeglem4  16316  ex-ceil  16325  bj-intexr  16506  peano3nninf  16612  nninfall  16614  isomninnlem  16637  iswomni0  16658  ismkvnnlem  16659  nconstwlpolem0  16670  gfsumval  16683  gfsumsn  16688  gfsump1  16689