Theorem biimpd 232

Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 218 and biimpi 219. (Contributed by NM, 11-Jan-1993.)

Hypothesis

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

Assertion

Ref	Expression
biimpd	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem biimpd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biimp 218	. 2 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mpbid  235  sylibd  242  sylbid  243  mpbidi  244  imbitrid  247  biimtrdi  256  con4bid  320  mtbird  328  mtbiri  330  imbi1d  344  bitr3  355  pm5.21im  377  biimpa  482  pm4.71da  573  bi23imp13  1133  alexbii  1866  spvv  2021  spfw  2066  cbvalw  2068  sbequiOLD  2121  chvarfv  2276  cbvalv1  2370  spv  2422  chvar  2424  cbval  2427  sb1  2507  nfsb4t  2528  exmoeu  2606  euim  2642  2eu3  2678  ralbida  3273  rgen2a  3356  ralcom2  3362  ceqsalt  3483  ceqsalgALT  3486  spcimgft  3510  spcdv  3548  rspcdv  3568  rspcebdv  3570  rexraleqim  3601  sbcn1  3791  sbcbi1  3796  sbeqalb  3801  sbcel21v  3806  elpwunsn  4645  rabsnifsb  4683  ssunsn2  4788  preqr1g  4812  iuneqconst  4963  axprlem3  5390  axprlem3OLD  5394  sbcop1  5464  propeqop  5484  euotd  5490  rexopabb  5506  sotr2  5597  relop  5830  elinxp  6012  elimasni  6087  sotri2  6123  ordpss  6386  onmindif  6452  dffv2  6974  mpteqb  7007  elfvmptrab  7017  chfnrn  7042  elpreima  7051  iinpreima  7063  exfo  7099  ffnfv  7113  f1elima  7261  f1ounsn  7274  f1eqcocnv  7303  fliftfun  7314  soisores  7329  isotr  7338  isomin  7339  ovmpodv2  7572  difsnexi  7761  onint  7790  oneqmin  7800  ordunisuc2  7841  tfindsg  7858  findsg  7895  resf1extb  7932  f1oweALT  7970  el2mpocl  8084  poseq  8157  soseq  8158  ressuppss  8182  funsssuppss  8189  suppofssd  8202  smoiso  8352  seqomlem2  8441  oaordi  8534  oawordri  8538  oaordex  8546  oalimcl  8548  omwordi  8559  oewordi  8580  oelim2  8584  nnmwordi  8624  xpider  8789  iiner  8790  undifixp  8942  mptelixpg  8943  dom2lem  8999  findcard2s  9161  pssnn  9164  nneneq  9201  fineqvlem  9237  dif1ennnALT  9248  unfilem2  9277  domunfican  9292  f1dmvrnfibi  9309  fsuppimp  9339  dffi2  9394  infsupprpr  9477  wemaplem2  9520  suc11reg  9599  noinfep  9640  cantnflem1  9669  r1fin  9756  tcrank  9867  cardlim  9978  fseqenlem1  10028  alephnbtwn  10075  alephord2i  10081  alephf1  10089  cardaleph  10093  alephiso  10102  dfac12lem2  10148  ackbij1lem16  10237  cflm  10252  cfcoflem  10275  sornom  10280  fin23lem27  10331  isf32lem7  10362  fin17  10397  fin1a2lem2  10404  fin1a2lem4  10406  fin1a2lem6  10408  fin1a2lem9  10411  axdc3lem2  10454  zorn2lem7  10505  uniimadom  10553  inar1  10785  grothomex  10839  addcanpi  10909  mulcanpi  10910  enqer  10931  genpcd  11016  genpnmax  11017  ltexprlem4  11049  reclem3pr  11059  reclem4pr  11060  suplem2pr  11063  axpre-ltadd  11177  axpre-sup  11179  ltletr  11327  00id  11410  addn0nid  11659  mul0or  11879  prodgt02  12088  lemul1a  12094  divgt0  12108  divge0  12109  ledivp1i  12165  ltdivp1i  12166  cju  12239  nnsub  12305  nominpos  12506  nn0n0n1ge2  12597  btwnnz  12698  suprfinzcl  12736  ublbneg  12983  zmax  12995  cnref1o  13036  ltsubrp  13081  ltaddrp  13082  xrltletr  13209  qbtwnre  13252  xltnegi  13269  xnn0xadd0  13300  iccsupr  13496  icoshft  13527  difreicc  13538  iccshftri  13541  iccshftli  13543  iccdili  13545  icccntri  13547  fzen  13596  elfz1b  13649  fzofzim  13766  eluzgtdifelfzo  13784  elfzo1elm1fzo0  13825  injresinjlem  13847  injresinj  13848  flval2  13876  flval3  13877  modmuladdim  13979  modaddmodup  13999  addmodlteq  14011  fseqsupubi  14043  ssnn0fi  14050  mptnn0fsuppr  14064  sq01  14290  hashf1rn  14417  hashgt12el  14488  hashgt12el2  14489  hashfundm  14508  hash2pr  14535  hash2exprb  14537  hashge2el2difr  14547  hashtpg  14551  hash3tr  14557  lswlgt0cl  14635  ccatalpha  14661  pfxfv  14753  pfxsuff1eqwrdeq  14769  ccatopth2  14787  swrdccat  14805  swrdccat3blem  14809  reuccatpfxs1lem  14816  repsdf2  14850  repswsymball  14851  repswrevw  14859  cshweqrep  14893  cshw1  14894  2cshwcshw  14897  scshwfzeqfzo  14898  cshwcsh2id  14900  swrdco  14909  swrd2lsw  15026  2swrd2eqwrdeq  15027  wwlktovfo  15032  cjre  15227  icodiamlt  15526  reusq0  15553  o1lo1  15625  o1of2  15701  o1rlimmul  15707  zsum  15805  modfsummods  15881  zprod  16025  reeff1  16209  dvdsmod0  16349  dvds2lem  16359  muldvds1  16371  dvdscmulr  16375  dvdsmulcr  16376  dvdsdivcl  16407  mod2eq1n2dvds  16438  oddnn02np1  16439  divalglem8  16491  ndvdsadd  16501  zeqzmulgcd  16601  dfgcd2  16637  absproddvds  16708  lcmftp  16727  coprmdvds  16744  2mulprm  16784  isprm5  16799  divgcdodd  16802  isprm6  16806  prmdvdsexpr  16809  prmdvdsbc  16818  cncongrprm  16821  phiprmpw  16868  modprm0  16898  pythagtriplem4  16912  pcz  16974  difsqpwdvds  16980  1arith  17020  prmgaplem5  17148  prmgaplem6  17149  cshwrepswhash1  17195  sbcie2s  17254  divsfval  17634  catsubcat  17929  fthmon  18019  isinitoi  18089  istermoi  18090  iszeroi  18099  setcmon  18177  setcepi  18178  funcestrcsetclem8  18236  fthestrcsetc  18239  funcsetcestrclem8  18251  fthsetcestrc  18254  odupos  18415  pltnle  18425  pltval3  18426  lublecllem  18447  latasym  18532  mrelatglb  18649  mrelatlub  18651  cnvpsb  18668  chninf  18724  mgmpropd  18744  0gisid  18762  isgrpid2  19101  ghmghmrn  19363  ghmf1  19374  kerf1ghm  19375  orbsta  19441  resscntz  19461  gsmsymgrfixlem1  19555  gsmsymgreqlem2  19559  mndodcongi  19671  odf1  19690  lsmss1  19793  lsmss2  19795  efgredeu  19880  cntzcmnss  19969  imasabl  20004  lt6abl  20023  ablfaclem3  20217  ogrpaddlt  20266  ringinvnz1ne0  20443  crngrhmfo  20638  0ringnnzr  20687  subrngringnsg  20716  srhmsubc  20843  domnmuln0  20872  isdrng3lem2  20916  lspsneq  21310  lspsneu  21311  lsmcv  21329  rnglidlmcl  21405  rngqiprngimf1lem  21498  lidldvgen  21566  domnchr  21746  znf1o  21765  zntoslem  21770  znfld  21774  cygznlem2a  21781  cygznlem3  21783  phlssphl  21873  islindf4  22052  uvcendim  22061  lindsenlbs  22065  psdmul  22395  ply1scln0  22518  gsummoncoe1  22534  matvscl  22654  scmataddcl  22739  scmatsubcl  22740  scmatfo  22753  scmatghm  22756  maducoeval2  22863  matunitlindf  22904  slesolinv  22906  cramerimplem2  22910  cpmatelimp  22938  cpmatelimp2  22940  cpmatacl  22942  cpmatinvcl  22943  pm2mpf1  23025  cayhamlem1  23092  cayleyhamilton1  23118  0ntr  23297  islpi  23375  lmss  23524  cmpcld  23628  cmpfi  23634  1stcelcls  23688  comppfsc  23759  ptcnplem  23848  qtophmeo  24044  fbdmn0  24061  fbasrn  24111  elfm3  24177  fmfnfmlem4  24184  fclscf  24252  cnpfcf  24268  alexsubALTlem3  24276  tsmsres  24371  blval2  24789  tnggrpr  24882  nmoleub  24958  nmhmcn  25349  ncvs1  25386  iscau4  25508  caussi  25526  cmssmscld  25579  cmslssbn  25601  cniccbdd  25690  ovoliunnul  25736  mbfinf  25894  itg2splitlem  25977  dvcn  26149  c1lip1  26225  c1lip3  26227  dvcnvrelem1  26245  dvfsumlem2  26255  ply1divex  26363  quotcan  26542  aannenlem1  26565  taylf  26598  taylthlem2  26611  ulmcaulem  26631  ulmcau  26632  reeff1o  26684  logccv  26901  rtprmirr  26998  logreclem  27000  isosctrlem2  27057  xrlimcnp  27206  rlimcxp  27211  ftalem7  27316  vmappw  27353  fsumdvdsmul  27432  fsumvma  27450  dchreq  27495  dchrptlem1  27501  dchrsum  27506  bposlem7  27527  lgsqrlem2  27584  lgsdchr  27592  gausslemma2dlem1a  27602  lgseisenlem2  27613  lgsquad2  27623  2lgslem1b  27629  2sqlem6  27660  2sqnn0  27675  addsq2reu  27677  2sqreulem2  27689  ltsval2  27893  ltsres  27899  nodenselem8  27928  nodense  27929  noresle  27934  cutsun12  28056  madeval2  28099  elmade  28123  negsf1o  28320  muls0ord  28451  recsex  28485  bdayons  28542  addonbday  28545  noseqrdgfn  28572  n0subs  28629  eln0zs  28666  zsoring  28675  bdayfinbndlem1  28733  z12bdaylem1  28736  tgcgrcomimp  28819  isperp2  29070  xmstrkgc  29343  brbtwn  29357  brcgr  29358  axcgrid  29374  axeuclidlem  29420  axeuclid  29421  elntg2  29443  lpvtx  29526  upgrex  29550  upgrpredgv  29597  upgredgpr  29600  uhgr0v0e  29699  subgrprop  29734  fusgrfisbase  29789  edgnbusgreu  29828  nbusgredgeu0  29829  cusgredg  29885  structtocusgr  29907  cusgrsize2inds  29914  cusgrsize  29915  usgredgsscusgredg  29920  fusgrmaxsize  29925  uspgrloopvtxel  29977  umgr2v2e  29986  vtxdginducedm1fi  30005  finsumvtxdg2sstep  30010  rgrprop  30021  rusgrprop  30023  0uhgrrusgr  30039  rusgrpropedg  30045  ewlkprop  30064  upgrewlkle2  30067  wlkprop  30072  upgrwlkcompim  30103  uspgr2wlkeq  30106  wlklenvclwlk  30114  wlkonprop  30117  wlkres  30129  redwlk  30131  wlkdlem2  30142  pfxwlk  30146  subgrwlk  30149  wksonproplem  30167  usgr2trlspth  30227  usgr2pth  30230  pthdlem1  30232  crctcshwlkn0lem4  30282  wwlksnprcl  30308  wlkiswwlks2  30344  wwlksm1edg  30350  wlknewwlksn  30356  wwlksnred  30361  wwlksnextbi  30363  wwlksnextwrd  30366  wwlksnextinj  30368  wwlksnextsurj  30369  umgr2wlk  30418  usgrwwlks2on  30427  umgrwwlks2on  30428  elwwlks2  30438  clwwlk1loop  30459  umgrclwwlkge2  30462  clwlkclwwlklem2a1  30463  clwlkclwwlklem2a4  30468  clwlkclwwlklem2a  30469  clwlkclwwlklem2  30471  clwlkclwwlkfo  30480  clwwisshclwwslemlem  30484  clwwlknwwlksn  30509  clwwlknlbonbgr1  30510  clwwlkn1loopb  30514  clwwlkf  30518  clwwlknon1  30568  clwwlknonwwlknonb  30577  clwwlknonex2lem2  30579  loop1cycl  30624  vdn0conngrumgrv2  30677  frgrnbnb  30774  frgrncvvdeqlem2  30781  frgrncvvdeqlem3  30782  frgrncvvdeqlem6  30785  frgrwopreglem4a  30791  fusgr2wsp2nb  30815  frrusgrord0lem  30820  numclwwlk2lem1lem  30823  2clwwlk2clwwlklem  30827  2clwwlk2clwwlk  30831  numclwwlk1lem2foa  30835  numclwwlk1lem2f1  30838  frgrreg  30875  hlipgt0  31396  ocin  31778  ocnel  31780  shmodsi  31871  pjmf1  32198  unopf1o  32398  staddi  32728  stadd3i  32730  mdi  32777  dmdmd  32782  dmdi  32784  dmdbr2  32785  dmdbr3  32787  dmdbr4  32788  dmdi4  32789  mdsl1i  32803  superpos  32836  cvbr4i  32849  atssma  32860  atcv1  32862  atomli  32864  chirredlem1  32872  addltmulALT  32928  ifeqeqx  33018  disjxpin  33062  suppss3  33195  fpwrelmap  33205  expgt0b  33288  mndlactfo  33468  mndractfo  33470  qsfld  33901  ply1degltdimlem  34133  ply1degltdim  34134  metider  34405  tpr2rico  34423  xrge0iifiso  34446  qqhcn  34502  qqhucn  34503  esumlub  34571  esumpinfval  34584  esumpinfsum  34588  ballotlemfc0  35005  ballotlemfcc  35006  ftc2re  35107  bnj517  35395  fnrelpredd  35597  rankfilimbi  35610  axsepg2  35667  axsepg3  35668  axsepg3ALT  35669  axsepg4  35670  axsepg5  35671  axnulg  35672  erdsze2lem2  35784  satfv1  35943  satfdmlem  35948  satf0op  35957  fmlasuc  35966  dfrdg4  36531  altopthsn  36542  btwncomim  36594  btwnexch3  36601  btwnexch2  36604  endofsegid  36666  opnrebl2  36941  nn0prpwlem  36942  onsuct0  37061  ordcmp  37067  nndivsub  37077  regsfromunir1  37160  dnibndlem13  37188  bj-cbvexvv  37371  bj-cbval  37377  bj-cbvex  37378  bj-cbvexw  37408  bj-nnf-cbval  37514  bj-cbv3tb  37531  bj-spimtv  37538  bj-equsal  37570  bj-sbsb  37581  bj-vtoclf  37659  bj-sepg  37668  bj-gabss  37680  bj-gabeqd  37682  currysetlem2  37693  bj-snsetex  37708  bj-axseprep  37820  bj-ismooredr2  37861  bj-inftyexpiinj  37962  bj-finsumval0  38038  bj-fvimacnv0  38039  bj-bary1lem1  38064  bj-bary1  38065  f1omptsnlem  38091  iooelexlt  38117  relowlpssretop  38119  rdgeqoa  38125  finxpsuclem  38152  fvineqsneq  38167  pibt2  38172  wl-isseteq  38260  wl-dfcleq  38269  wl-equsal1i  38308  ltflcei  38363  sin2h  38365  cos2h  38366  tan2h  38367  poimirlem3  38373  poimirlem4  38374  poimirlem18  38388  poimirlem20  38390  poimirlem21  38391  poimirlem22  38392  poimirlem24  38394  poimirlem25  38395  poimirlem26  38396  poimirlem27  38397  poimirlem28  38398  poimirlem31  38401  poimir  38403  heicant  38405  mblfinlem1  38407  mblfinlem2  38408  mblfinlem3  38409  mblfinlem4  38410  mbfresfi  38416  cnambfre  38418  ftc1anc  38451  dvasin  38454  areacirclem1  38458  areacirclem4  38461  areacirc  38463  findcard4  38464  brabg2  38468  fzmul  38492  fdc  38496  incsequz2  38500  isbnd2  38534  opidonOLD  38603  opidon2OLD  38605  grpomndo  38626  elghomlem2OLD  38637  rngoueqz  38691  dvrunz  38705  divrngidl  38779  refressn  39282  dral1-o  39778  lsatn0  39873  l1cvpat  39928  leat2  40168  atnle  40191  cvlcvr1  40213  cvrexchlem  40293  cvratlem  40295  cvrat  40296  atcvrj0  40302  atle  40310  snatpsubN  40624  linepsubN  40626  pmapsub  40642  lneq2at  40652  lncvrelatN  40655  2llnma3r  40662  cdlemblem  40667  paddasslem5  40698  poml4N  40827  lhpmcvr4N  40900  trlval2  41037  cdlemd6  41077  cdleme7ga  41122  cdleme25b  41228  cdleme29b  41249  cdleme35fnpq  41323  cdleme50f1  41417  cdlemf1  41435  cdlemg27b  41570  cdlemk28-3  41782  tendospcanN  41897  diaf11N  41923  dia2dimlem1  41938  dibf11N  42035  dihf11  42141  dihmeetlem1N  42164  dochvalr  42231  dochnel2  42266  dvh4dimlem  42317  dochsat0  42331  mapd1o  42522  hdmapf1oN  42739  hgmapval0  42766  hgmapf1oN  42777  hlhilhillem  42834  nnproddivdvdsd  42867  lcmineqlem  42919  aks4d1p1p5  42942  aks4d1p3  42945  aks4d1p8d2  42952  aks4d1p8  42954  aks4d1p9  42955  fldhmf1  42957  isprimroot2  42961  primrootsunit1  42964  primrootscoprmpow  42966  posbezout  42967  primrootscoprbij  42969  primrootlekpowne0  42972  primrootspoweq0  42973  aks6d1c1p1  42974  aks6d1c1p2  42976  aks6d1c1p3  42977  aks6d1c1p4  42978  aks6d1c1p5  42979  aks6d1c1p7  42980  aks6d1c1p6  42981  aks6d1c1p8  42982  aks6d1c2p2  42986  aks6d1c2lem3  42993  aks6d1c2lem4  42994  hashnexinj  42995  aks6d1c2  42997  aks6d1c5lem0  43002  aks6d1c5lem1  43003  aks6d1c5  43006  sticksstones1  43013  sticksstones3  43015  sticksstones8  43020  sticksstones11  43023  sticksstones12  43025  sticksstones20  43033  sticksstones22  43035  aks6d1c6lem3  43039  aks6d1c6lem4  43040  aks6d1c6isolem1  43041  aks6d1c6isolem2  43042  aks6d1c6lem5  43044  aks6d1c7  43051  rhmqusspan  43052  unitscyglem2  43063  unitscyglem3  43064  aks5lem8  43068  sn-axprlem3  43089  oexpreposd  43198  sn-remul0ord  43284  frlmsnic  43423  fsuppind  43437  prjspval  43450  rexrabdioph  43636  fphpdo  43659  irrapxlem3  43666  rmxypairf1o  43753  rmxycomplete  43759  zindbi  43788  lermxnn0  43792  ltrmy  43794  rmyeq0  43795  rmyeq  43796  lermy  43797  acongsym  43818  acongneg2  43819  wepwsolem  43884  onsupuni  44071  onsupmaxb  44081  onsucf1o  44114  onov0suclim  44116  oe0suclim  44119  onsucwordi  44130  cantnfresb  44166  omabs2  44174  tfsconcat0b  44188  tfsconcatrev  44190  naddcnffo  44206  oaun3lem1  44216  oaltom  44246  omltoe  44248  sdomne0  44254  sdomne0d  44255  safesnsupfidom1o  44258  intabssd  44360  iscard4  44374  ss2iundf  44500  frege129d  44604  frege133d  44606  axfrege52a  44697  axfrege52c  44728  ntrk0kbimka  44880  gneispace  44975  suprleubrd  45007  suprlubrd  45009  radcnvrat  45139  nzss  45142  expgrowthi  45158  bi23impib  45310  rspsbc2  45358  tratrb  45360  sbcim2g  45362  truniALT  45365  3impcombi  45640  tpid3gVD  45665  orbi1rVD  45671  sbc3orgVD  45674  rspsbc2VD  45678  tratrbVD  45684  sbcim2gVD  45698  sbcbiVD  45699  truniALTVD  45701  trintALTVD  45703  trintALT  45704  csbingVD  45707  csbsngVD  45716  csbxpgVD  45717  csbresgVD  45718  csbrngVD  45719  csbima12gALTVD  45720  csbunigVD  45721  csbfv12gALTVD  45722  relopabVD  45724  isosctrlem1ALT  45757  relpfrlem  45777  trfr  45786  fzisoeu  46134  xrralrecnnge  46220  allbutfi  46223  climinf  46437  liminfreuzlem  46631  climliminf  46635  climliminflimsup  46637  xlimpnfxnegmnf  46643  xlimbr  46656  stoweidlem7  46836  stoweidlem62  46891  sge0gerpmpt  47231  meaiuninclem  47309  carageniuncllem2  47351  issmflem  47556  et-sqrtnegnre  47702  ormkglobd  47706  tmachlem-agreeprod  47766  funressnfv  47932  funressnvmo  47934  f1cof1b  47966  2reu3  47999  ralbinrald  48011  afv0fv0  48038  afv0nbfvbi  48040  afvfv0bi  48041  fnbrafvb  48043  afvres  48061  tz6.12-afv  48062  afvco2  48065  ndmaovcl  48092  afv2res  48128  tz6.12-afv2  48129  nelbrim  48164  f1oresf1o2  48180  zm1nn  48191  nltle2tri  48202  subsubelfzo0  48216  2tceilhalfelfzo1  48225  iccpartres  48319  iccpartiltu  48323  fargshiftfv  48340  ichnreuop  48373  ichreuopeq  48374  prsprel  48388  sprsymrelf1lem  48392  sprsymrelfolem2  48394  sprsymrelfo  48398  prpair  48402  paireqne  48412  sbcpr  48422  nprmmul2  48429  nprmmul3  48430  fmtnof1  48439  goldbachthlem2  48450  fmtnoprmfac1  48469  fmtnoprmfac2  48471  lighneallem2  48510  lighneallem4b  48513  lighneallem4  48514  evennodd  48560  oddneven  48561  oexpnegnz  48595  evenltle  48634  fpprwppr  48656  fpprwpprb  48657  gbowge7  48680  gbege6  48682  sbgoldbwt  48694  sbgoldbst  48695  nnsum3primesle9  48711  bgoldbtbndlem2  48723  grimprop  48800  isuspgrimlem  48812  uhgrimisgrgriclem  48847  clnbgrgrimlem  48850  grtriproplem  48856  isgrtri  48860  grimgrtri  48866  stgr1  48878  isubgr3stgr  48892  grlimprop  48901  uspgrlimlem2  48906  uspgrlimlem3  48907  grlimprclnbgr  48913  gpg5nbgrvtx13starlem1  48988  clintop  49124  isassintop  49126  lidldomn1  49147  uzlidlring  49151  2zrngnmlid2  49173  rngccatidALTV  49188  ringccatidALTV  49222  srhmsubcALTV  49241  ztprmneprm  49278  pgrpgt2nabl  49297  lindslinindimp2lem4  49392  lincresunit3  49412  fldivexpfllog2  49496  digexp  49538  naryfvalelfv  49563  affinecomb1  49633  eenglngeehlnmlem1  49668  eenglngeehlnmlem2  49669  eenglngeehlnm  49670  itscnhlc0yqe  49690  itsclc0yqsol  49695  itscnhlc0xyqsol  49696  itschlc0xyqsol1  49697  itschlc0xyqsol  49698  itsclquadeu  49708  inlinecirc02plem  49717  inlinecirc02p  49718  mofsn  49773  seposep  49853  resipos  49902  idmon  49947  idepi  49948  prsthinc  50391  grptcmon  50520  grptcepi  50521  spd  50605  spcdvw  50606  setrec2fun  50619