Theorem biimpa 479

Description: Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)

Hypothesis

Ref	Expression
biimpa.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpa	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem biimpa

Step	Hyp	Ref	Expression
1		biimpa.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 231	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	imp 409	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  simprbda  501  simplbda  502  pm5.1  821  biimp3a  1465  equsex  2440  euor  2695  euorv  2696  euan  2706  euanv  2709  cgsexg  3537  cgsex2g  3538  cgsex4g  3539  ceqsex  3540  sbciegft  3808  sbeqalb  3836  reuan  3880  sseqtrid  4019  elpwunsn  4621  ralxfr2d  5311  propeqop  5397  euotd  5403  relop  5721  elsnxp  6142  sspred  6156  fnbr  6459  f1o00  6649  nfunsn  6707  foelrni  6727  dffv2  6756  iinpreima  6837  funressn  6921  fnex  6980  f1prex  7040  weniso  7107  riotaeqimp  7140  f1ocnv2d  7398  ofrval  7419  limsssuc  7565  opreuopreu  7734  eloprabi  7761  frxp  7820  poxp  7822  smodm2  7992  smoiso  7999  tz7.44lem1  8041  oev2  8148  oesuclem  8150  oecl  8162  omordi  8192  omwordri  8198  omword2  8200  omordlim  8203  omlimcl  8204  omeulem2  8209  oeordi  8213  oewordri  8218  oelim2  8221  oeoa  8223  oeoe  8225  nnawordi  8247  nnaordex  8264  erth  8338  iiner  8369  pw2f1olem  8621  pw2f1o  8622  onomeneq  8708  onfin2  8710  unxpdomlem2  8723  isinf  8731  findcard2  8758  fipreima  8830  fipwss  8893  preleqALT  9080  cantnfp1lem3  9143  carden2b  9396  carddomi2  9399  infxpenlem  9439  acni2  9472  numacn  9475  alephfp  9534  pwsdompw  9626  ackbij2lem3  9663  cfeq0  9678  cfsuc  9679  cfsmolem  9692  domfin4  9733  axdc3lem2  9873  axdc3lem4  9875  alephreg  10004  fpwwe2  10065  winainflem  10115  r1limwun  10158  inar1  10197  grudomon  10239  nlt1pi  10328  indpi  10329  nqereu  10351  ltbtwnnq  10400  prlem934  10455  prlem936  10469  addgt0sr  10526  leltne  10730  ne0gt0  10745  mullt0  11159  msqgt0  11160  mulne0  11282  divne0  11310  div2neg  11363  ltmul12a  11496  recgt1i  11537  negfi  11589  div4p1lem1div2  11893  nn0lt2  12046  peano5uzi  12072  eluzp1m1  12269  eluzaddi  12272  eluzsubi  12273  uz2m1nn  12324  nn01to3  12342  rpnnen1lem5  12381  rphalflt  12419  xrleltne  12539  max0sub  12590  xmulpnf1n  12672  xmulge0  12678  xadddi  12689  supxr  12707  supxr2  12708  ixxdisj  12754  ixxun  12755  ixxub  12760  ixxlb  12761  iccgelb  12794  icodisj  12863  difreicc  12871  iccf1o  12883  fzsuc2  12966  fzonmapblen  13084  elfznelfzo  13143  flge0nn0  13191  flge1nn  13192  2submod  13301  modfzo0difsn  13312  seqf1olem2  13411  expubnd  13542  sqlecan  13572  bernneq  13591  bernneq2  13592  expnbnd  13594  discr1  13601  facwordi  13650  faclbnd4lem4  13657  bcpasc  13682  hashgt0n0  13727  elprchashprn2  13758  hash1to3  13850  iswrdi  13866  ffz0iswrdOLD  13892  ccatsymb  13936  ccatass  13942  ccat1st1st  13984  swrdlend  14015  swrdfv2  14023  swrdspsleq  14027  pfxeq  14058  swrdswrdlem  14066  swrdswrd  14067  swrdpfx  14069  pfxccatin12lem1  14090  swrdccatin2  14091  revccat  14128  revrev  14129  repswpfx  14147  repswccat  14148  cshwcsh2id  14190  revco  14196  cshco  14198  s2f1o  14278  s4f1o  14280  wrdlen2i  14304  wwlktovf  14320  ofccat  14329  trclub  14358  sqr0lem  14600  sqrlem2  14603  sqrlem7  14608  max0add  14670  recval  14682  nnabscl  14685  absmax  14689  sqreulem  14719  climi0  14869  lo1bdd2  14881  rlimresb  14922  lo1eq  14925  rlimeq  14926  isercolllem3  15023  climsup  15026  fsumsplit  15097  fsumcom2  15129  explecnv  15220  fprodser  15303  fprodsplit  15320  fprodcom2  15338  eftlub  15462  sin02gt0  15545  rpnnen2lem10  15576  dvdsleabs2  15662  odd2np1  15690  oexpneg  15694  sqoddm1div8z  15703  bitsf1  15795  sadcaddlem  15806  bitsuz  15823  rplpwr  15907  rppwr  15908  nn0seqcvgd  15914  lcmneg  15947  qredeq  16001  dvdsnprmd  16034  oddprmge3  16044  ge2nprmge4  16045  isprm7  16052  qgt0numnn  16091  phibndlem  16107  hashgcdeq  16126  reumodprminv  16141  coprimeprodsq2  16146  pythagtrip  16171  dvdsprmpweqle  16222  fldivp1  16233  unbenlem  16244  4sqlem9  16282  4sqlem15  16295  4sqlem16  16296  vdwlem6  16322  vdwlem10  16326  vdwlem11  16327  vdwlem13  16329  vdw  16330  prmgaplem7  16393  prmgaplem8  16394  cshwshashlem1  16429  mreuni  16871  cidpropd  16980  subsubc  17123  ffthiso  17199  fuciso  17245  setcmon  17347  setcepi  17348  catciso  17367  funcestrcsetclem7  17396  funcestrcsetclem8  17397  setc1strwun  17403  funcsetcestrclem7  17411  hofcl  17509  hofpropd  17517  yonedalem4c  17527  yonedainv  17531  issstrmgm  17863  imasmnd  17949  pwsco1mhm  17996  imasgrp  18215  subginv  18286  subgmulg  18293  eqger  18330  subgga  18430  orbstafun  18441  orbsta  18443  symggrp  18528  psgnsn  18648  dfod2  18691  gexval  18703  gex1  18716  sylow2blem1  18745  sylow3lem1  18752  pj1eu  18822  efgredlema  18866  frgp0  18886  frgpmhm  18891  odadd1  18968  0cyg  19013  gsumzres  19029  gsumzsplit  19047  gsummptfzcl  19089  dprd2dlem1  19163  dprd2da  19164  dmdprdsplit2  19168  dprdsplit  19170  pgpfaclem3  19205  ablfac2  19211  imasring  19369  rhmf1o  19484  kerf1ghm  19497  kerf1hrmOLD  19498  subrg1  19545  abvneg  19605  lmhmf1o  19818  lmhmima  19819  reslmhm2b  19826  pwssplit0  19830  pwssplit1  19831  lsmspsn  19856  lspdisj  19897  lidlmcl  19990  isnzr2hash  20037  fidomndrnglem  20079  mplsubglem  20214  mplmonmul  20245  mplbas2  20251  subrgascl  20278  subrgasclcl  20279  evlsval2  20300  mpfind  20320  lply1binomsc  20475  absabv  20602  phlssphl  20803  f1lindf  20966  mat0dimscm  21078  scmataddcl  21125  scmatsubcl  21126  smatvscl  21133  mdetunilem8  21228  chfacfscmul0  21466  chfacfscmulfsupp  21467  chfacfscmulgsum  21468  chfacfpmmul0  21470  chfacfpmmulfsupp  21471  chfacfpmmulgsum  21472  cpmidpmatlem3  21480  chcoeffeqlem  21493  cayleyhamilton0  21497  cayleyhamiltonALT  21499  cayleyhamilton1  21500  elcls  21681  clsndisj  21683  isclo2  21696  neiuni  21730  neissex  21735  neiptopreu  21741  tgrest  21767  neitr  21788  tgcnp  21861  lmfpm  21903  lmcl  21905  lmss  21906  lmff  21909  ist1-2  21955  cnt1  21958  cmpsublem  22007  clsconn  22038  locfindis  22138  kgeni  22145  kgenidm  22155  txcnpi  22216  ptpjopn  22220  ptclsg  22223  txcmplem1  22249  qtoptop2  22307  qtoptopon  22312  r0sep  22356  ptunhmeo  22416  t0kq  22426  fsubbas  22475  neifil  22488  uffixsn  22533  ufildr  22539  rnelfm  22561  isfcls2  22621  uffclsflim  22639  alexsublem  22652  cnextfun  22672  cnextfvval  22673  cnextf  22674  cnextcn  22675  tmdcn2  22697  symgtgp  22714  tsmssplit  22760  ustuni  22835  trust  22838  utoptop  22843  restutop  22846  restutopopn  22847  ustuqtop1  22850  ustuqtop2  22851  ustuqtop3  22852  ustuqtop4  22853  utop2nei  22859  utop3cls  22860  ucncn  22894  trcfilu  22903  cfiluweak  22904  psmetdmdm  22915  xmeter  23043  prdsbl  23101  neibl  23111  methaus  23130  prdsxmslem2  23139  metustto  23163  metustexhalf  23166  metust  23168  cfilucfil  23169  psmetutop  23177  tngngp2  23261  tngngp  23263  tgqioo  23408  xrsxmet  23417  icccmplem1  23430  icccmplem2  23431  cnmpopc  23532  iihalf2  23537  icoopnst  23543  iocopnst  23544  xrhmeo  23550  lebnumlem1  23565  lebnumlem3  23567  pi1blem  23643  pi1grplem  23653  pi1xfrf  23657  pi1xfr  23659  pi1xfrcnvlem  23660  pi1cof  23663  pi1coghm  23665  cmetcaulem  23891  causs  23901  metcld  23909  lmcau  23916  rrxcph  23995  minveclem4  24035  ivthlem2  24053  ivthlem3  24054  ivthicc  24059  ovolshftlem1  24110  ovolicc1  24117  ovolicopnf  24125  volfiniun  24148  uniioombllem3  24186  dyaddisjlem  24196  vitalilem2  24210  itg1ge0  24287  mbfi1fseqlem3  24318  xrge0f  24332  itg2seq  24343  itg2monolem1  24351  itg2addlem  24359  itg2gt0  24361  iblcnlem  24389  itgss3  24415  itgsplit  24436  dvnff  24520  dvferm2  24584  dvlip2  24592  dveq0  24597  dvge0  24603  dvcnvre  24616  dvfsumle  24618  dvfsumabs  24620  dvfsumlem2  24624  ftc1lem2  24633  ftc1lem4  24636  ftc1lem5  24637  ftc1cn  24640  ftc2  24641  itgsubstlem  24645  coe1mul3  24693  ply1divex  24730  dgrlem  24819  dgrlb  24826  coemulhi  24844  dgrlt  24856  dgrmul  24860  plydivlem4  24885  fta1  24897  aaliou2b  24930  taylplem2  24952  dvtaylp  24958  ulmcau  24983  tanabsge  25092  sinq12gt0  25093  argimgt0  25195  cxplea  25279  cxple2  25280  cxpsqrt  25286  cxpaddlelem  25332  loglesqrt  25339  logrec  25341  ang180lem2  25388  lawcos  25394  asinlem3a  25448  asinlem3  25449  asinsin  25470  atanlogaddlem  25491  atanlogadd  25492  atanlogsub  25494  atantan  25501  atanbnd  25504  atantayl2  25516  leibpilem1  25518  efrlim  25547  wilthlem2  25646  basellem2  25659  sqfpc  25714  ppieq0  25753  sqff1o  25759  fsumdvdscom  25762  ppiub  25780  chpeq0  25784  chtleppi  25786  fsumvma  25789  fsumvma2  25790  mersenne  25803  dchrabs2  25838  dchr1re  25839  dchrpt  25843  lgsdilem  25900  lgsdinn0  25921  gausslemma2dlem0b  25933  gausslemma2dlem1a  25941  gausslemma2dlem5  25947  gausslemma2dlem6  25948  lgsquad3  25963  m1lgs  25964  2lgslem1a  25967  2lgslem1  25970  2lgslem3a1  25976  2lgslem3b1  25977  2lgslem3c1  25978  2lgslem3d1  25979  2sqlem6  25999  rpvmasumlem  26063  dchrisumlem3  26067  dchrisum0flblem1  26084  pntibndlem2a  26166  pntlem3  26185  padicabv  26206  ercgrg  26303  tglnunirn  26334  tglineeltr  26417  mirln2  26463  mirbtwnhl  26466  isperp2  26501  outpasch  26541  lnopp2hpgb  26549  dfcgrg2  26649  ttgbtwnid  26670  axcontlem2  26751  axcontlem12  26761  elntg2  26771  upgredg  26922  fusgrfisstep  27111  nbupgrres  27146  usgrnbcnvfv  27147  nbusgredgeu  27148  nbcplgr  27216  cusgrexi  27225  structtocusgr  27228  cusgrsizeinds  27234  vtxdgoddnumeven  27335  uhgr0edg0rgr  27355  wlkl1loop  27419  upgriswlk  27422  usgr2pthlem  27544  cyclnspth  27581  wwlknvtx  27623  wspthnp  27628  elwwlks2ons3  27734  elwspths2on  27739  usgr2wspthons3  27743  clwlkclwwlklem2a4  27775  clwlkclwwlk2  27781  clwlkclwwlkfolem  27785  clwlkclwwlkf1  27788  clwwisshclwws  27793  loopclwwlkn1b  27820  clwwlkf1  27828  wwlksext2clwwlk  27836  clwwnisshclwwsn  27838  eleclclwwlknlem2  27840  1pthon2v  27932  upgr3v3e3cycl  27959  upgreupthi  27987  eupth2lemb  28016  frgrncvvdeqlem7  28084  frgrncvvdeqlem8  28085  frgrncvvdeqlem9  28086  clwwnonrepclwwnon  28124  numclwwlkovh  28152  numclwwlk2lem1  28155  frgrreggt1  28172  frgrregord013  28174  cnnv  28454  nmounbseqi  28554  nmounbseqiALT  28555  nmlnogt0  28574  nmblolbii  28576  blocnilem  28581  ajmoi  28635  minvecolem4  28657  hhnv  28942  norm1  29026  hhssnv  29041  pjhtheu  29171  pjpreeq  29175  spanunsni  29356  fh1  29395  fh2  29396  cm2j  29397  chscllem4  29417  pjid  29472  adjmo  29609  eleigveccl  29736  eigvalcl  29738  eigvec1  29739  eighmre  29740  eighmorth  29741  nmop0h  29768  nmbdoplbi  29801  nmcoplbi  29805  nmophmi  29808  lncnopbd  29814  nmbdfnlbi  29826  nmcfnlbi  29829  cnlnadjeui  29854  branmfn  29882  rnbra  29884  nmopleid  29916  strlem5  30032  hstrlem5  30040  dmdbr3  30082  dmdbr4  30083  mdsl3  30093  hatomistici  30139  cvexchlem  30145  chirredlem1  30167  chirredlem2  30168  chirredi  30171  atcvat3i  30173  atcvat4i  30174  atabsi  30178  mdsymlem1  30180  mdsymlem3  30182  mdsymlem5  30184  dmdbr5ati  30199  cdj1i  30210  opreu2reuALT  30240  foresf1o  30265  rabfodom  30266  elabreximd  30270  elpreq  30290  iunrnmptss  30317  f1o3d  30372  acunirnmpt2f  30406  disjdsct  30438  1stpreimas  30441  fcobij  30458  fpwrelmapffslem  30468  xrofsup  30492  eliccelico  30500  elicoelioo  30501  dvdszzq  30531  prmdvdsbc  30532  numdenneg  30533  fsumiunle  30545  dpadd3  30588  threehalves  30591  s3f1  30623  ccatf1  30625  pfxlsw2ccat  30626  wrdt2ind  30627  cshf1o  30636  xrge0addgt0  30678  xrge0adddir  30679  xrge0npcan  30681  omndmul3  30714  symgcom  30727  pmtrcnel  30733  pmtrcnel2  30734  pmtrcnelor  30735  tocyc01  30760  trsp2cyc  30765  cycpmco2lem1  30768  cycpmco2lem4  30771  cycpmco2  30775  cycpmrn  30785  tocyccntz  30786  cyc3evpm  30792  cyc3genpmlem  30793  cyc3genpm  30794  cycpmgcl  30795  cycpmconjslem2  30797  cycpmconjs  30798  cyc3conja  30799  submarchi  30815  archirng  30817  archirngz  30818  archiexdiv  30819  archiabllem1a  30820  imaslmod  30922  linds2eq  30941  prmidlnr  30956  prmidl  30957  prmidlidl  30960  isprmidlc  30963  prmidlc  30964  qsidomlem1  30965  qsidomlem2  30966  mxidlidl  30972  mxidlnr  30973  mxidlmax  30974  lvecdimfi  30998  lvecdim0i  31004  lssdimle  31006  dimpropd  31007  lbslsat  31014  lindsunlem  31020  lbsdiflsp0  31022  dimkerim  31023  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  extdg1id  31053  1smat1  31069  madjusmdetlem2  31093  locfinreflem  31104  metideq  31133  unitdivcld  31144  cnre2csqlem  31153  ordtconnlem1  31167  fmcncfil  31174  lmxrge0  31195  pl1cn  31198  zrhunitpreima  31219  qqhval2lem  31222  qqhf  31227  indf1ofs  31285  esumfsup  31329  esumpcvgval  31337  esum2dlem  31351  esum2d  31352  esumiun  31353  sigasspw  31375  issgon  31382  ispisys2  31412  meascnbl  31478  voliune  31488  volfiniune  31489  omssubaddlem  31557  carsggect  31576  carsgclctunlem2  31577  oddpwdc  31612  eulerpartlems  31618  eulerpartlemgvv  31634  ballotlemfrcn0  31787  sgncl  31796  sgnneg  31798  sgn3da  31799  sgnmul  31800  sgnsub  31802  gsumnunsn  31811  signsplypnf  31820  signsply0  31821  signslema  31832  signstfvneq0  31842  signsvfpn  31855  signsvfnn  31856  repr0  31882  reprlt  31890  reprgt  31892  reprinfz1  31893  chtvalz  31900  breprexplemc  31903  hgt750lemb  31927  hgt750leme  31929  lpadlem3  31949  bnj563  32014  bnj1001  32231  revwlk  32371  spthcycl  32376  usgrgt2cycl  32377  umgracycusgr  32401  subfacp1lem5  32431  subfacp1lem6  32432  erdszelem9  32446  ptpconn  32480  resconn  32493  cvmlift3lem7  32572  satfv1  32610  fmlasuc  32633  satffunlem1lem2  32650  satffunlem2lem2  32653  satefvfmla0  32665  msrrcl  32790  trpredrec  33077  scutbdaylt  33276  btwnintr  33480  btwnouttr  33485  cgrxfr  33516  btwnconn1lem12  33559  colinbtwnle  33579  lineelsb2  33609  nn0prpwlem  33670  neibastop3  33710  onintopssconn  33788  bj-restsnss  34377  bj-restsnss2  34378  bj-idres  34455  taupilem1  34605  relowlssretop  34647  finxpsuclem  34681  unccur  34890  lindsenlbs  34902  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem2  34909  poimirlem8  34915  poimirlem14  34921  poimirlem15  34922  poimirlem17  34924  poimirlem20  34927  poimirlem22  34929  poimirlem24  34931  poimirlem25  34932  poimirlem27  34934  poimirlem28  34935  poimirlem31  34938  heicant  34942  mblfinlem2  34945  itg2gt0cn  34962  itgaddnclem2  34966  ftc1cnnclem  34980  ftc1cnnc  34981  ftc1anclem2  34983  ftc1anclem5  34986  ftc1anclem7  34988  ftc1anc  34990  ftc2nc  34991  dvasin  34993  areacirclem5  35001  areacirc  35002  fdc  35035  incsequz  35038  blbnd  35080  prdstotbnd  35087  cnpwstotbnd  35090  ismtyres  35101  rngohomf  35259  rngohom1  35261  rngohomadd  35262  rngohommul  35263  idlss  35309  idl0cl  35311  idladdcl  35312  idllmulcl  35313  idlrmulcl  35314  maxidlnr  35335  maxidlmax  35336  smprngopr  35345  pridlc  35364  ac6s6f  35466  eqvrelth  35861  lshpnel2N  36136  islsati  36145  lkr0f  36245  lfl1dim  36272  lfl1dim2N  36273  omlfh1N  36409  leat  36444  atlatmstc  36470  cvlatexch3  36489  lnnat  36578  cvrat3  36593  cvrat4  36594  3dim3  36620  dalem4  36816  dalem39  36862  paddasslem12  36982  psubcliN  37089  pmapojoinN  37119  lhpm0atN  37180  lhprelat3N  37191  trlnid  37330  trlval3  37338  cdleme22b  37492  trljco  37891  diaglbN  38206  dibvalrel  38314  dicvalrelN  38336  diclspsn  38345  dih1dimatlem  38480  dihlatat  38488  lcfl6  38651  lcfl8  38653  lcfrvalsnN  38692  lcfrlem9  38701  mapdheq2  38880  hlhillcs  39109  hlhilhillem  39111  factwoffsmonot  39147  fzosumm1  39175  frlmsnic  39198  renegneg  39290  mzpindd  39392  lzunuz  39414  2rexfrabdioph  39442  irrapxlem3  39470  pellexlem2  39476  pellexlem5  39479  pell1234qrreccl  39500  pell14qrdich  39515  pell1qrge1  39516  elpell1qr2  39518  reglogltb  39537  reglogleb  39538  rmxycomplete  39563  2nn0ind  39591  congabseq  39620  acongrep  39626  acongeq  39629  jm2.22  39641  jm2.26lem3  39647  pw2f1ocnv  39683  limsuc2  39690  fnwe2lem3  39701  aomclem6  39708  kercvrlsm  39732  pwssplit4  39738  lpirlnr  39766  rfovcnvf1od  40399  dssmapnvod  40415  cvgdvgrat  40694  radcnvrat  40695  dvconstbi  40715  bccbc  40726  bi2imp  40865  ax6e2ndeqALT  41314  mulltgt0  41328  refsumcn  41336  cncmpmax  41338  projf1o  41508  unirnmapsn  41526  icoiccdif  41849  climinf  41936  climreeq  41943  climeldmeq  41995  xlimresdm  42189  coskpi2  42196  cosknegpi  42199  icccncfext  42219  dvmptfprodlem  42278  volioore  42324  stoweidlem27  42361  stoweidlem29  42363  stoweidlem31  42365  stoweidlem34  42368  stoweidlem48  42382  stoweidlem59  42393  fourierdlem109  42549  fourierswlem  42564  elaa2  42568  etransclem37  42605  hspmbllem2  42958  smflimmpt  43133  sigarcol  43170  ndmaovg  43432  afv2orxorb  43476  subsubelfzo0  43575  iccelpart  43642  fargshiftf1  43650  fargshiftfo  43651  sbcpr  43732  reuopreuprim  43737  fmtnoprmfac1lem  43775  fmtno4prmfac  43783  2pwp1prmfmtno  43801  sfprmdvdsmersenne  43817  lighneallem3  43821  proththd  43828  evenm1odd  43853  evenp1odd  43854  nnoALTV  43909  fpprel2  43955  stgoldbwt  43990  sbgoldbst  43992  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbtbndlem2  44020  upgrwlkupwlk  44064  rnghmf1o  44223  rnghmsubcsetclem1  44295  zrinitorngc  44320  zrtermorngc  44321  rhmsubcsetclem1  44341  rhmsubcrngclem1  44347  funcringcsetcALTV2lem8  44363  funcringcsetclem8ALTV  44386  zrtermoringc  44390  ply1sclrmsm  44486  lincfsuppcl  44517  zofldiv2  44640  elbigolo1  44666  blennn0em1  44700  blennn0e2  44703  dig2nn0ld  44713  nn0sumshdiglem2  44731  rrxlinesc  44771  rrxlinec  44772  eenglngeehlnm  44775  rrxsphere  44784  itschlc0xyqsol  44803  itscnhlinecirc02plem3  44820