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  2277  cbvalv1  2371  spv  2423  chvar  2425  cbval  2428  sb1  2508  nfsb4t  2529  exmoeu  2607  euim  2643  2eu3  2679  ralbida  3274  rgen2a  3357  ralcom2  3363  ceqsalt  3484  ceqsalgALT  3487  spcimgft  3511  spcdv  3549  rspcdv  3569  rspcebdv  3571  rexraleqim  3601  sbcn1  3791  sbcbi1  3796  sbeqalb  3801  sbcel21v  3806  elpwunsn  4645  rabsnifsb  4683  ssunsn2  4788  preqr1g  4812  iuneqconst  4963  axprlem3  5387  sbcop1  5458  propeqop  5479  euotd  5486  rexopabb  5502  sotr2  5593  relop  5828  elinxp  6008  elimasni  6089  sotri2  6123  ordpss  6391  onmindif  6457  dffv2  6980  mpteqb  7013  elfvmptrab  7023  chfnrn  7048  elpreima  7057  iinpreima  7069  exfo  7105  ffnfv  7119  f1elima  7267  f1ounsn  7280  f1eqcocnv  7309  fliftfun  7320  soisores  7335  isotr  7344  isomin  7345  ovmpodv2  7578  difsnexi  7775  onint  7804  oneqmin  7814  ordunisuc2  7855  tfindsg  7872  findsg  7909  resf1extb  7946  f1oweALT  7984  el2mpocl  8097  poseq  8175  soseq  8176  ressuppss  8200  funsssuppss  8207  suppofssd  8220  smoiso  8370  seqomlem2  8461  oaordi  8554  oawordri  8558  oaordex  8566  oalimcl  8568  omwordi  8579  oewordi  8600  oelim2  8604  nnmwordi  8644  xpider  8809  iiner  8810  undifixp  8962  mptelixpg  8963  dom2lem  9019  findcard2s  9181  pssnn  9184  nneneq  9221  fineqvlem  9257  dif1ennnALT  9268  unfilem2  9298  domunfican  9313  f1dmvrnfibi  9330  fsuppimp  9360  dffi2  9415  infsupprpr  9498  wemaplem2  9541  suc11reg  9620  noinfep  9661  cantnflem1  9690  r1fin  9780  tcrank  9901  rankfilimbi  9902  spcdvw  9970  setrec2fun  9973  cardlim  10053  fseqenlem1  10103  alephnbtwn  10150  alephord2i  10156  alephf1  10164  cardaleph  10168  alephiso  10177  dfac12lem2  10223  ackbij1lem16  10312  cflm  10327  cfcoflem  10350  sornom  10355  fin23lem27  10406  isf32lem7  10437  fin17  10472  fin1a2lem2  10479  fin1a2lem4  10481  fin1a2lem6  10483  fin1a2lem9  10486  axdc3lem2  10529  zorn2lem7  10580  uniimadom  10628  inar1  10860  grothomex  10914  addcanpi  10984  mulcanpi  10985  enqer  11006  genpcd  11091  genpnmax  11092  ltexprlem4  11124  reclem3pr  11134  reclem4pr  11135  suplem2pr  11138  axpre-ltadd  11252  axpre-sup  11254  ltletr  11402  00id  11485  addn0nid  11736  mul0or  11956  prodgt02  12165  lemul1a  12171  divgt0  12185  divge0  12186  ledivp1i  12242  ltdivp1i  12243  cju  12316  nnsub  12382  nominpos  12583  nn0n0n1ge2  12674  btwnnz  12775  suprfinzcl  12813  ublbneg  13060  zmax  13072  cnref1o  13113  ltsubrp  13158  ltaddrp  13159  xrltletr  13286  qbtwnre  13329  xltnegi  13346  xnn0xadd0  13377  iccsupr  13573  icoshft  13604  difreicc  13615  iccshftri  13618  iccshftli  13620  iccdili  13622  icccntri  13624  fzen  13674  elfz1b  13727  fzofzim  13844  eluzgtdifelfzo  13862  elfzo1elm1fzo0  13903  injresinjlem  13925  injresinj  13926  flval2  13954  flval3  13955  modmuladdim  14057  modaddmodup  14077  addmodlteq  14089  fseqsupubi  14121  ssnn0fi  14128  mptnn0fsuppr  14142  sq01  14369  hashf1rn  14496  hashgt12el  14567  hashgt12el2  14568  hashfundm  14587  hash2pr  14614  hash2exprb  14616  hashge2el2difr  14626  hashtpg  14630  hash3tr  14636  lswlgt0cl  14714  ccatalpha  14740  pfxfv  14832  pfxsuff1eqwrdeq  14848  ccatopth2  14866  swrdccat  14884  swrdccat3blem  14888  reuccatpfxs1lem  14895  repsdf2  14929  repswsymball  14930  repswrevw  14938  cshweqrep  14972  cshw1  14973  2cshwcshw  14976  scshwfzeqfzo  14977  cshwcsh2id  14979  swrdco  14988  swrd2lsw  15105  2swrd2eqwrdeq  15106  wwlktovfo  15111  cjre  15306  icodiamlt  15605  reusq0  15632  o1lo1  15704  o1of2  15780  o1rlimmul  15786  zsum  15884  modfsummods  15960  zprod  16104  reeff1  16288  dvdsmod0  16428  dvds2lem  16438  muldvds1  16450  dvdscmulr  16454  dvdsmulcr  16455  dvdsdivcl  16486  mod2eq1n2dvds  16517  oddnn02np1  16518  divalglem8  16570  ndvdsadd  16580  zeqzmulgcd  16682  dfgcd2  16719  absproddvds  16792  lcmftp  16811  coprmdvds  16828  2mulprm  16868  isprm5  16883  divgcdodd  16886  isprm6  16890  prmdvdsexpr  16893  prmdvdsbc  16902  cncongrprm  16905  phiprmpw  16953  modprm0  16983  pythagtriplem4  16997  pcz  17059  difsqpwdvds  17065  1arith  17105  prmgaplem5  17233  prmgaplem6  17234  cshwrepswhash1  17280  sbcie2s  17339  divsfval  17719  catsubcat  18014  fthmon  18104  isinitoi  18174  istermoi  18175  iszeroi  18184  setcmon  18262  setcepi  18263  funcestrcsetclem8  18321  fthestrcsetc  18324  funcsetcestrclem8  18336  fthsetcestrc  18339  odupos  18500  pltnle  18510  pltval3  18511  lublecllem  18532  latasym  18617  mrelatglb  18734  mrelatlub  18736  cnvpsb  18753  chninf  18809  mgmpropd  18829  0gisid  18848  isgrpid2  19187  ghmghmrn  19449  ghmf1  19460  kerf1ghm  19461  orbsta  19527  resscntz  19547  gsmsymgrfixlem1  19641  gsmsymgreqlem2  19645  mndodcongi  19757  odf1  19776  lsmss1  19879  lsmss2  19881  efgredeu  19966  cntzcmnss  20055  imasabl  20090  lt6abl  20109  ablfaclem3  20303  ogrpaddlt  20352  ringinvnz1ne0  20531  crngrhmfo  20726  0ringnnzr  20776  subrngringnsg  20805  srhmsubc  20932  domnmuln0  20961  isdrng3lem2  21006  lspsneq  21400  lspsneu  21401  lsmcv  21419  rnglidlmcl  21495  rngqiprngimf1lem  21590  lidldvgen  21658  domnchr  21838  znf1o  21857  zntoslem  21862  znfld  21866  cygznlem2a  21873  cygznlem3  21875  phlssphl  21965  islindf4  22144  uvcendim  22153  lindsenlbs  22157  psdmul  22487  ply1scln0  22610  gsummoncoe1  22626  matvscl  22746  scmataddcl  22831  scmatsubcl  22832  scmatfo  22845  scmatghm  22848  maducoeval2  22955  matunitlindf  22996  slesolinv  22998  cramerimplem2  23002  cpmatelimp  23030  cpmatelimp2  23032  cpmatacl  23034  cpmatinvcl  23035  pm2mpf1  23117  cayhamlem1  23184  cayleyhamilton1  23210  0ntr  23389  islpi  23467  lmss  23616  cmpcld  23720  cmpfi  23726  1stcelcls  23780  comppfsc  23851  ptcnplem  23940  qtophmeo  24136  fbdmn0  24153  fbasrn  24203  elfm3  24269  fmfnfmlem4  24276  fclscf  24344  cnpfcf  24360  alexsubALTlem3  24368  tsmsres  24463  blval2  24881  tnggrpr  24974  nmoleub  25050  nmhmcn  25441  ncvs1  25478  iscau4  25600  caussi  25618  cmssmscld  25671  cmslssbn  25693  cniccbdd  25782  ovoliunnul  25828  mbfinf  25986  itg2splitlem  26069  dvcn  26241  c1lip1  26317  c1lip3  26319  dvcnvrelem1  26337  dvfsumlem2  26347  ply1divex  26455  quotcan  26632  aannenlem1  26655  taylf  26688  taylthlem2  26701  ulmcaulem  26721  ulmcau  26722  reeff1o  26774  logccv  26991  rtprmirr  27088  logreclem  27090  isosctrlem2  27147  xrlimcnp  27296  rlimcxp  27301  ftalem7  27406  vmappw  27443  fsumdvdsmul  27522  fsumvma  27540  dchreq  27585  dchrptlem1  27591  dchrsum  27596  bposlem7  27617  lgsqrlem2  27674  lgsdchr  27682  gausslemma2dlem1a  27692  lgseisenlem2  27703  lgsquad2  27713  2lgslem1b  27719  2sqlem6  27750  2sqnn0  27765  addsq2reu  27767  2sqreulem2  27779  ltsval2  28013  ltsres  28019  nodenselem8  28048  nodense  28049  noresle  28054  cutsun12  28176  madeval2  28219  elmade  28243  negsf1o  28440  muls0ord  28571  recsex  28605  bdayons  28662  addonbday  28665  noseqrdgfn  28692  n0subs  28749  eln0zs  28786  zsoring  28795  bdayfinbndlem1  28853  z12bdaylem1  28856  tgcgrcomimp  28939  isperp2  29190  xmstrkgc  29463  brbtwn  29477  brcgr  29478  axcgrid  29494  axeuclidlem  29540  axeuclid  29541  elntg2  29563  lpvtx  29646  upgrex  29670  upgrpredgv  29717  upgredgpr  29720  uhgr0v0e  29819  subgrprop  29854  fusgrfisbase  29909  edgnbusgreu  29948  nbusgredgeu0  29949  cusgredg  30005  structtocusgr  30027  cusgrsize2inds  30034  cusgrsize  30035  usgredgsscusgredg  30040  fusgrmaxsize  30045  uspgrloopvtxel  30097  umgr2v2e  30106  vtxdginducedm1fi  30125  finsumvtxdg2sstep  30130  rgrprop  30141  rusgrprop  30143  0uhgrrusgr  30159  rusgrpropedg  30165  ewlkprop  30184  upgrewlkle2  30187  wlkprop  30192  upgrwlkcompim  30223  uspgr2wlkeq  30226  wlklenvclwlk  30234  wlkonprop  30237  wlkres  30249  redwlk  30251  wlkdlem2  30262  pfxwlk  30266  subgrwlk  30269  wksonproplem  30287  usgr2trlspth  30347  usgr2pth  30350  pthdlem1  30352  crctcshwlkn0lem4  30402  wwlksnprcl  30428  wlkiswwlks2  30464  wwlksm1edg  30470  wlknewwlksn  30476  wwlksnred  30481  wwlksnextbi  30483  wwlksnextwrd  30486  wwlksnextinj  30488  wwlksnextsurj  30489  umgr2wlk  30538  usgrwwlks2on  30547  umgrwwlks2on  30548  elwwlks2  30558  clwwlk1loop  30579  umgrclwwlkge2  30582  clwlkclwwlklem2a1  30583  clwlkclwwlklem2a4  30588  clwlkclwwlklem2a  30589  clwlkclwwlklem2  30591  clwlkclwwlkfo  30600  clwwisshclwwslemlem  30604  clwwlknwwlksn  30629  clwwlknlbonbgr1  30630  clwwlkn1loopb  30634  clwwlkf  30638  clwwlknon1  30688  clwwlknonwwlknonb  30697  clwwlknonex2lem2  30699  loop1cycl  30744  vdn0conngrumgrv2  30797  frgrnbnb  30894  frgrncvvdeqlem2  30901  frgrncvvdeqlem3  30902  frgrncvvdeqlem6  30905  frgrwopreglem4a  30911  fusgr2wsp2nb  30935  frrusgrord0lem  30940  numclwwlk2lem1lem  30943  2clwwlk2clwwlklem  30947  2clwwlk2clwwlk  30951  numclwwlk1lem2foa  30955  numclwwlk1lem2f1  30958  frgrreg  30995  hlipgt0  31516  ocin  31898  ocnel  31900  shmodsi  31991  pjmf1  32318  unopf1o  32518  staddi  32848  stadd3i  32850  mdi  32897  dmdmd  32902  dmdi  32904  dmdbr2  32905  dmdbr3  32907  dmdbr4  32908  dmdi4  32909  mdsl1i  32923  superpos  32956  cvbr4i  32969  atssma  32980  atcv1  32982  atomli  32984  chirredlem1  32992  addltmulALT  33048  ifeqeqx  33138  disjxpin  33182  suppss3  33315  fpwrelmap  33325  expgt0b  33408  mndlactfo  33588  mndractfo  33590  qsfld  34022  ply1degltdimlem  34254  ply1degltdim  34255  metider  34526  tpr2rico  34544  xrge0iifiso  34567  qqhcn  34623  qqhucn  34624  esumlub  34692  esumpinfval  34705  esumpinfsum  34709  ballotlemfc0  35125  ballotlemfcc  35126  ftc2re  35227  bnj517  35515  soinfdom  35717  fnrelpredd  35720  axsepg2  35808  axsepg3  35809  axsepg3ALT  35810  axsepg4  35811  axsepg5  35812  axnulg  35813  erdsze2lem2  35969  satfv1  36128  satfdmlem  36133  satf0op  36142  fmlasuc  36151  dfrdg4  36715  altopthsn  36726  btwncomim  36778  btwnexch3  36785  btwnexch2  36788  endofsegid  36850  opnrebl2  37109  nn0prpwlem  37110  onsuct0  37229  ordcmp  37235  nndivsub  37245  regsfromunir1  37328  dnibndlem13  37356  bj-cbvexvv  37539  bj-cbval  37545  bj-cbvex  37546  bj-cbvexw  37576  bj-nnf-cbval  37682  bj-cbv3tb  37699  bj-spimtv  37706  bj-equsal  37738  bj-sbsb  37749  bj-vtoclf  37827  bj-sepg  37836  bj-gabss  37848  bj-gabeqd  37850  currysetlem2  37861  bj-snsetex  37876  bj-axseprep  37990  bj-ismooredr2  38031  bj-inftyexpiinj  38130  bj-finsumval0  38206  bj-fvimacnv0  38207  bj-bary1lem1  38232  bj-bary1  38233  f1omptsnlem  38259  iooelexlt  38285  relowlpssretop  38287  rdgeqoa  38293  finxpsuclem  38320  fvineqsneq  38335  pibt2  38340  wl-isseteq  38428  wl-dfcleq  38437  wl-equsal1i  38476  ltflcei  38531  sin2h  38533  cos2h  38534  tan2h  38535  poimirlem3  38541  poimirlem4  38542  poimirlem18  38556  poimirlem20  38558  poimirlem21  38559  poimirlem22  38560  poimirlem24  38562  poimirlem25  38563  poimirlem26  38564  poimirlem27  38565  poimirlem28  38566  poimirlem31  38569  poimir  38571  heicant  38573  mblfinlem1  38575  mblfinlem2  38576  mblfinlem3  38577  mblfinlem4  38578  mbfresfi  38584  cnambfre  38586  ftc1anc  38619  dvasin  38622  areacirclem1  38626  areacirclem4  38629  areacirc  38631  findcard4  38632  brabg2  38651  fzmul  38675  fdc  38679  incsequz2  38683  isbnd2  38717  opidonOLD  38786  opidon2OLD  38788  grpomndo  38809  elghomlem2OLD  38820  rngoueqz  38874  dvrunz  38888  divrngidl  38962  refressn  39465  dral1-o  39961  lsatn0  40056  l1cvpat  40111  leat2  40351  atnle  40374  cvlcvr1  40396  cvrexchlem  40476  cvratlem  40478  cvrat  40479  atcvrj0  40485  atle  40493  snatpsubN  40807  linepsubN  40809  pmapsub  40825  lneq2at  40835  lncvrelatN  40838  2llnma3r  40845  cdlemblem  40850  paddasslem5  40881  poml4N  41010  lhpmcvr4N  41083  trlval2  41220  cdlemd6  41260  cdleme7ga  41305  cdleme25b  41411  cdleme29b  41432  cdleme35fnpq  41506  cdleme50f1  41600  cdlemf1  41618  cdlemg27b  41753  cdlemk28-3  41965  tendospcanN  42080  diaf11N  42106  dia2dimlem1  42121  dibf11N  42218  dihf11  42324  dihmeetlem1N  42347  dochvalr  42414  dochnel2  42449  dvh4dimlem  42500  dochsat0  42514  mapd1o  42705  hdmapf1oN  42922  hgmapval0  42949  hgmapf1oN  42960  hlhilhillem  43017  nnproddivdvdsd  43050  lcmineqlem  43102  aks4d1p1p5  43125  aks4d1p3  43128  aks4d1p8d2  43135  aks4d1p8  43137  aks4d1p9  43138  fldhmf1  43140  isprimroot2  43144  primrootsunit1  43147  primrootscoprmpow  43149  posbezout  43150  primrootscoprbij  43152  primrootlekpowne0  43155  primrootspoweq0  43156  aks6d1c1p1  43157  aks6d1c1p2  43159  aks6d1c1p3  43160  aks6d1c1p4  43161  aks6d1c1p5  43162  aks6d1c1p7  43163  aks6d1c1p6  43164  aks6d1c1p8  43165  aks6d1c2p2  43169  aks6d1c2lem3  43176  aks6d1c2lem4  43177  hashnexinj  43178  aks6d1c2  43180  aks6d1c5lem0  43185  aks6d1c5lem1  43186  aks6d1c5  43189  sticksstones1  43196  sticksstones3  43198  sticksstones8  43203  sticksstones11  43206  sticksstones12  43208  sticksstones20  43216  sticksstones22  43218  aks6d1c6lem3  43222  aks6d1c6lem4  43223  aks6d1c6isolem1  43224  aks6d1c6isolem2  43225  aks6d1c6lem5  43227  aks6d1c7  43234  rhmqusspan  43235  unitscyglem2  43246  unitscyglem3  43247  aks5lem8  43251  sn-axprlem3  43272  oexpreposd  43379  sn-remul0ord  43459  frlmsnic  43604  fsuppind  43618  prjspval  43631  rexrabdioph  43800  fphpdo  43823  irrapxlem3  43830  rmxypairf1o  43917  rmxycomplete  43923  zindbi  43952  lermxnn0  43956  ltrmy  43958  rmyeq0  43959  rmyeq  43960  lermy  43961  acongsym  43982  acongneg2  43983  wepwsolem  44048  onsupuni  44230  onsupmaxb  44240  onsucf1o  44273  onov0suclim  44275  oe0suclim  44278  onsucwordi  44289  cantnfresb  44325  omabs2  44333  tfsconcat0b  44347  tfsconcatrev  44349  naddcnffo  44365  oaun3lem1  44375  oaltom  44405  omltoe  44407  sdomne0  44413  sdomne0d  44414  safesnsupfidom1o  44417  intabssd  44519  iscard4  44533  ss2iundf  44658  frege129d  44762  frege133d  44764  axfrege52a  44855  axfrege52c  44886  ntrk0kbimka  45038  gneispace  45133  suprleubrd  45165  suprlubrd  45167  radcnvrat  45297  nzss  45300  expgrowthi  45316  bi23impib  45468  rspsbc2  45516  tratrb  45518  sbcim2g  45520  truniALT  45523  3impcombi  45798  tpid3gVD  45823  orbi1rVD  45829  sbc3orgVD  45832  rspsbc2VD  45836  tratrbVD  45842  sbcim2gVD  45856  sbcbiVD  45857  truniALTVD  45859  trintALTVD  45861  trintALT  45862  csbingVD  45865  csbsngVD  45874  csbxpgVD  45875  csbresgVD  45876  csbrngVD  45877  csbima12gALTVD  45878  csbunigVD  45879  csbfv12gALTVD  45880  relopabVD  45882  isosctrlem1ALT  45915  relpfrlem  45942  trfr  45951  fzisoeu  46315  xrralrecnnge  46400  allbutfi  46403  climinf  46617  liminfreuzlem  46811  climliminf  46815  climliminflimsup  46817  xlimpnfxnegmnf  46823  xlimbr  46836  stoweidlem7  47016  stoweidlem62  47071  sge0gerpmpt  47411  meaiuninclem  47489  carageniuncllem2  47531  issmflem  47736  et-sqrtnegnre  47882  ormkglobd  47886  tmachlem-agreeprod  47946  funressnfv  48112  funressnvmo  48114  f1cof1b  48146  2reu3  48179  ralbinrald  48191  afv0fv0  48218  afv0nbfvbi  48220  afvfv0bi  48221  fnbrafvb  48223  afvres  48241  tz6.12-afv  48242  afvco2  48245  ndmaovcl  48272  afv2res  48308  tz6.12-afv2  48309  nelbrim  48344  f1oresf1o2  48360  zm1nn  48371  nltle2tri  48382  subsubelfzo0  48396  2tceilhalfelfzo1  48405  iccpartres  48499  iccpartiltu  48503  fargshiftfv  48520  ichnreuop  48553  ichreuopeq  48554  prsprel  48568  sprsymrelf1lem  48572  sprsymrelfolem2  48574  sprsymrelfo  48578  prpair  48582  paireqne  48592  sbcpr  48602  nprmmul2  48609  nprmmul3  48610  fmtnof1  48619  goldbachthlem2  48630  fmtnoprmfac1  48649  fmtnoprmfac2  48651  lighneallem2  48690  lighneallem4b  48693  lighneallem4  48694  evennodd  48740  oddneven  48741  oexpnegnz  48775  evenltle  48814  fpprwppr  48836  fpprwpprb  48837  gbowge7  48860  gbege6  48862  sbgoldbwt  48874  sbgoldbst  48875  nnsum3primesle9  48891  bgoldbtbndlem2  48903  grimprop  48980  isuspgrimlem  48992  uhgrimisgrgriclem  49027  clnbgrgrimlem  49030  grtriproplem  49036  isgrtri  49040  grimgrtri  49046  stgr1  49058  isubgr3stgr  49072  grlimprop  49081  uspgrlimlem2  49086  uspgrlimlem3  49087  grlimprclnbgr  49093  gpg5nbgrvtx13starlem1  49168  clintop  49304  isassintop  49306  lidldomn1  49327  uzlidlring  49331  2zrngnmlid2  49353  rngccatidALTV  49368  ringccatidALTV  49402  srhmsubcALTV  49421  ztprmneprm  49458  pgrpgt2nabl  49477  lindslinindimp2lem4  49572  lincresunit3  49592  fldivexpfllog2  49676  digexp  49718  naryfvalelfv  49743  affinecomb1  49813  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849  eenglngeehlnm  49850  itscnhlc0yqe  49870  itsclc0yqsol  49875  itscnhlc0xyqsol  49876  itschlc0xyqsol1  49877  itschlc0xyqsol  49878  itsclquadeu  49888  inlinecirc02plem  49897  inlinecirc02p  49898  mofsn  49953  seposep  50033  resipos  50082  idmon  50127  idepi  50128  prsthinc  50571  grptcmon  50700  grptcepi  50701  spd  50785