Theorem fveq2i 6896

Description: Equality inference for function value. (Contributed by NM, 28-Jul-1999.)

Hypothesis

Ref	Expression
fveq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
fveq2i	⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Proof of Theorem fveq2i

Step	Hyp	Ref	Expression
1		fveq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		fveq2 6893	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹‘𝐴) = (𝐹‘𝐵)

Syntax hints:   = wceq 1534  ‘cfv 6546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-iota 6498  df-fv 6554

This theorem is referenced by:  fveq12i  6899  ot1stg  8009  ot2ndg  8010  ot3rdg  8011  wfrlem5OLD  8335  wfrlem14OLD  8344  tfr2a  8417  rdgsucmptf  8450  rdgsucmptnf  8451  rdg0n  8456  frsucmpt  8460  frsucmptn  8461  infiso  9544  inf3lemc  9662  cantnf  9729  wemapwe  9733  cnfcom2lem  9737  cnfcom2  9738  cnfcom3lem  9739  r1sucg  9805  rankprb  9887  rankopb  9888  ranksuc  9901  rankmapu  9914  cardiun  10018  alephsuc  10104  alephcard  10106  alephfplem2  10141  ackbij1lem8  10261  ackbij1lem13  10266  ackbij1lem14  10267  ackbij2lem2  10274  infpssrlem2  10338  fin23lem34  10380  fin23lem35  10381  aleph1  10605  pwcfsdom  10617  cfpwsdom  10618  alephom  10619  rankcf  10811  addpqnq  10972  mulpqnq  10975  addcomnq  10985  mulcomnq  10987  addclprlem2  11051  infrenegsup  12243  fseq1p1m1  13623  fz0to4untppr  13652  fldiv4p1lem1div2  13849  om2uzrdg  13970  uzrdgsuci  13974  fzennn  13982  axdc4uzlem  13997  seqp1d  14032  seqf1olem2  14056  facp1  14290  fac2  14291  fac3  14292  fac4  14293  4bc2eq6  14341  hashcard  14367  hasheq0  14375  hashun2  14395  hashun3  14396  hashprg  14407  hashprb  14409  hashprdifel  14410  hashp1i  14415  pr0hash2ex  14420  hashdif  14425  hashunlei  14437  hashfzo  14441  hashxplem  14445  hashfun  14449  hashimarn  14452  hashbclem  14464  hashbc  14465  hashf1lem2  14470  hashtpg  14499  ccatalpha  14596  s1len  14609  ccat2s1p2  14633  revs1  14768  cats1len  14864  lsws2  14908  lsws3  14909  lsws4  14910  rei  15156  imi  15157  sqrt1  15271  sqrt4  15272  sqrt9  15273  abs0  15285  absi  15286  sqreulem  15359  fsumabs  15800  fsumrelem  15806  o1fsum  15812  hashrabrex  15824  hashuni  15825  incexclem  15835  incexc  15836  isumnn0nn  15841  fprodefsum  16092  efsep  16107  sin0  16146  cos0  16147  ef01bndlem  16181  cos2bnd  16185  sin4lt0  16192  ruclem6  16232  aleph1re  16242  pwp1fsum  16388  m1bits  16435  sadcaddlem  16452  sadaddlem  16461  sadeq  16467  algrp1  16570  eucalg  16583  prmind2  16681  dfphi2  16771  phiprmpw  16773  phimullem  16776  pockthlem  16902  pockthg  16903  prmunb  16911  prmreclem4  16916  vdwap1  16974  vdwlem12  16989  prmo2  17037  prmo3  17038  prmgaplem7  17054  prmo4  17125  prmo5  17126  prmo6  17127  imasvsca  17530  mreexdomd  17657  isoval  17776  yonedalem21  18293  yonedalem22  18298  oduleval  18309  odubas  18311  odubasOLD  18312  joincomALT  18421  meetcomALT  18423  lubsn  18502  isacs5lem  18565  acsmapd  18574  efmnd1hash  18877  efmnd1bas  18878  efmnd2hash  18879  ressmulgnnd  19068  oppgplusfval  19338  setsplusg  19340  oppglemOLD  19341  symgbas  19364  symghash  19371  symgplusg  19376  symg1hash  19383  symg2hash  19385  symgtset  19393  symggen  19464  psgnsn  19514  psgnprfval1  19516  psgnprfval2  19517  odngen  19571  sylow1lem1  19592  efgs1b  19730  efgsfo  19733  efgredlemg  19736  efgredlemd  19738  frgpuplem  19766  gsumzmhm  19931  gsumzinv  19939  dprd2da  20038  dmdprdsplit2lem  20041  pgpfaclem1  20077  mgpplusg  20117  mgplemOLD  20118  ringidval  20162  opprmulfval  20314  opprlem  20317  opprlemOLD  20318  isrhm2d  20465  rhm1  20467  rhmopp  20487  cntzsubrng  20545  rhmsubclem3  20661  rhmsubclem4  20662  subdrgint  20778  rmodislmod  20902  rmodislmodOLD  20903  lspprid2  20971  lsmpr  21063  lsppr  21067  lspsntri  21071  lbspropd  21073  lspexchn2  21108  lspindp2l  21111  lspindp2  21112  lspsnat  21122  lsppratlem1  21124  lsppratlem3  21126  lsppratlem4  21127  lidlrsppropd  21229  zrhpsgnodpm  21584  psgnfix1  21590  psgnfix2  21591  psgndiflemB  21592  dsmmbas2  21731  dsmmelbas  21733  dsmmsubg  21737  frlmip  21772  islinds2  21807  lindsind2  21813  lindfmm  21821  islindf4  21832  assamulgscmlem2  21893  evlsval  22097  selvval  22126  psropprmul  22223  ply1sca2  22239  ply1mpl0  22242  ply1mpl1  22244  coe1fzgsumd  22292  ply1fermltlchr  22300  evls1var  22326  evl1gsumd  22345  evl1varpw  22349  evl1varpwval  22350  evl1scvarpw  22351  mat1bas  22439  mat0dim0  22457  mat0dimid  22458  mat0dimscm  22459  mat0dimcrng  22460  mat1rhmelval  22470  dmatval  22482  scmatval  22494  mat1scmat  22529  1mavmul  22538  marrepfval  22550  marepvfval  22555  ma1repvcl  22560  ma1repveval  22561  submafval  22569  mdetfval1  22580  mdetralt  22598  mdetunilem7  22608  m2detleiblem3  22619  m2detleiblem4  22620  madufval  22627  maducoeval2  22630  madugsum  22633  minmar1fval  22636  cramerimplem1  22673  cramer0  22680  pmatcoe1fsupp  22691  cpmat  22699  mat2pmatfval  22713  mat2pmatmul  22721  idmatidpmat  22727  m2cpminv0  22751  pmatcollpwfi  22772  pmatcollpw3fi1lem1  22776  pm2mpval  22785  chpmatval2  22823  cpmidpmat  22863  cayleyhamilton1  22882  sn0cld  23082  lpdifsn  23135  restcls  23173  restntr  23174  ordtrest2  23196  leordtval  23205  pttoponconst  23589  ptclsg  23607  xkoptsub  23646  xkofvcn  23676  tgqtop  23704  hmeocls  23760  hmeontr  23761  ptcmpfi  23805  ptcmplem1  24044  tmdgsum  24087  utop2nei  24243  cuspcvg  24294  iscusp2  24295  cnextucn  24296  comet  24510  nrmmetd  24571  isngp3  24595  ngpds  24601  tngnm  24656  cnmetdval  24775  qdensere2  24801  tgioo3  24809  cnmpopc  24937  cnheibor  24969  htpyco2  24993  phtpyco2  25004  pco0  25029  pi1xfrcnv  25072  cnrbas  25157  cncvs  25160  cnnm  25176  ipcau2  25250  cfilfcls  25290  cncmet  25338  reust  25397  rrxprds  25405  rrxsca  25412  ehleudis  25434  ehleudisval  25435  pjthlem1  25453  ovolunlem1a  25513  ovolfiniun  25518  ovoliunlem2  25520  ovoliunlem3  25521  ovoliun  25522  ovolicc1  25533  ismbl2  25544  unmbl  25554  volinun  25563  volfiniun  25564  voliunlem1  25567  voliunlem2  25568  ioorinv  25593  mbfimaopnlem  25672  itg2cnlem2  25780  itg2cn  25781  dfitg  25787  itg0  25797  iblre  25811  itgreval  25814  itgitg2  25824  iblconst  25835  itgconst  25836  itgcn  25862  limcflflem  25897  dvn1  25944  dvlipcn  26015  c1lip2  26019  dvcnvrelem2  26039  ply1divalg2  26163  ply1remlem  26189  dgr0  26287  elqaalem2  26345  dvradcnv  26447  pserdvlem2  26455  pserdv2  26457  abelthlem6  26463  abelthlem9  26467  sinhalfpilem  26488  cospi  26497  sincos4thpi  26538  sincos6thpi  26540  sincos3rdpi  26541  pige3ALT  26544  sinkpi  26546  eflog  26600  logfac  26625  logdmopn  26673  logtayl  26684  cxpcn3  26773  root1eq1  26780  cxpeq  26782  logbleb  26808  logblt  26809  sqrt2cxp2logb9e3  26824  ang180lem1  26834  ang180lem2  26835  ang180lem4  26837  lawcos  26841  1cubrlem  26866  asin1  26919  atan0  26933  atan1  26953  log2cnv  26969  birthdaylem2  26977  lgamgulmlem2  27055  gam1  27090  ftalem3  27100  ppiprm  27176  ppinprm  27177  chtprm  27178  chtnprm  27179  ppi1  27189  ppi1i  27193  ppi2i  27194  cht2  27197  cht3  27198  ppiub  27230  chtub  27238  bposlem6  27315  bposlem8  27317  bposlem9  27318  lgsval2lem  27333  lgsqrlem1  27372  lgsqrlem4  27375  lgsquadlem2  27407  chebbnd1  27498  rplogsumlem1  27510  rplogsumlem2  27511  dchrisum0flb  27536  mulog2sumlem2  27561  pntpbnd1a  27611  pntlemf  27631  nosepne  27707  noinfbnd2lem1  27757  bday0s  27855  bday1s  27858  left0s  27913  right0s  27914  left1s  27915  right1s  27916  precsexlem1  28203  precsexlem2  28204  cchhllem  28817  cchhllemOLD  28818  axlowdimlem17  28889  graop  28962  setsiedg  28969  vtxvalsnop  28974  iedgvalsnop  28975  usgrexmpllem  29193  uhgrspan1lem2  29234  uhgrspan1lem3  29235  upgrres1lem2  29244  upgrres1lem3  29245  structtocusgr  29379  cusgrsizeinds  29386  cusgrsize  29388  vtxdg0e  29408  uspgrloopvtx  29449  uspgrloopiedg  29451  uspgrloopedg  29452  umgr2v2evtx  29455  umgr2v2eiedg  29457  vtxdginducedm1lem1  29473  vtxdginducedm1  29477  vtxdginducedm1fi  29478  finsumvtxdg2ssteplem1  29479  finsumvtxdg2ssteplem2  29480  finsumvtxdg2ssteplem3  29481  finsumvtxdg2ssteplem4  29482  finsumvtxdg2sstep  29483  finsumvtxdg2size  29484  wlkres  29604  wlkp1lem2  29608  trlreslem  29633  clwlkcompbp  29716  crctcshlem2  29749  crctcshwlkn0  29752  2wlkdlem1  29856  2wlkdlem2  29857  2wlkdlem4  29859  2pthdlem1  29861  2wlkond  29868  2pthd  29871  umgr2adedgwlk  29876  clwwlknclwwlkdifnum  29910  clwwlkccatlem  29919  clwlkclwwlkfo  29939  clwlknf1oclwwlkn  30014  clwwlknon2num  30035  0wlkon  30050  0clwlk  30060  0cycl  30064  1pthdlem1  30065  1pthdlem2  30066  1wlkdlem1  30067  1wlkdlem4  30070  1pthond  30074  lp1cycl  30082  wlk2v2elem2  30086  wlk2v2e  30087  3wlkdlem1  30089  3wlkdlem2  30090  3wlkdlem4  30092  3pthdlem1  30094  3wlkond  30101  3pthd  30104  3cycld  30108  3cyclpd  30109  upgr3v3e3cycl  30110  upgr4cycl4dv4e  30115  eupth2eucrct  30147  eupthvdres  30165  eupth2lem3  30166  eucrct2eupth  30175  konigsbergvtx  30176  konigsbergiedg  30177  konigsberg  30187  2clwwlk2  30278  numclwlk1lem1  30299  numclwlk1  30301  numclwwlkqhash  30305  frgrreg  30324  ex-co  30368  ex-ceil  30378  ex-fac  30381  ex-hash  30383  ex-sqrt  30384  ex-prmo  30389  0vfval  30536  nvvop  30539  vsfval  30563  cnnvg  30608  cnnvs  30610  cnnvnm  30611  imsdval  30616  ipidsq  30640  nmblolbii  30729  blocnilem  30734  ip0i  30755  ip1ilem  30756  ipasslem10  30769  siilem1  30781  cnbn  30799  h2hva  30904  h2hsm  30905  h2hnm  30906  axhfvadd-zf  30912  axhvcom-zf  30913  axhvass-zf  30914  axhv0cl-zf  30915  axhvaddid-zf  30916  axhfvmul-zf  30917  axhvmulid-zf  30918  axhvmulass-zf  30919  axhvdistr1-zf  30920  axhvdistr2-zf  30921  axhvmul0-zf  30922  axhfi-zf  30923  axhis1-zf  30924  axhis2-zf  30925  axhis3-zf  30926  axhis4-zf  30927  axhcompl-zf  30928  norm-iii-i  31069  normsubi  31071  norm3difi  31077  normpar2i  31086  hh0v  31098  hhssva  31187  hhsssm  31188  hhssnm  31189  hhshsslem1  31197  hhsscms  31208  choc1  31257  shjcom  31288  pjhthlem1  31321  pjoc2i  31368  shs0i  31379  chj0i  31385  chdmj1i  31411  chjassi  31416  spansn0  31471  spanpr  31510  qlaxr4i  31564  pjadjii  31604  pjaddii  31605  pjmulii  31607  pjsubii  31608  pjcji  31614  pjnormi  31651  pjpythi  31652  ho0val  31680  lnop0  31896  lnophmlem2  31947  nmbdoplbi  31954  nmcopexi  31957  lnfn0i  31972  nmcfnexi  31981  nmopadji  32020  nmoptri2i  32029  nmopcoadj2i  32032  unierri  32034  branmfn  32035  pjbdlni  32079  pjclem2  32126  sto1i  32166  stm1ri  32174  st0  32179  hstrlem3a  32190  hstrlem4  32192  golem1  32201  superpos  32284  shatomistici  32291  iuninc  32481  hashunif  32713  pfxlsw2ccat  32817  chnub  32884  pmtrprfv2  32970  psgnfzto1st  32987  cyc2fv1  33003  cycpmco2lem4  33011  cycpmco2lem7  33014  cycpmco2  33015  cyc3fv1  33019  cyc3fv2  33020  cycpmrn  33025  cyc3genpmlem  33033  rlocval  33119  primefldchr  33156  xrge0slmod  33229  imaslmhm  33238  zringfrac  33435  evl1deg2  33455  evl1deg3  33456  lmimdim  33504  rlmdim  33510  rgmoddimOLD  33511  lbslsat  33517  ply1degltdimlem  33523  lindsun  33526  ccfldextdgrr  33564  0ringirng  33571  algextdeglem2  33591  algextdeglem3  33592  algextdeglem4  33593  algextdeglem5  33594  algextdeglem6  33595  algextdeglem7  33596  algextdeglem8  33597  rtelextdg2lem  33599  constrsuc  33610  2sqr3minply  33620  lmatfvlem  33643  lmat22e11  33646  madjusmdetlem1  33655  zarmxt1  33708  sqsscirc1  33736  ordtrest2NEW  33751  lmlim  33775  qqh0  33812  qqh1  33813  qqhcn  33819  qqhucn  33820  rrhcn  33825  cnrrext  33838  rrhre  33849  brsigarn  34030  sxval  34036  measvuni  34060  measunl  34062  measinblem  34066  volmeas  34077  braew  34088  aean  34090  sxbrsigalem3  34119  sxbrsiga  34137  0elcarsg  34154  inelcarsg  34158  carsgclctunlem1  34164  carsgclctunlem2  34166  omsmeas  34170  sitgval  34179  sitgclg  34189  sitmcl  34198  eulerpart  34229  fiblem  34245  fibp1  34248  fib2  34249  fib3  34250  fib4  34251  fib5  34252  fib6  34253  probdif  34267  probfinmeasbALTV  34276  cndprobnul  34284  bayesth  34286  dstrvprob  34318  coinflipprob  34326  coinflippvt  34331  ballotlem1  34333  ballotlem2  34335  ballotlemfval0  34342  ballotlem4  34345  ballotlemi1  34349  ballotlemii  34350  ballotlemic  34353  ballotlem1c  34354  ballotlemgun  34371  ballotth  34384  ccatmulgnn0dir  34401  signstfveq0  34436  signsvtp  34442  signsvtn  34443  signsvfpn  34444  signsvfnn  34445  ftc2re  34457  hgt750lemd  34507  hgt750lem  34510  2cycld  34979  derang0  35010  subfac0  35018  subfac1  35019  subfacp1lem3  35023  subfacp1lem5  35025  subfacp1lem6  35026  kur14lem6  35052  kur14lem7  35053  cvmliftlem5  35130  cvmliftlem10  35135  cvmliftlem13  35137  cvmlift2lem9  35152  cvmliftphtlem  35158  satfv1  35204  fmla1  35228  satfv0fvfmla0  35254  sategoelfvb  35260  msubff1  35397  iexpire  35570  rdgprc0  35630  rankaltopb  35816  rankeq1o  36008  clsun  36053  bj-rdg0gALT  36791  istoprelowl  37080  finxp1o  37112  finxpreclem4  37114  lindsdom  37328  matunitlindflem1  37330  ptrecube  37334  poimirlem3  37337  poimirlem4  37338  poimirlem30  37364  mblfinlem2  37372  mblfinlem3  37373  mblfinlem4  37374  ismblfin  37375  voliunnfl  37378  ftc1anclem3  37409  ftc1anclem4  37410  ftc1anclem5  37411  ftc1anclem6  37412  dvasin  37418  dvacos  37419  dvreasin  37420  dvreacos  37421  areacirclem4  37425  fdc  37459  prdsbnd2  37509  ismtyres  37522  reheibor  37553  rngo1cl  37653  rngokerinj  37689  riotaclbgBAD  38665  pmapglb  39482  trlcocnv  40432  dicval2  40891  dicopelval2  40893  dicelval2N  40894  djhfval  41109  djhcom  41117  dihjatcclem1  41130  dihjatcclem2  41131  dihprrnlem1N  41136  dihprrnlem2  41137  djhlsmat  41139  dvh4dimlem  41155  dvh2dim  41157  dvh3dim3N  41161  lclkrlem2c  41221  lclkrlem2m  41231  lclkrlem2v  41240  lcfrlem2  41255  lcfrlem18  41272  lcfrlem21  41275  lcfrlem23  41277  mapdindp4  41435  mapdh6eN  41452  mapdh7dN  41462  mapdh8ab  41489  mapdh8ad  41491  mapdh8b  41492  mapdh8e  41496  hdmap1l6e  41526  hdmapfval  41539  hdmapip1  41628  lcmfunnnd  41724  lcm1un  41725  lcm2un  41726  lcm3un  41727  lcm4un  41728  lcm5un  41729  lcm6un  41730  lcm7un  41731  lcm8un  41732  aks6d1c1p2  41821  aks6d1c1p3  41822  aks6d1c1p4  41823  aks6d1c5lem3  41849  aks6d1c7lem2  41893  aks5lem3a  41901  unitscyglem3  41909  unitscyglem4  41910  prjspnval2  42308  acos1half  42366  mapfzcons  42410  mzpresrename  42444  mzpcompact2lem  42445  diophren  42507  rabren3dioph  42509  monotoddzzfi  42637  jm2.23  42691  expdiophlem1  42716  dnnumch1  42742  aomclem6  42757  dfac21  42764  lnrfg  42817  mendsca  42887  mendvscafval  42888  cytpval  42904  arearect  42917  aleph1min  43261  resqrtvalex  43349  imsqrtvalex  43350  comptiunov2i  43410  trclfvdecomr  43432  ntrclscls00  43770  hashnzfz  44031  hashnzfz2  44032  dvradcnv2  44058  binomcxplemnotnn0  44067  rfcnpre3  44669  rfcnpre4  44670  fprodabs2  45252  mccl  45255  lptioo2cn  45302  lptioo1cn  45303  limclner  45308  limsupresuz  45360  limsupequzmpt2  45375  limsupequzmptf  45388  climlimsupcex  45426  liminfresre  45436  liminfvalxr  45440  liminfresuz  45441  liminfequzmpt2  45448  liminf0  45450  liminfpnfuz  45473  cosnegpi  45524  dvnmul  45600  iblempty  45622  iblsplit  45623  stoweidlem11  45668  stoweidlem14  45671  wallispilem3  45724  wallispilem4  45725  wallispi2lem2  45729  dirkerper  45753  fourierdlem41  45805  fourierdlem42  45806  fourierdlem48  45811  fourierdlem62  45825  fourierdlem69  45832  fourierdlem73  45836  fourierdlem79  45842  fourierdlem80  45843  fourierdlem81  45844  fourierdlem89  45852  fourierdlem90  45853  fourierdlem91  45854  fourierdlem93  45856  fourierdlem96  45859  fourierdlem97  45860  fourierdlem98  45861  fourierdlem99  45862  fourierdlem100  45863  fourierdlem103  45866  fourierdlem104  45867  fourierdlem108  45871  fourierdlem110  45873  fourierdlem112  45875  fourierdlem113  45876  fouriersw  45888  etransclem23  45914  rrxtopn0  45950  sge0tsms  46037  sge0splitmpt  46068  sge0iunmptlemfi  46070  sge0iunmptlemre  46072  sge0iunmpt  46075  sge0isum  46084  sge0xaddlem2  46091  sge0xadd  46092  meaunle  46121  psmeasure  46128  meaiunincf  46140  meaiuninc3  46142  meaiininclem  46143  meaiininc  46144  caragen0  46163  caragenuncllem  46169  omeiunltfirp  46176  ovnsubadd  46229  hoidmv1lelem3  46250  hoidmv1le  46251  hoidmvlelem3  46254  hoidmvlelem5  46256  hoidmvle  46257  hspmbllem2  46284  ovnsplit  46305  ovnovollem3  46315  vonioolem2  46338  vonct  46350  smflimlem4  46431  smflimsuplem2  46478  smflimsuplem8  46484  smflimsup  46485  tworepnotupword  46541  iccpartigtl  47031  iccpartlt  47032  fmtnorec2  47151  fmtno5  47165  nnsum4primeseven  47408  opstrgric  47510  ushggricedg  47511  cznrnglem  47672  cznabel  47673  cznrng  47674  cznnring  47675  rhmsubcALTVlem3  47696  ply1mulgsum  47809  lineval  47813  lcoop  47830  lincfsuppcl  47832  lincvalsng  47835  lincvalpr  47837  lincvalsc0  47840  linc0scn0  47842  lincdifsn  47843  linc1  47844  lincsum  47848  lindslinindimp2lem4  47880  lindslinindsimp2lem5  47881  snlindsntor  47890  lincresunit3lem2  47899  lincresunit3  47900  zlmodzxzldeplem3  47921  ldepsnlinc  47927  blen1  48008  blen2  48009  itcoval0mpt  48090  ackval1  48105  ackval2  48106  ackval3  48107  ackval40  48117  ackval41a  48118  ackval42  48120  ackval50  48122  lines  48155  rrxsphere  48172  2sphere  48173  itscnhlinecirc02plem3  48208  inlinecirc02p  48211  icccldii  48288  iscnrm3rlem3  48312  mndtcco  48448  aacllem  48585