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  2023  spfw  2068  cbvalw  2070  sbequiOLD  2123  chvarfv  2280  cbvalv1  2374  spv  2425  chvar  2427  cbval  2430  sb1  2510  nfsb4t  2531  exmoeu  2609  euim  2645  2eu3  2681  ralbida  3277  rgen2a  3360  ralcom2  3366  ceqsalt  3487  ceqsalgALT  3490  spcimgft  3514  spcdv  3552  rspcdv  3572  rspcebdv  3574  rexraleqim  3604  sbcn1  3794  sbcbi1  3799  sbeqalb  3804  sbcel21v  3809  elpwunsn  4646  rabsnifsb  4685  ssunsn2  4788  preqr1g  4812  iuneqconst  4968  axprlem3  5394  sbcop1  5465  propeqop  5486  euotd  5493  rexopabb  5509  sotr2  5600  relopabi  5809  relop  5838  elinxp  6026  elimasni  6107  sotri2  6141  ordpss  6417  onmindif  6483  dffv2  7011  mpteqb  7044  elfvmptrab  7054  chfnrn  7079  elpreimaOLD  7089  iinpreima  7101  exfo  7137  ffnfv  7151  f1elima  7298  f1ounsn  7311  f1eqcocnv  7340  fliftfun  7351  soisores  7366  isotr  7375  isomin  7376  ovmpodv2  7610  difsnexi  7807  onint  7838  oneqmin  7848  ordunisuc2  7889  tfindsg  7906  findsg  7943  resf1extb  7980  f1oweALT  8018  el2mpocl  8132  poseq  8212  soseq  8213  ressuppss  8238  funsssuppss  8245  suppofssd  8258  smoiso  8408  seqomlem2  8499  oaordi  8592  oawordri  8596  oaordex  8604  oalimcl  8606  omwordi  8617  oewordi  8638  oelim2  8642  nnmwordi  8682  xpider  8847  iiner  8848  undifixp  9000  mptelixpg  9001  dom2lem  9057  findcard2s  9219  pssnn  9222  nneneq  9259  fineqvlem  9295  dif1ennnALT  9306  unfilem2  9336  domunfican  9351  f1dmvrnfibi  9368  fsuppimp  9398  dffi2  9452  infsupprpr  9535  wemaplem2  9578  suc11reg  9657  noinfep  9698  cantnflem1  9727  r1fin  9817  tcrank  9938  rankfilimbi  9939  spcdvw  10007  setrec2fun  10010  cardlim  10090  fseqenlem1  10142  alephnbtwn  10189  alephord2i  10195  alephf1  10203  cardaleph  10207  alephiso  10216  dfac12lem2  10262  ackbij1lem16  10351  cflm  10366  cfcoflem  10389  sornom  10394  fin23lem27  10445  isf32lem7  10476  fin17  10511  fin1a2lem2  10518  fin1a2lem4  10520  fin1a2lem6  10522  fin1a2lem9  10525  axdc3lem2  10568  zorn2lem7  10619  uniimadom  10667  inar1  10899  grothomex  10953  addcanpi  11023  mulcanpi  11024  enqer  11045  genpcd  11130  genpnmax  11131  ltexprlem4  11163  reclem3pr  11173  reclem4pr  11174  suplem2pr  11177  axpre-ltadd  11291  axpre-sup  11293  ltletr  11441  00id  11524  addn0nid  11775  mul0or  11996  prodgt02  12205  lemul1a  12211  divgt0  12225  divge0  12226  ledivp1i  12282  ltdivp1i  12283  cju  12356  nnsub  12422  nominpos  12623  nn0n0n1ge2  12714  btwnnz  12815  suprfinzcl  12853  ublbneg  13100  zmax  13112  cnref1o  13153  ltsubrp  13198  ltaddrp  13199  xrltletr  13326  qbtwnre  13369  xltnegi  13386  xnn0xadd0  13417  iccsupr  13613  icoshft  13644  difreicc  13655  iccshftri  13658  iccshftli  13660  iccdili  13662  icccntri  13664  fzen  13714  elfz1b  13767  fzofzim  13884  eluzgtdifelfzo  13902  elfzo1elm1fzo0  13943  injresinjlem  13965  injresinj  13966  flval2  13994  flval3  13995  modmuladdim  14097  modaddmodup  14117  addmodlteq  14129  fseqsupubi  14161  ssnn0fi  14168  mptnn0fsuppr  14182  sq01  14410  hashf1rn  14537  hashgt12el  14608  hashgt12el2  14609  hashfundm  14628  hash2pr  14655  hash2exprb  14657  hashge2el2difr  14667  hashtpg  14671  hash3tr  14677  lswlgt0cl  14755  ccatalpha  14781  pfxfv  14874  pfxsuff1eqwrdeq  14890  ccatopth2  14908  swrdccat  14926  swrdccat3blem  14930  reuccatpfxs1lem  14937  repsdf2  14971  repswsymball  14972  repswrevw  14980  cshweqrep  15014  cshw1  15015  2cshwcshw  15018  scshwfzeqfzo  15019  cshwcsh2id  15021  swrdco  15030  swrd2lsw  15148  2swrd2eqwrdeq  15149  wwlktovfo  15154  cjre  15349  icodiamlt  15649  reusq0  15676  o1lo1  15748  o1of2  15824  o1rlimmul  15830  zsum  15928  modfsummods  16004  zprod  16148  reeff1  16332  dvdsmod0  16472  dvds2lem  16482  muldvds1  16494  dvdscmulr  16498  dvdsmulcr  16499  dvdsdivcl  16530  mod2eq1n2dvds  16561  oddnn02np1  16562  divalglem8  16614  ndvdsadd  16624  zeqzmulgcd  16726  dfgcd2  16763  absproddvds  16836  lcmftp  16855  coprmdvds  16872  2mulprm  16912  isprm5  16927  divgcdodd  16930  isprm6  16934  prmdvdsexpr  16937  prmdvdsbc  16946  cncongrprm  16949  phiprmpw  16997  modprm0  17027  pythagtriplem4  17041  pcz  17103  difsqpwdvds  17109  1arith  17149  prmgaplem5  17277  prmgaplem6  17278  cshwrepswhash1  17324  sbcie2s  17383  divsfval  17769  catsubcat  18064  fthmon  18154  isinitoi  18224  istermoi  18225  iszeroi  18234  setcmon  18312  setcepi  18313  funcestrcsetclem8  18371  fthestrcsetc  18374  funcsetcestrclem8  18386  fthsetcestrc  18389  odupos  18550  pltnle  18560  pltval3  18561  lublecllem  18582  latasym  18667  mrelatglb  18784  mrelatlub  18786  cnvpsb  18803  chninf  18859  mgmpropd  18879  0gisid  18898  isgrpid2  19237  ghmghmrn  19499  ghmf1  19510  kerf1ghm  19511  orbsta  19578  resscntz  19598  gsmsymgrfixlem1  19692  gsmsymgreqlem2  19696  mndodcongi  19808  odf1  19827  lsmss1  19930  lsmss2  19932  efgredeu  20017  cntzcmnss  20106  imasabl  20141  lt6abl  20160  ablfaclem3  20354  ogrpaddlt  20403  ringinvnz1ne0  20582  crngrhmfo  20777  0ringnnzr  20827  subrngringnsg  20856  srhmsubc  20983  domnmuln0  21012  isdrng3lem2  21057  lspsneq  21451  lspsneu  21452  lsmcv  21470  rnglidlmcl  21546  rngqiprngimf1lem  21641  lidldvgen  21709  domnchr  21893  znf1o  21912  zntoslem  21917  znfld  21921  cygznlem2a  21928  cygznlem3  21930  phlssphl  22020  islindf4  22199  uvcendim  22208  lindsenlbs  22212  psdmul  22542  ply1scln0  22665  gsummoncoe1  22681  matvscl  22801  scmataddcl  22886  scmatsubcl  22887  scmatfo  22900  scmatghm  22903  maducoeval2  23010  matunitlindf  23051  slesolinv  23053  cramerimplem2  23057  cpmatelimp  23085  cpmatelimp2  23087  cpmatacl  23089  cpmatinvcl  23090  pm2mpf1  23172  cayhamlem1  23239  cayleyhamilton1  23265  0ntr  23444  islpi  23522  lmss  23671  cmpcld  23775  cmpfi  23781  1stcelcls  23835  comppfsc  23906  ptcnplem  23995  qtophmeo  24191  fbdmn0  24208  fbasrn  24258  elfm3  24324  fmfnfmlem4  24331  fclscf  24399  cnpfcf  24415  alexsubALTlem3  24423  tsmsres  24518  blval2  24936  tnggrpr  25029  nmoleub  25105  nmhmcn  25496  ncvs1  25533  iscau4  25655  caussi  25673  cmssmscld  25726  cmslssbn  25748  cniccbdd  25837  ovoliunnul  25883  mbfinf  26041  itg2splitlem  26124  dvcn  26296  c1lip1  26372  c1lip3  26374  dvcnvrelem1  26392  dvfsumlem2  26402  ply1divex  26510  quotcan  26687  aannenlem1  26712  taylf  26745  taylthlem2  26758  ulmcaulem  26778  ulmcau  26779  reeff1o  26831  logccv  27048  rtprmirr  27145  logreclem  27147  isosctrlem2  27204  xrlimcnp  27353  rlimcxp  27358  ftalem7  27463  vmappw  27500  fsumdvdsmul  27579  fsumvma  27597  dchreq  27642  dchrptlem1  27648  dchrsum  27653  bposlem7  27674  lgsqrlem2  27731  lgsdchr  27739  gausslemma2dlem1a  27749  lgseisenlem2  27760  lgsquad2  27770  2lgslem1b  27776  2sqlem6  27807  2sqnn0  27822  addsq2reu  27824  2sqreulem2  27836  ltsval2  28070  ltsres  28076  nodenselem8  28105  nodense  28106  noresle  28111  cutsun12  28233  madeval2  28276  elmade  28300  negsf1o  28497  muls0ord  28628  recsex  28662  bdayons  28719  addonbday  28722  noseqrdgfn  28749  n0subs  28806  eln0zs  28843  zsoring  28852  bdayfinbndlem1  28910  z12bdaylem1  28913  tgcgrcomimp  28996  isperp2  29247  xmstrkgc  29520  brbtwn  29534  brcgr  29535  axcgrid  29551  axeuclidlem  29597  axeuclid  29598  elntg2  29620  lpvtx  29703  upgrex  29727  upgrpredgv  29774  upgredgpr  29777  uhgr0v0e  29876  subgrprop  29911  fusgrfisbase  29966  edgnbusgreu  30005  nbusgredgeu0  30006  cusgredg  30062  structtocusgr  30084  cusgrsize2inds  30091  cusgrsize  30092  usgredgsscusgredg  30097  fusgrmaxsize  30102  uspgrloopvtxel  30154  umgr2v2e  30163  vtxdginducedm1fi  30182  finsumvtxdg2sstep  30187  rgrprop  30198  rusgrprop  30200  0uhgrrusgr  30216  rusgrpropedg  30222  ewlkprop  30241  upgrewlkle2  30244  wlkprop  30249  upgrwlkcompim  30280  uspgr2wlkeq  30283  wlklenvclwlk  30291  wlkonprop  30294  wlkres  30306  redwlk  30308  wlkdlem2  30319  pfxwlk  30323  subgrwlk  30326  wksonproplem  30344  usgr2trlspth  30404  usgr2pth  30407  pthdlem1  30409  crctcshwlkn0lem4  30459  wwlksnprcl  30485  wlkiswwlks2  30521  wwlksm1edg  30527  wlknewwlksn  30533  wwlksnred  30538  wwlksnextbi  30540  wwlksnextwrd  30543  wwlksnextinj  30545  wwlksnextsurj  30546  umgr2wlk  30595  usgrwwlks2on  30604  umgrwwlks2on  30605  elwwlks2  30615  clwwlk1loop  30636  umgrclwwlkge2  30639  clwlkclwwlklem2a1  30640  clwlkclwwlklem2a4  30645  clwlkclwwlklem2a  30646  clwlkclwwlklem2  30648  clwlkclwwlkfo  30657  clwwisshclwwslemlem  30661  clwwlknwwlksn  30686  clwwlknlbonbgr1  30687  clwwlkn1loopb  30691  clwwlkf  30695  clwwlknon1  30745  clwwlknonwwlknonb  30754  clwwlknonex2lem2  30756  loop1cycl  30801  vdn0conngrumgrv2  30854  frgrnbnb  30951  frgrncvvdeqlem2  30958  frgrncvvdeqlem3  30959  frgrncvvdeqlem6  30962  frgrwopreglem4a  30968  fusgr2wsp2nb  30992  frrusgrord0lem  30997  numclwwlk2lem1lem  31000  2clwwlk2clwwlklem  31004  2clwwlk2clwwlk  31008  numclwwlk1lem2foa  31012  numclwwlk1lem2f1  31015  frgrreg  31052  hlipgt0  31573  ocin  31955  ocnel  31957  shmodsi  32048  pjmf1  32375  unopf1o  32575  staddi  32905  stadd3i  32907  mdi  32954  dmdmd  32959  dmdi  32961  dmdbr2  32962  dmdbr3  32964  dmdbr4  32965  dmdi4  32966  mdsl1i  32980  superpos  33013  cvbr4i  33026  atssma  33037  atcv1  33039  atomli  33041  chirredlem1  33049  addltmulALT  33147  ifeqeqx  33236  disjxpin  33280  suppss3  33411  fpwrelmap  33421  expgt0b  33504  mndlactfo  33687  mndractfo  33689  qsfld  34126  ply1degltdimlem  34365  ply1degltdim  34366  metider  34637  tpr2rico  34655  xrge0iifiso  34678  qqhcn  34734  qqhucn  34735  esumlub  34803  esumpinfval  34816  esumpinfsum  34820  ballotlemfc0  35236  ballotlemfcc  35237  ftc2re  35338  bnj517  35626  soinfdom  35841  fnrelpredd  35845  axsepg2  35949  axsepg3  35950  axsepg3ALT  35951  axsepg4  35952  axsepg5  35953  axnulg  35954  srepdflem1  36126  erdsze2lem2  36177  satfv1  36336  satfdmlem  36341  satf0op  36350  fmlasuc  36359  dfrdg4  36930  altopthsn  36941  btwncomim  36993  btwnexch3  37000  btwnexch2  37003  endofsegid  37065  opnrebl2  37324  nn0prpwlem  37325  onsuct0  37444  ordcmp  37450  nndivsub  37460  regsfromunir1  37543  dnibndlem13  37571  bj-cbvexvv  37754  bj-cbval  37760  bj-cbvex  37761  bj-cbvexw  37791  bj-nnf-cbval  37897  bj-cbv3tb  37914  bj-spimtv  37921  bj-equsal  37953  bj-sbsb  37964  bj-vtoclf  38042  bj-sepg  38051  bj-gabss  38063  bj-gabeqd  38065  currysetlem2  38076  bj-snsetex  38091  bj-axseprep  38260  bj-ismooredr2  38301  bj-inftyexpiinj  38398  bj-finsumval0  38474  bj-fvimacnv0  38475  bj-bary1lem1  38500  bj-bary1  38501  f1omptsnlem  38527  iooelexlt  38553  relowlpssretop  38555  rdgeqoa  38561  finxpsuclem  38588  fvineqsneq  38603  pibt2  38608  wl-isseteq  38696  wl-dfcleq  38705  wl-equsal1i  38744  ltflcei  38799  sin2h  38801  cos2h  38802  tan2h  38803  poimirlem3  38809  poimirlem4  38810  poimirlem18  38824  poimirlem20  38826  poimirlem21  38827  poimirlem22  38828  poimirlem24  38830  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  poimirlem28  38834  poimirlem31  38837  poimir  38839  heicant  38841  mblfinlem1  38843  mblfinlem2  38844  mblfinlem3  38845  mblfinlem4  38846  mbfresfi  38852  cnambfre  38854  ftc1anc  38887  dvasin  38890  areacirclem1  38894  areacirclem4  38897  areacirc  38899  findcard4  38900  brabg2  38919  fzmul  38941  fdc  38945  incsequz2  38949  isbnd2  38983  opidonOLD  39052  opidon2OLD  39054  grpomndo  39075  elghomlem2OLD  39086  rngoueqz  39140  dvrunz  39154  divrngidl  39228  refressn  39731  dral1-o  40227  lsatn0  40322  l1cvpat  40377  leat2  40617  atnle  40640  cvlcvr1  40662  cvrexchlem  40742  cvratlem  40744  cvrat  40745  atcvrj0  40751  atle  40759  snatpsubN  41073  linepsubN  41075  pmapsub  41091  lneq2at  41101  lncvrelatN  41104  2llnma3r  41111  cdlemblem  41116  paddasslem5  41147  poml4N  41276  lhpmcvr4N  41349  trlval2  41486  cdlemd6  41526  cdleme7ga  41571  cdleme25b  41677  cdleme29b  41698  cdleme35fnpq  41772  cdleme50f1  41866  cdlemf1  41884  cdlemg27b  42019  cdlemk28-3  42231  tendospcanN  42346  diaf11N  42372  dia2dimlem1  42387  dibf11N  42484  dihf11  42590  dihmeetlem1N  42613  dochvalr  42680  dochnel2  42715  dvh4dimlem  42766  dochsat0  42780  mapd1o  42971  hdmapf1oN  43188  hgmapval0  43215  hgmapf1oN  43226  hlhilhillem  43283  nnproddivdvdsd  43316  lcmineqlem  43368  aks4d1p1p5  43391  aks4d1p3  43394  aks4d1p8d2  43401  aks4d1p8  43403  aks4d1p9  43404  fldhmf1  43406  isprimroot2  43410  primrootsunit1  43413  primrootscoprmpow  43415  posbezout  43416  primrootscoprbij  43418  primrootlekpowne0  43421  primrootspoweq0  43422  aks6d1c1p1  43423  aks6d1c1p2  43425  aks6d1c1p3  43426  aks6d1c1p4  43427  aks6d1c1p5  43428  aks6d1c1p7  43429  aks6d1c1p6  43430  aks6d1c1p8  43431  aks6d1c2p2  43435  aks6d1c2lem3  43442  aks6d1c2lem4  43443  hashnexinj  43444  aks6d1c2  43446  aks6d1c5lem0  43451  aks6d1c5lem1  43452  aks6d1c5  43455  sticksstones1  43462  sticksstones3  43464  sticksstones8  43469  sticksstones11  43472  sticksstones12  43474  sticksstones20  43482  sticksstones22  43484  aks6d1c6lem3  43488  aks6d1c6lem4  43489  aks6d1c6isolem1  43490  aks6d1c6isolem2  43491  aks6d1c6lem5  43493  aks6d1c7  43500  rhmqusspan  43501  unitscyglem2  43512  unitscyglem3  43513  aks5lem8  43517  sn-axprlem3  43539  oexpreposd  43645  sn-remul0ord  43725  frlmsnic  43870  fsuppind  43884  prjspval  43897  rexrabdioph  44067  fphpdo  44090  irrapxlem3  44097  rmxypairf1o  44184  rmxycomplete  44190  zindbi  44219  lermxnn0  44223  ltrmy  44225  rmyeq0  44226  rmyeq  44227  lermy  44228  acongsym  44249  acongneg2  44250  wepwsolem  44315  onsupuni  44492  onsupmaxb  44502  onsucf1o  44535  onov0suclim  44537  oe0suclim  44540  onsucwordi  44551  cantnfresb  44587  omabs2  44595  tfsconcat0b  44609  tfsconcatrev  44611  naddcnffo  44627  oaun3lem1  44637  oaltom  44667  omltoe  44669  sdomne0  44675  sdomne0d  44676  safesnsupfidom1o  44679  intabssd  44781  iscard4  44795  ss2iundf  44920  frege129d  45024  frege133d  45026  axfrege52a  45117  axfrege52c  45148  ntrk0kbimka  45300  gneispace  45395  suprleubrd  45427  suprlubrd  45429  radcnvrat  45559  nzss  45562  expgrowthi  45578  bi23impib  45729  rspsbc2  45777  tratrb  45779  sbcim2g  45781  truniALT  45784  3impcombi  46059  tpid3gVD  46084  orbi1rVD  46090  sbc3orgVD  46093  rspsbc2VD  46097  tratrbVD  46103  sbcim2gVD  46117  sbcbiVD  46118  truniALTVD  46120  trintALTVD  46122  trintALT  46123  csbingVD  46126  csbsngVD  46135  csbxpgVD  46136  csbresgVD  46137  csbrngVD  46138  csbima12gALTVD  46139  csbunigVD  46140  csbfv12gALTVD  46141  relopabVD  46143  isosctrlem1ALT  46176  relpfrlem  46207  trfr  46216  fzisoeu  46589  xrralrecnnge  46674  allbutfi  46677  climinf  46891  liminfreuzlem  47085  climliminf  47089  climliminflimsup  47091  xlimpnfxnegmnf  47097  xlimbr  47110  stoweidlem7  47290  stoweidlem62  47345  sge0gerpmpt  47685  meaiuninclem  47763  carageniuncllem2  47805  issmflem  48010  et-sqrtnegnre  48156  ormkglobd  48160  tmachlem-agreeprod  48220  funressnfv  48386  funressnvmo  48388  f1cof1b  48420  2reu3  48454  ralbinrald  48466  afv0fv0  48492  afv0nbfvbi  48494  afvfv0bi  48495  fnbrafvb  48497  afvres  48515  tz6.12-afv  48516  afvco2  48519  ndmaovcl  48546  afv2res  48582  tz6.12-afv2  48583  nelbrim  48618  f1oresf1o2  48634  zm1nn  48645  nltle2tri  48656  subsubelfzo0  48670  2tceilhalfelfzo1  48679  iccpartres  48773  iccpartiltu  48777  fargshiftfv  48794  ichnreuop  48827  ichreuopeq  48828  prsprel  48842  sprsymrelf1lem  48846  sprsymrelfolem2  48848  sprsymrelfo  48852  prpair  48856  paireqne  48866  sbcpr  48876  nprmmul2  48883  nprmmul3  48884  fmtnof1  48893  goldbachthlem2  48904  fmtnoprmfac1  48923  fmtnoprmfac2  48925  lighneallem2  48964  lighneallem4b  48967  lighneallem4  48968  evennodd  49014  oddneven  49015  oexpnegnz  49049  evenltle  49088  fpprwppr  49110  fpprwpprb  49111  gbowge7  49134  gbege6  49136  sbgoldbwt  49148  sbgoldbst  49149  nnsum3primesle9  49165  bgoldbtbndlem2  49177  grimprop  49254  isuspgrimlem  49266  uhgrimisgrgriclem  49301  clnbgrgrimlem  49304  grtriproplem  49310  isgrtri  49314  grimgrtri  49320  stgr1  49332  isubgr3stgr  49346  grlimprop  49355  uspgrlimlem2  49360  uspgrlimlem3  49361  grlimprclnbgr  49367  gpg5nbgrvtx13starlem1  49442  clintop  49578  isassintop  49580  lidldomn1  49601  uzlidlring  49605  2zrngnmlid2  49627  rngccatidALTV  49642  ringccatidALTV  49676  srhmsubcALTV  49695  subrgccdom  49709  ztprmneprm  49790  pgrpgt2nabl  49809  lindslinindimp2lem4  49904  lincresunit3  49924  fldivexpfllog2  50008  digexp  50050  naryfvalelfv  50075  affinecomb1  50145  eenglngeehlnmlem1  50181  eenglngeehlnmlem2  50182  itscnhlc0yqe  50202  itsclc0yqsol  50207  itscnhlc0xyqsol  50208  itschlc0xyqsol1  50209  itschlc0xyqsol  50210  itsclquadeu  50220  inlinecirc02plem  50229  inlinecirc02p  50230  mofsn  50286  seposep  50371  resipos  50420  idmon  50465  idepi  50466  prsthinc  50930  grptcmon  51062  grptcepi  51063  spd  51192