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  1865  spvv  2020  spfw  2065  cbvalw  2067  sbequiOLD  2120  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  3600  sbcn1  3790  sbcbi1  3795  sbeqalb  3800  sbcel21v  3805  elpwunsn  4641  rabsnifsb  4679  ssunsn2  4782  preqr1g  4806  iuneqconst  4962  axprlem3  5387  sbcop1  5458  propeqop  5479  euotd  5486  rexopabb  5502  sotr2  5593  relop  5829  elinxp  6010  elimasni  6091  sotri2  6125  ordpss  6394  onmindif  6460  dffv2  6985  mpteqb  7018  elfvmptrab  7028  chfnrn  7053  elpreima  7062  iinpreima  7074  exfo  7110  ffnfv  7124  f1elima  7271  f1ounsn  7284  f1eqcocnv  7313  fliftfun  7324  soisores  7339  isotr  7348  isomin  7349  ovmpodv2  7582  difsnexi  7779  onint  7808  oneqmin  7818  ordunisuc2  7859  tfindsg  7876  findsg  7913  resf1extb  7950  f1oweALT  7988  el2mpocl  8102  poseq  8182  soseq  8183  ressuppss  8208  funsssuppss  8215  suppofssd  8228  smoiso  8378  seqomlem2  8469  oaordi  8562  oawordri  8566  oaordex  8574  oalimcl  8576  omwordi  8587  oewordi  8608  oelim2  8612  nnmwordi  8652  xpider  8817  iiner  8818  undifixp  8970  mptelixpg  8971  dom2lem  9027  findcard2s  9189  pssnn  9192  nneneq  9229  fineqvlem  9265  dif1ennnALT  9276  unfilem2  9306  domunfican  9321  f1dmvrnfibi  9338  fsuppimp  9368  dffi2  9422  infsupprpr  9505  wemaplem2  9548  suc11reg  9627  noinfep  9668  cantnflem1  9697  r1fin  9787  tcrank  9908  rankfilimbi  9909  spcdvw  9977  setrec2fun  9980  cardlim  10060  fseqenlem1  10110  alephnbtwn  10157  alephord2i  10163  alephf1  10171  cardaleph  10175  alephiso  10184  dfac12lem2  10230  ackbij1lem16  10319  cflm  10334  cfcoflem  10357  sornom  10362  fin23lem27  10413  isf32lem7  10444  fin17  10479  fin1a2lem2  10486  fin1a2lem4  10488  fin1a2lem6  10490  fin1a2lem9  10493  axdc3lem2  10536  zorn2lem7  10587  uniimadom  10635  inar1  10867  grothomex  10921  addcanpi  10991  mulcanpi  10992  enqer  11013  genpcd  11098  genpnmax  11099  ltexprlem4  11131  reclem3pr  11141  reclem4pr  11142  suplem2pr  11145  axpre-ltadd  11259  axpre-sup  11261  ltletr  11409  00id  11492  addn0nid  11743  mul0or  11963  prodgt02  12172  lemul1a  12178  divgt0  12192  divge0  12193  ledivp1i  12249  ltdivp1i  12250  cju  12323  nnsub  12389  nominpos  12590  nn0n0n1ge2  12681  btwnnz  12782  suprfinzcl  12820  ublbneg  13067  zmax  13079  cnref1o  13120  ltsubrp  13165  ltaddrp  13166  xrltletr  13293  qbtwnre  13336  xltnegi  13353  xnn0xadd0  13384  iccsupr  13580  icoshft  13611  difreicc  13622  iccshftri  13625  iccshftli  13627  iccdili  13629  icccntri  13631  fzen  13681  elfz1b  13734  fzofzim  13851  eluzgtdifelfzo  13869  elfzo1elm1fzo0  13910  injresinjlem  13932  injresinj  13933  flval2  13961  flval3  13962  modmuladdim  14064  modaddmodup  14084  addmodlteq  14096  fseqsupubi  14128  ssnn0fi  14135  mptnn0fsuppr  14149  sq01  14376  hashf1rn  14503  hashgt12el  14574  hashgt12el2  14575  hashfundm  14594  hash2pr  14621  hash2exprb  14623  hashge2el2difr  14633  hashtpg  14637  hash3tr  14643  lswlgt0cl  14721  ccatalpha  14747  pfxfv  14840  pfxsuff1eqwrdeq  14856  ccatopth2  14874  swrdccat  14892  swrdccat3blem  14896  reuccatpfxs1lem  14903  repsdf2  14937  repswsymball  14938  repswrevw  14946  cshweqrep  14980  cshw1  14981  2cshwcshw  14984  scshwfzeqfzo  14985  cshwcsh2id  14987  swrdco  14996  swrd2lsw  15114  2swrd2eqwrdeq  15115  wwlktovfo  15120  cjre  15315  icodiamlt  15614  reusq0  15641  o1lo1  15713  o1of2  15789  o1rlimmul  15795  zsum  15893  modfsummods  15969  zprod  16113  reeff1  16297  dvdsmod0  16437  dvds2lem  16447  muldvds1  16459  dvdscmulr  16463  dvdsmulcr  16464  dvdsdivcl  16495  mod2eq1n2dvds  16526  oddnn02np1  16527  divalglem8  16579  ndvdsadd  16589  zeqzmulgcd  16691  dfgcd2  16728  absproddvds  16801  lcmftp  16820  coprmdvds  16837  2mulprm  16877  isprm5  16892  divgcdodd  16895  isprm6  16899  prmdvdsexpr  16902  prmdvdsbc  16911  cncongrprm  16914  phiprmpw  16962  modprm0  16992  pythagtriplem4  17006  pcz  17068  difsqpwdvds  17074  1arith  17114  prmgaplem5  17242  prmgaplem6  17243  cshwrepswhash1  17289  sbcie2s  17348  divsfval  17728  catsubcat  18023  fthmon  18113  isinitoi  18183  istermoi  18184  iszeroi  18193  setcmon  18271  setcepi  18272  funcestrcsetclem8  18330  fthestrcsetc  18333  funcsetcestrclem8  18345  fthsetcestrc  18348  odupos  18509  pltnle  18519  pltval3  18520  lublecllem  18541  latasym  18626  mrelatglb  18743  mrelatlub  18745  cnvpsb  18762  chninf  18818  mgmpropd  18838  0gisid  18857  isgrpid2  19196  ghmghmrn  19458  ghmf1  19469  kerf1ghm  19470  orbsta  19536  resscntz  19556  gsmsymgrfixlem1  19650  gsmsymgreqlem2  19654  mndodcongi  19766  odf1  19785  lsmss1  19888  lsmss2  19890  efgredeu  19975  cntzcmnss  20064  imasabl  20099  lt6abl  20118  ablfaclem3  20312  ogrpaddlt  20361  ringinvnz1ne0  20540  crngrhmfo  20735  0ringnnzr  20785  subrngringnsg  20814  srhmsubc  20941  domnmuln0  20970  isdrng3lem2  21015  lspsneq  21409  lspsneu  21410  lsmcv  21428  rnglidlmcl  21504  rngqiprngimf1lem  21599  lidldvgen  21667  domnchr  21847  znf1o  21866  zntoslem  21871  znfld  21875  cygznlem2a  21882  cygznlem3  21884  phlssphl  21974  islindf4  22153  uvcendim  22162  lindsenlbs  22166  psdmul  22496  ply1scln0  22619  gsummoncoe1  22635  matvscl  22755  scmataddcl  22840  scmatsubcl  22841  scmatfo  22854  scmatghm  22857  maducoeval2  22964  matunitlindf  23005  slesolinv  23007  cramerimplem2  23011  cpmatelimp  23039  cpmatelimp2  23041  cpmatacl  23043  cpmatinvcl  23044  pm2mpf1  23126  cayhamlem1  23193  cayleyhamilton1  23219  0ntr  23398  islpi  23476  lmss  23625  cmpcld  23729  cmpfi  23735  1stcelcls  23789  comppfsc  23860  ptcnplem  23949  qtophmeo  24145  fbdmn0  24162  fbasrn  24212  elfm3  24278  fmfnfmlem4  24285  fclscf  24353  cnpfcf  24369  alexsubALTlem3  24377  tsmsres  24472  blval2  24890  tnggrpr  24983  nmoleub  25059  nmhmcn  25450  ncvs1  25487  iscau4  25609  caussi  25627  cmssmscld  25680  cmslssbn  25702  cniccbdd  25791  ovoliunnul  25837  mbfinf  25995  itg2splitlem  26078  dvcn  26250  c1lip1  26326  c1lip3  26328  dvcnvrelem1  26346  dvfsumlem2  26356  ply1divex  26464  quotcan  26641  aannenlem1  26664  taylf  26697  taylthlem2  26710  ulmcaulem  26730  ulmcau  26731  reeff1o  26783  logccv  27000  rtprmirr  27097  logreclem  27099  isosctrlem2  27156  xrlimcnp  27305  rlimcxp  27310  ftalem7  27415  vmappw  27452  fsumdvdsmul  27531  fsumvma  27549  dchreq  27594  dchrptlem1  27600  dchrsum  27605  bposlem7  27626  lgsqrlem2  27683  lgsdchr  27691  gausslemma2dlem1a  27701  lgseisenlem2  27712  lgsquad2  27722  2lgslem1b  27728  2sqlem6  27759  2sqnn0  27774  addsq2reu  27776  2sqreulem2  27788  ltsval2  28022  ltsres  28028  nodenselem8  28057  nodense  28058  noresle  28063  cutsun12  28185  madeval2  28228  elmade  28252  negsf1o  28449  muls0ord  28580  recsex  28614  bdayons  28671  addonbday  28674  noseqrdgfn  28701  n0subs  28758  eln0zs  28795  zsoring  28804  bdayfinbndlem1  28862  z12bdaylem1  28865  tgcgrcomimp  28948  isperp2  29199  xmstrkgc  29472  brbtwn  29486  brcgr  29487  axcgrid  29503  axeuclidlem  29549  axeuclid  29550  elntg2  29572  lpvtx  29655  upgrex  29679  upgrpredgv  29726  upgredgpr  29729  uhgr0v0e  29828  subgrprop  29863  fusgrfisbase  29918  edgnbusgreu  29957  nbusgredgeu0  29958  cusgredg  30014  structtocusgr  30036  cusgrsize2inds  30043  cusgrsize  30044  usgredgsscusgredg  30049  fusgrmaxsize  30054  uspgrloopvtxel  30106  umgr2v2e  30115  vtxdginducedm1fi  30134  finsumvtxdg2sstep  30139  rgrprop  30150  rusgrprop  30152  0uhgrrusgr  30168  rusgrpropedg  30174  ewlkprop  30193  upgrewlkle2  30196  wlkprop  30201  upgrwlkcompim  30232  uspgr2wlkeq  30235  wlklenvclwlk  30243  wlkonprop  30246  wlkres  30258  redwlk  30260  wlkdlem2  30271  pfxwlk  30275  subgrwlk  30278  wksonproplem  30296  usgr2trlspth  30356  usgr2pth  30359  pthdlem1  30361  crctcshwlkn0lem4  30411  wwlksnprcl  30437  wlkiswwlks2  30473  wwlksm1edg  30479  wlknewwlksn  30485  wwlksnred  30490  wwlksnextbi  30492  wwlksnextwrd  30495  wwlksnextinj  30497  wwlksnextsurj  30498  umgr2wlk  30547  usgrwwlks2on  30556  umgrwwlks2on  30557  elwwlks2  30567  clwwlk1loop  30588  umgrclwwlkge2  30591  clwlkclwwlklem2a1  30592  clwlkclwwlklem2a4  30597  clwlkclwwlklem2a  30598  clwlkclwwlklem2  30600  clwlkclwwlkfo  30609  clwwisshclwwslemlem  30613  clwwlknwwlksn  30638  clwwlknlbonbgr1  30639  clwwlkn1loopb  30643  clwwlkf  30647  clwwlknon1  30697  clwwlknonwwlknonb  30706  clwwlknonex2lem2  30708  loop1cycl  30753  vdn0conngrumgrv2  30806  frgrnbnb  30903  frgrncvvdeqlem2  30910  frgrncvvdeqlem3  30911  frgrncvvdeqlem6  30914  frgrwopreglem4a  30920  fusgr2wsp2nb  30944  frrusgrord0lem  30949  numclwwlk2lem1lem  30952  2clwwlk2clwwlklem  30956  2clwwlk2clwwlk  30960  numclwwlk1lem2foa  30964  numclwwlk1lem2f1  30967  frgrreg  31004  hlipgt0  31525  ocin  31907  ocnel  31909  shmodsi  32000  pjmf1  32327  unopf1o  32527  staddi  32857  stadd3i  32859  mdi  32906  dmdmd  32911  dmdi  32913  dmdbr2  32914  dmdbr3  32916  dmdbr4  32917  dmdi4  32918  mdsl1i  32932  superpos  32965  cvbr4i  32978  atssma  32989  atcv1  32991  atomli  32993  chirredlem1  33001  addltmulALT  33099  ifeqeqx  33189  disjxpin  33233  suppss3  33365  fpwrelmap  33375  expgt0b  33458  mndlactfo  33638  mndractfo  33640  qsfld  34072  ply1degltdimlem  34304  ply1degltdim  34305  metider  34576  tpr2rico  34594  xrge0iifiso  34617  qqhcn  34673  qqhucn  34674  esumlub  34742  esumpinfval  34755  esumpinfsum  34759  ballotlemfc0  35175  ballotlemfcc  35176  ftc2re  35277  bnj517  35565  soinfdom  35774  fnrelpredd  35778  axsepg2  35876  axsepg3  35877  axsepg3ALT  35878  axsepg4  35879  axsepg5  35880  axnulg  35881  srepdflem1  36036  erdsze2lem2  36087  satfv1  36246  satfdmlem  36251  satf0op  36260  fmlasuc  36269  dfrdg4  36839  altopthsn  36850  btwncomim  36902  btwnexch3  36909  btwnexch2  36912  endofsegid  36974  opnrebl2  37233  nn0prpwlem  37234  onsuct0  37353  ordcmp  37359  nndivsub  37369  regsfromunir1  37452  dnibndlem13  37480  bj-cbvexvv  37663  bj-cbval  37669  bj-cbvex  37670  bj-cbvexw  37700  bj-nnf-cbval  37806  bj-cbv3tb  37823  bj-spimtv  37830  bj-equsal  37862  bj-sbsb  37873  bj-vtoclf  37951  bj-sepg  37960  bj-gabss  37972  bj-gabeqd  37974  currysetlem2  37985  bj-snsetex  38000  bj-axseprep  38126  bj-ismooredr2  38167  bj-inftyexpiinj  38267  bj-finsumval0  38343  bj-fvimacnv0  38344  bj-bary1lem1  38369  bj-bary1  38370  f1omptsnlem  38396  iooelexlt  38422  relowlpssretop  38424  rdgeqoa  38430  finxpsuclem  38457  fvineqsneq  38472  pibt2  38477  wl-isseteq  38565  wl-dfcleq  38574  wl-equsal1i  38613  ltflcei  38668  sin2h  38670  cos2h  38671  tan2h  38672  poimirlem3  38678  poimirlem4  38679  poimirlem18  38693  poimirlem20  38695  poimirlem21  38696  poimirlem22  38697  poimirlem24  38699  poimirlem25  38700  poimirlem26  38701  poimirlem27  38702  poimirlem28  38703  poimirlem31  38706  poimir  38708  heicant  38710  mblfinlem1  38712  mblfinlem2  38713  mblfinlem3  38714  mblfinlem4  38715  mbfresfi  38721  cnambfre  38723  ftc1anc  38756  dvasin  38759  areacirclem1  38763  areacirclem4  38766  areacirc  38768  findcard4  38769  brabg2  38788  fzmul  38812  fdc  38816  incsequz2  38820  isbnd2  38854  opidonOLD  38923  opidon2OLD  38925  grpomndo  38946  elghomlem2OLD  38957  rngoueqz  39011  dvrunz  39025  divrngidl  39099  refressn  39602  dral1-o  40098  lsatn0  40193  l1cvpat  40248  leat2  40488  atnle  40511  cvlcvr1  40533  cvrexchlem  40613  cvratlem  40615  cvrat  40616  atcvrj0  40622  atle  40630  snatpsubN  40944  linepsubN  40946  pmapsub  40962  lneq2at  40972  lncvrelatN  40975  2llnma3r  40982  cdlemblem  40987  paddasslem5  41018  poml4N  41147  lhpmcvr4N  41220  trlval2  41357  cdlemd6  41397  cdleme7ga  41442  cdleme25b  41548  cdleme29b  41569  cdleme35fnpq  41643  cdleme50f1  41737  cdlemf1  41755  cdlemg27b  41890  cdlemk28-3  42102  tendospcanN  42217  diaf11N  42243  dia2dimlem1  42258  dibf11N  42355  dihf11  42461  dihmeetlem1N  42484  dochvalr  42551  dochnel2  42586  dvh4dimlem  42637  dochsat0  42651  mapd1o  42842  hdmapf1oN  43059  hgmapval0  43086  hgmapf1oN  43097  hlhilhillem  43154  nnproddivdvdsd  43187  lcmineqlem  43239  aks4d1p1p5  43262  aks4d1p3  43265  aks4d1p8d2  43272  aks4d1p8  43274  aks4d1p9  43275  fldhmf1  43277  isprimroot2  43281  primrootsunit1  43284  primrootscoprmpow  43286  posbezout  43287  primrootscoprbij  43289  primrootlekpowne0  43292  primrootspoweq0  43293  aks6d1c1p1  43294  aks6d1c1p2  43296  aks6d1c1p3  43297  aks6d1c1p4  43298  aks6d1c1p5  43299  aks6d1c1p7  43300  aks6d1c1p6  43301  aks6d1c1p8  43302  aks6d1c2p2  43306  aks6d1c2lem3  43313  aks6d1c2lem4  43314  hashnexinj  43315  aks6d1c2  43317  aks6d1c5lem0  43322  aks6d1c5lem1  43323  aks6d1c5  43326  sticksstones1  43333  sticksstones3  43335  sticksstones8  43340  sticksstones11  43343  sticksstones12  43345  sticksstones20  43353  sticksstones22  43355  aks6d1c6lem3  43359  aks6d1c6lem4  43360  aks6d1c6isolem1  43361  aks6d1c6isolem2  43362  aks6d1c6lem5  43364  aks6d1c7  43371  rhmqusspan  43372  unitscyglem2  43383  unitscyglem3  43384  aks5lem8  43388  sn-axprlem3  43409  oexpreposd  43516  sn-remul0ord  43596  frlmsnic  43741  fsuppind  43755  prjspval  43768  rexrabdioph  43938  fphpdo  43961  irrapxlem3  43968  rmxypairf1o  44055  rmxycomplete  44061  zindbi  44090  lermxnn0  44094  ltrmy  44096  rmyeq0  44097  rmyeq  44098  lermy  44099  acongsym  44120  acongneg2  44121  wepwsolem  44186  onsupuni  44368  onsupmaxb  44378  onsucf1o  44411  onov0suclim  44413  oe0suclim  44416  onsucwordi  44427  cantnfresb  44463  omabs2  44471  tfsconcat0b  44485  tfsconcatrev  44487  naddcnffo  44503  oaun3lem1  44513  oaltom  44543  omltoe  44545  sdomne0  44551  sdomne0d  44552  safesnsupfidom1o  44555  intabssd  44657  iscard4  44671  ss2iundf  44796  frege129d  44900  frege133d  44902  axfrege52a  44993  axfrege52c  45024  ntrk0kbimka  45176  gneispace  45271  suprleubrd  45303  suprlubrd  45305  radcnvrat  45435  nzss  45438  expgrowthi  45454  bi23impib  45605  rspsbc2  45653  tratrb  45655  sbcim2g  45657  truniALT  45660  3impcombi  45935  tpid3gVD  45960  orbi1rVD  45966  sbc3orgVD  45969  rspsbc2VD  45973  tratrbVD  45979  sbcim2gVD  45993  sbcbiVD  45994  truniALTVD  45996  trintALTVD  45998  trintALT  45999  csbingVD  46002  csbsngVD  46011  csbxpgVD  46012  csbresgVD  46013  csbrngVD  46014  csbima12gALTVD  46015  csbunigVD  46016  csbfv12gALTVD  46017  relopabVD  46019  isosctrlem1ALT  46052  relpfrlem  46079  trfr  46088  fzisoeu  46452  xrralrecnnge  46537  allbutfi  46540  climinf  46754  liminfreuzlem  46948  climliminf  46952  climliminflimsup  46954  xlimpnfxnegmnf  46960  xlimbr  46973  stoweidlem7  47153  stoweidlem62  47208  sge0gerpmpt  47548  meaiuninclem  47626  carageniuncllem2  47668  issmflem  47873  et-sqrtnegnre  48019  ormkglobd  48023  tmachlem-agreeprod  48083  funressnfv  48249  funressnvmo  48251  f1cof1b  48283  2reu3  48317  ralbinrald  48329  afv0fv0  48355  afv0nbfvbi  48357  afvfv0bi  48358  fnbrafvb  48360  afvres  48378  tz6.12-afv  48379  afvco2  48382  ndmaovcl  48409  afv2res  48445  tz6.12-afv2  48446  nelbrim  48481  f1oresf1o2  48497  zm1nn  48508  nltle2tri  48519  subsubelfzo0  48533  2tceilhalfelfzo1  48542  iccpartres  48636  iccpartiltu  48640  fargshiftfv  48657  ichnreuop  48690  ichreuopeq  48691  prsprel  48705  sprsymrelf1lem  48709  sprsymrelfolem2  48711  sprsymrelfo  48715  prpair  48719  paireqne  48729  sbcpr  48739  nprmmul2  48746  nprmmul3  48747  fmtnof1  48756  goldbachthlem2  48767  fmtnoprmfac1  48786  fmtnoprmfac2  48788  lighneallem2  48827  lighneallem4b  48830  lighneallem4  48831  evennodd  48877  oddneven  48878  oexpnegnz  48912  evenltle  48951  fpprwppr  48973  fpprwpprb  48974  gbowge7  48997  gbege6  48999  sbgoldbwt  49011  sbgoldbst  49012  nnsum3primesle9  49028  bgoldbtbndlem2  49040  grimprop  49117  isuspgrimlem  49129  uhgrimisgrgriclem  49164  clnbgrgrimlem  49167  grtriproplem  49173  isgrtri  49177  grimgrtri  49183  stgr1  49195  isubgr3stgr  49209  grlimprop  49218  uspgrlimlem2  49223  uspgrlimlem3  49224  grlimprclnbgr  49230  gpg5nbgrvtx13starlem1  49305  clintop  49441  isassintop  49443  lidldomn1  49464  uzlidlring  49468  2zrngnmlid2  49490  rngccatidALTV  49505  ringccatidALTV  49539  srhmsubcALTV  49558  ztprmneprm  49595  pgrpgt2nabl  49614  lindslinindimp2lem4  49709  lincresunit3  49729  fldivexpfllog2  49813  digexp  49855  naryfvalelfv  49880  affinecomb1  49950  eenglngeehlnmlem1  49986  eenglngeehlnmlem2  49987  itscnhlc0yqe  50007  itsclc0yqsol  50012  itscnhlc0xyqsol  50013  itschlc0xyqsol1  50014  itschlc0xyqsol  50015  itsclquadeu  50025  inlinecirc02plem  50034  inlinecirc02p  50035  mofsn  50091  seposep  50176  resipos  50225  idmon  50270  idepi  50271  prsthinc  50735  grptcmon  50867  grptcepi  50868  spd  50997