Theorem biimpd 230

Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 216 and biimpi 217. (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 216	. 2 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  mpbid  233  sylibd  240  sylbid  241  mpbidi  242  imbitrid  245  biimtrdi  254  con4bid  318  mtbird  326  mtbiri  328  imbi1d  342  bitr3  353  pm5.21im  375  biimpa  477  bi23imp13  1121  alexbii  1840  spvv  1995  spfw  2040  cbvalw  2042  sbequi  2095  chvarfv  2252  cbvalv1  2349  spv  2401  chvar  2403  cbval  2406  sb1  2486  nfsb4t  2507  exmoeu  2585  euim  2621  2eu3  2657  ralbida  3250  rgen2a  3335  ralcom2  3341  ceqsalt  3464  ceqsalgALT  3467  spcimgft  3492  spcdv  3532  rspcdv  3552  rspcebdv  3554  rexraleqim  3585  sbcn1  3775  sbcbi1  3780  sbeqalb  3785  sbcel21v  3790  elpwunsn  4616  rabsnifsb  4654  ssunsn2  4758  preqr1g  4783  iuneqconst  4933  axprlem3  5354  axprlem3OLD  5358  sbcop1  5428  propeqop  5448  euotd  5454  rexopabb  5470  sotr2  5560  relop  5792  elinxp  5971  elimasni  6043  sotri2  6079  onmindif  6404  dffv2  6922  mpteqb  6955  elfvmptrab  6965  chfnrn  6990  elpreima  6999  iinpreima  7010  exfo  7046  ffnfv  7060  f1elima  7207  f1ounsn  7216  f1eqcocnv  7245  fliftfun  7256  soisores  7271  isotr  7280  isomin  7281  ovmpodv2  7514  difsnexi  7704  onint  7733  oneqmin  7743  ordunisuc2  7784  tfindsg  7801  findsg  7837  resf1extb  7874  f1oweALT  7914  el2mpocl  8025  poseq  8098  soseq  8099  ressuppss  8123  funsssuppss  8130  suppofssd  8143  smoiso  8292  seqomlem2  8380  oaordi  8471  oawordri  8475  oaordex  8483  oalimcl  8485  omwordi  8496  oewordi  8517  oelim2  8521  nnmwordi  8561  xpider  8725  iiner  8726  undifixp  8872  mptelixpg  8873  dom2lem  8929  findcard2s  9090  pssnn  9093  nneneq  9130  fineqvlem  9166  dif1ennnALT  9177  unfilem2  9206  domunfican  9222  f1dmvrnfibi  9241  fsuppimp  9271  dffi2  9326  infsupprpr  9409  wemaplem2  9452  suc11reg  9531  noinfep  9572  cantnflem1  9601  r1fin  9688  tcrank  9799  cardlim  9887  fseqenlem1  9937  alephnbtwn  9984  alephord2i  9990  alephf1  9998  cardaleph  10002  alephiso  10011  dfac12lem2  10058  ackbij1lem16  10147  cflm  10163  cfcoflem  10185  sornom  10190  fin23lem27  10241  isf32lem7  10272  fin17  10307  fin1a2lem2  10314  fin1a2lem4  10316  fin1a2lem6  10318  fin1a2lem9  10321  axdc3lem2  10364  zorn2lem7  10415  uniimadom  10457  inar1  10689  grothomex  10743  addcanpi  10813  mulcanpi  10814  enqer  10835  genpcd  10920  genpnmax  10921  ltexprlem4  10953  reclem3pr  10963  reclem4pr  10964  suplem2pr  10967  axpre-ltadd  11081  axpre-sup  11083  ltletr  11229  00id  11312  addn0nid  11561  mul0or  11781  prodgt02  11994  lemul1a  12000  mulgt1OLD  12005  divgt0  12015  divge0  12016  ledivp1i  12072  ltdivp1i  12073  cju  12146  nnsub  12212  nominpos  12405  nn0n0n1ge2  12496  btwnnz  12596  suprfinzcl  12634  ublbneg  12874  zmax  12886  cnref1o  12926  ltsubrp  12971  ltaddrp  12972  xrltletr  13099  qbtwnre  13142  xltnegi  13159  xnn0xadd0  13190  iccsupr  13386  icoshft  13417  difreicc  13428  iccshftri  13431  iccshftli  13433  iccdili  13435  icccntri  13437  fzen  13486  elfz1b  13538  fzofzim  13655  eluzgtdifelfzo  13673  elfzo1elm1fzo0  13714  injresinjlem  13736  injresinj  13737  flval2  13764  flval3  13765  modmuladdim  13867  modaddmodup  13887  addmodlteq  13899  fseqsupubi  13931  ssnn0fi  13938  mptnn0fsuppr  13952  sq01  14178  hashf1rn  14305  hashgt12el  14375  hashgt12el2  14376  hashfundm  14395  hash2pr  14422  hash2exprb  14424  hashge2el2difr  14434  hashtpg  14438  hash3tr  14444  lswlgt0cl  14522  ccatalpha  14547  pfxfv  14636  pfxsuff1eqwrdeq  14652  ccatopth2  14670  swrdccat  14688  swrdccat3blem  14692  reuccatpfxs1lem  14699  repsdf2  14731  repswsymball  14732  repswrevw  14740  cshweqrep  14774  cshw1  14775  2cshwcshw  14778  scshwfzeqfzo  14779  cshwcsh2id  14781  swrdco  14790  swrd2lsw  14905  2swrd2eqwrdeq  14906  wwlktovfo  14911  cjre  15092  icodiamlt  15391  reusq0  15418  o1lo1  15490  o1of2  15566  o1rlimmul  15572  zsum  15671  modfsummods  15747  zprod  15893  reeff1  16078  dvdsmod0  16218  dvds2lem  16228  muldvds1  16240  dvdscmulr  16244  dvdsmulcr  16245  dvdsdivcl  16276  mod2eq1n2dvds  16307  oddnn02np1  16308  divalglem8  16360  ndvdsadd  16370  zeqzmulgcd  16470  dfgcd2  16506  absproddvds  16577  lcmftp  16596  coprmdvds  16613  2mulprm  16653  isprm5  16668  divgcdodd  16671  isprm6  16675  prmdvdsexpr  16678  prmdvdsbc  16687  cncongrprm  16690  phiprmpw  16737  modprm0  16767  pythagtriplem4  16781  pcz  16843  difsqpwdvds  16849  1arith  16889  prmgaplem5  17017  prmgaplem6  17018  cshwrepswhash1  17064  sbcie2s  17122  divsfval  17502  catsubcat  17797  fthmon  17887  isinitoi  17957  istermoi  17958  iszeroi  17967  setcmon  18045  setcepi  18046  funcestrcsetclem8  18104  fthestrcsetc  18107  funcsetcestrclem8  18119  fthsetcestrc  18122  odupos  18283  pltnle  18293  pltval3  18294  lublecllem  18315  latasym  18400  mrelatglb  18517  mrelatlub  18519  cnvpsb  18536  chninf  18592  mgmpropd  18610  isgrpid2  18943  ghmghmrn  19201  ghmf1  19212  kerf1ghm  19213  orbsta  19279  resscntz  19299  gsmsymgrfixlem1  19393  gsmsymgreqlem2  19397  mndodcongi  19509  odf1  19528  lsmss1  19631  lsmss2  19633  efgredeu  19718  cntzcmnss  19807  imasabl  19842  lt6abl  19861  ablfaclem3  20055  ogrpaddlt  20104  ringinvnz1ne0  20272  0ringnnzr  20497  subrngringnsg  20525  srhmsubc  20652  domnmuln0  20681  lspsneq  21115  lspsneu  21116  lsmcv  21134  rnglidlmcl  21209  rngqiprngimf1lem  21287  lidldvgen  21327  domnchr  21507  znf1o  21526  zntoslem  21531  znfld  21535  cygznlem2a  21542  cygznlem3  21544  phlssphl  21634  islindf4  21813  uvcendim  21822  psdmul  22154  ply1scln0  22277  gsummoncoe1  22294  matvscl  22414  scmataddcl  22499  scmatsubcl  22500  scmatfo  22513  scmatghm  22516  maducoeval2  22623  slesolinv  22663  cramerimplem2  22667  cpmatelimp  22695  cpmatelimp2  22697  cpmatacl  22699  cpmatinvcl  22700  pm2mpf1  22782  cayhamlem1  22849  cayleyhamilton1  22875  0ntr  23054  islpi  23132  lmss  23281  cmpcld  23385  cmpfi  23391  1stcelcls  23444  comppfsc  23515  ptcnplem  23604  qtophmeo  23800  fbdmn0  23817  fbasrn  23867  elfm3  23933  fmfnfmlem4  23940  fclscf  24008  cnpfcf  24024  alexsubALTlem3  24032  tsmsres  24127  blval2  24545  tnggrpr  24638  nmoleub  24714  nmhmcn  25105  ncvs1  25142  iscau4  25264  caussi  25282  cmssmscld  25335  cmslssbn  25357  cniccbdd  25446  ovoliunnul  25492  mbfinf  25650  itg2splitlem  25733  dvcn  25906  c1lip1  25982  c1lip3  25984  dvcnvrelem1  26002  dvfsumlem2  26012  ply1divex  26120  quotcan  26293  aannenlem1  26312  taylf  26344  taylthlem2  26357  ulmcaulem  26377  ulmcau  26378  reeff1o  26430  logccv  26645  rtprmirr  26742  logreclem  26744  isosctrlem2  26801  xrlimcnp  26950  rlimcxp  26955  ftalem7  27060  vmappw  27097  fsumdvdsmul  27176  fsumvma  27194  dchreq  27239  dchrptlem1  27245  dchrsum  27250  bposlem7  27271  lgsqrlem2  27328  lgsdchr  27336  gausslemma2dlem1a  27346  lgseisenlem2  27357  lgsquad2  27367  2lgslem1b  27373  2sqlem6  27404  2sqnn0  27419  addsq2reu  27421  2sqreulem2  27433  ltsval2  27638  ltsres  27644  nodenselem8  27673  nodense  27674  noresle  27679  cutsun12  27800  madeval2  27843  elmade  27867  negsf1o  28064  muls0ord  28195  recsex  28229  bdayons  28286  addonbday  28289  noseqrdgfn  28316  n0subs  28373  eln0zs  28410  zsoring  28419  bdayfinbndlem1  28477  z12bdaylem1  28480  tgcgrcomimp  28563  isperp2  28801  xmstrkgc  28972  brbtwn  28986  brcgr  28987  axcgrid  29003  axeuclidlem  29049  axeuclid  29050  elntg2  29072  lpvtx  29155  upgrex  29179  upgrpredgv  29226  upgredgpr  29229  uhgr0v0e  29325  subgrprop  29360  fusgrfisbase  29415  edgnbusgreu  29454  nbusgredgeu0  29455  cusgredg  29511  structtocusgr  29533  cusgrsize2inds  29540  cusgrsize  29541  usgredgsscusgredg  29546  fusgrmaxsize  29551  uspgrloopvtxel  29603  umgr2v2e  29612  vtxdginducedm1fi  29631  finsumvtxdg2sstep  29636  rgrprop  29647  rusgrprop  29649  0uhgrrusgr  29665  rusgrpropedg  29671  ewlkprop  29690  upgrewlkle2  29693  wlkprop  29698  upgrwlkcompim  29729  uspgr2wlkeq  29732  wlklenvclwlk  29740  wlkonprop  29743  wlkres  29755  redwlk  29757  wlkdlem2  29768  wksonproplem  29789  usgr2trlspth  29847  usgr2pth  29850  pthdlem1  29852  crctcshwlkn0lem4  29899  wwlksnprcl  29925  wlkiswwlks2  29961  wwlksm1edg  29967  wlknewwlksn  29973  wwlksnred  29978  wwlksnextbi  29980  wwlksnextwrd  29983  wwlksnextinj  29985  wwlksnextsurj  29986  umgr2wlk  30035  usgrwwlks2on  30044  umgrwwlks2on  30045  elwwlks2  30055  clwwlk1loop  30076  umgrclwwlkge2  30079  clwlkclwwlklem2a1  30080  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwlkclwwlkfo  30097  clwwisshclwwslemlem  30101  clwwlknwwlksn  30126  clwwlknlbonbgr1  30127  clwwlkn1loopb  30131  clwwlkf  30135  clwwlknon1  30185  clwwlknonwwlknonb  30194  clwwlknonex2lem2  30196  vdn0conngrumgrv2  30284  frgrnbnb  30381  frgrncvvdeqlem2  30388  frgrncvvdeqlem3  30389  frgrncvvdeqlem6  30392  frgrwopreglem4a  30398  fusgr2wsp2nb  30422  frrusgrord0lem  30427  numclwwlk2lem1lem  30430  2clwwlk2clwwlklem  30434  2clwwlk2clwwlk  30438  numclwwlk1lem2foa  30442  numclwwlk1lem2f1  30445  frgrreg  30482  hlipgt0  31003  ocin  31385  ocnel  31387  shmodsi  31478  pjmf1  31805  unopf1o  32005  staddi  32335  stadd3i  32337  mdi  32384  dmdmd  32389  dmdi  32391  dmdbr2  32392  dmdbr3  32394  dmdbr4  32395  dmdi4  32396  mdsl1i  32410  superpos  32443  cvbr4i  32456  atssma  32467  atcv1  32469  atomli  32471  chirredlem1  32479  addltmulALT  32535  bian1dOLD  32544  ifeqeqx  32630  disjxpin  32677  suppss3  32815  fpwrelmap  32825  expgt0b  32909  mndlactfo  33106  mndractfo  33108  qsfld  33581  ply1degltdimlem  33806  ply1degltdim  33807  metider  34078  tpr2rico  34096  xrge0iifiso  34119  qqhcn  34175  qqhucn  34176  esumlub  34244  esumpinfval  34257  esumpinfsum  34261  ballotlemfc0  34677  ballotlemfcc  34678  ftc2re  34782  bnj517  35067  fnrelpredd  35272  rankfilimbi  35282  axsepg2  35321  axsepg3  35322  axsepg3ALT  35323  axsepg4  35324  axsepg5  35325  axnulg  35326  pfxwlk  35352  subgrwlk  35360  loop1cycl  35365  erdsze2lem2  35432  satfv1  35591  satfdmlem  35596  satf0op  35605  fmlasuc  35614  dfrdg4  36179  altopthsn  36189  btwncomim  36241  btwnexch3  36248  btwnexch2  36251  endofsegid  36313  opnrebl2  36549  nn0prpwlem  36550  onsuct0  36669  ordcmp  36675  nndivsub  36685  regsfromunir1  36768  dnibndlem13  36796  bj-cbvexvv  36980  bj-cbval  36986  bj-cbvex  36987  bj-cbvexw  37017  bj-nnf-cbval  37123  bj-cbv3tb  37140  bj-spimtv  37147  bj-equsal  37179  bj-sbsb  37190  bj-vtoclf  37268  bj-zfauscl  37277  bj-gabss  37288  bj-gabeqd  37290  currysetlem2  37301  bj-snsetex  37316  bj-axseprep  37427  bj-ismooredr2  37468  bj-inftyexpiinj  37569  bj-finsumval0  37645  bj-fvimacnv0  37646  bj-bary1lem1  37671  bj-bary1  37672  f1omptsnlem  37698  iooelexlt  37724  relowlpssretop  37726  rdgeqoa  37732  finxpsuclem  37759  fvineqsneq  37774  pibt2  37779  wl-isseteq  37867  wl-dfcleq  37876  wl-equsal1i  37915  ltflcei  37975  sin2h  37977  cos2h  37978  tan2h  37979  lindsenlbs  37982  matunitlindf  37985  poimirlem3  37990  poimirlem4  37991  poimirlem18  38005  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  poimirlem24  38011  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem28  38015  poimirlem31  38018  poimir  38020  heicant  38022  mblfinlem1  38024  mblfinlem2  38025  mblfinlem3  38026  mblfinlem4  38027  mbfresfi  38033  cnambfre  38035  ftc1anc  38068  dvasin  38071  areacirclem1  38075  areacirclem4  38078  areacirc  38080  brabg2  38084  fzmul  38108  fdc  38112  incsequz2  38116  isbnd2  38150  opidonOLD  38219  opidon2OLD  38221  grpomndo  38242  elghomlem2OLD  38253  rngoueqz  38307  dvrunz  38321  divrngidl  38395  refressn  38900  dral1-o  39396  lsatn0  39491  l1cvpat  39546  leat2  39786  atnle  39809  cvlcvr1  39831  cvrexchlem  39911  cvratlem  39913  cvrat  39914  atcvrj0  39920  atle  39928  snatpsubN  40242  linepsubN  40244  pmapsub  40260  lneq2at  40270  lncvrelatN  40273  2llnma3r  40280  cdlemblem  40285  paddasslem5  40316  poml4N  40445  lhpmcvr4N  40518  trlval2  40655  cdlemd6  40695  cdleme7ga  40740  cdleme25b  40846  cdleme29b  40867  cdleme35fnpq  40941  cdleme50f1  41035  cdlemf1  41053  cdlemg27b  41188  cdlemk28-3  41400  tendospcanN  41515  diaf11N  41541  dia2dimlem1  41556  dibf11N  41653  dihf11  41759  dihmeetlem1N  41782  dochvalr  41849  dochnel2  41884  dvh4dimlem  41935  dochsat0  41949  mapd1o  42140  hdmapf1oN  42357  hgmapval0  42384  hgmapf1oN  42395  hlhilhillem  42452  nnproddivdvdsd  42485  lcmineqlem  42537  aks4d1p1p5  42560  aks4d1p3  42563  aks4d1p8d2  42570  aks4d1p8  42572  aks4d1p9  42573  fldhmf1  42575  isprimroot2  42579  primrootsunit1  42582  primrootscoprmpow  42584  posbezout  42585  primrootscoprbij  42587  primrootlekpowne0  42590  primrootspoweq0  42591  aks6d1c1p1  42592  aks6d1c1p2  42594  aks6d1c1p3  42595  aks6d1c1p4  42596  aks6d1c1p5  42597  aks6d1c1p7  42598  aks6d1c1p6  42599  aks6d1c1p8  42600  aks6d1c2p2  42604  aks6d1c2lem3  42611  aks6d1c2lem4  42612  hashnexinj  42613  aks6d1c2  42615  aks6d1c5lem0  42620  aks6d1c5lem1  42621  aks6d1c5  42624  sticksstones1  42631  sticksstones3  42633  sticksstones8  42638  sticksstones11  42641  sticksstones12  42643  sticksstones20  42651  sticksstones22  42653  aks6d1c6lem3  42657  aks6d1c6lem4  42658  aks6d1c6isolem1  42659  aks6d1c6isolem2  42660  aks6d1c6lem5  42662  aks6d1c7  42669  rhmqusspan  42670  unitscyglem2  42681  unitscyglem3  42682  aks5lem8  42686  sn-axprlem3  42705  oexpreposd  42799  sn-remul0ord  42885  frlmsnic  43026  fsuppind  43040  prjspval  43053  rexrabdioph  43239  fphpdo  43262  irrapxlem3  43269  rmxypairf1o  43356  rmxycomplete  43362  zindbi  43391  lermxnn0  43395  ltrmy  43397  rmyeq0  43398  rmyeq  43399  lermy  43400  acongsym  43421  acongneg2  43422  wepwsolem  43487  onsupuni  43674  onsupmaxb  43684  onsucf1o  43717  onov0suclim  43719  oe0suclim  43722  onsucwordi  43733  cantnfresb  43769  omabs2  43777  tfsconcat0b  43791  tfsconcatrev  43793  naddcnffo  43809  oaun3lem1  43819  oaltom  43849  omltoe  43851  sdomne0  43857  sdomne0d  43858  safesnsupfidom1o  43861  intabssd  43963  iscard4  43977  ss2iundf  44103  frege129d  44207  frege133d  44209  axfrege52a  44300  axfrege52c  44331  ntrk0kbimka  44483  gneispace  44578  suprleubrd  44610  suprlubrd  44612  radcnvrat  44758  nzss  44761  expgrowthi  44777  ordpss  44894  bi23impib  44930  rspsbc2  44978  tratrb  44980  sbcim2g  44982  truniALT  44985  3impcombi  45260  tpid3gVD  45285  orbi1rVD  45291  sbc3orgVD  45294  rspsbc2VD  45298  tratrbVD  45304  sbcim2gVD  45318  sbcbiVD  45319  truniALTVD  45321  trintALTVD  45323  trintALT  45324  csbingVD  45327  csbsngVD  45336  csbxpgVD  45337  csbresgVD  45338  csbrngVD  45339  csbima12gALTVD  45340  csbunigVD  45341  csbfv12gALTVD  45342  relopabVD  45344  isosctrlem1ALT  45377  relpfrlem  45397  trfr  45406  fzisoeu  45748  xrralrecnnge  45834  allbutfi  45837  climinf  46051  liminfreuzlem  46245  climliminf  46249  climliminflimsup  46251  xlimpnfxnegmnf  46257  xlimbr  46270  stoweidlem7  46450  stoweidlem62  46505  sge0gerpmpt  46845  meaiuninclem  46923  carageniuncllem2  46965  issmflem  47170  et-sqrtnegnre  47316  ormkglobd  47320  natlocalincr  47321  funressnfv  47506  funressnvmo  47508  f1cof1b  47540  2reu3  47573  ralbinrald  47585  afv0fv0  47612  afv0nbfvbi  47614  afvfv0bi  47615  fnbrafvb  47617  afvres  47635  tz6.12-afv  47636  afvco2  47639  ndmaovcl  47666  afv2res  47702  tz6.12-afv2  47703  nelbrim  47738  f1oresf1o2  47754  zm1nn  47765  nltle2tri  47776  subsubelfzo0  47790  2tceilhalfelfzo1  47799  iccpartres  47893  iccpartiltu  47897  fargshiftfv  47914  ichnreuop  47947  ichreuopeq  47948  prsprel  47962  sprsymrelf1lem  47966  sprsymrelfolem2  47968  sprsymrelfo  47972  prpair  47976  paireqne  47986  sbcpr  47996  nprmmul2  48003  nprmmul3  48004  fmtnof1  48013  goldbachthlem2  48024  fmtnoprmfac1  48043  fmtnoprmfac2  48045  lighneallem2  48084  lighneallem4b  48087  lighneallem4  48088  evennodd  48134  oddneven  48135  oexpnegnz  48169  evenltle  48208  fpprwppr  48230  fpprwpprb  48231  gbowge7  48254  gbege6  48256  sbgoldbwt  48268  sbgoldbst  48269  nnsum3primesle9  48285  bgoldbtbndlem2  48297  grimprop  48374  isuspgrimlem  48386  uhgrimisgrgriclem  48421  clnbgrgrimlem  48424  grtriproplem  48430  isgrtri  48434  grimgrtri  48440  stgr1  48452  isubgr3stgr  48466  grlimprop  48475  uspgrlimlem2  48480  uspgrlimlem3  48481  grlimprclnbgr  48487  gpg5nbgrvtx13starlem1  48562  clintop  48699  isassintop  48701  lidldomn1  48722  uzlidlring  48726  2zrngnmlid2  48748  rngccatidALTV  48763  ringccatidALTV  48797  srhmsubcALTV  48816  ztprmneprm  48838  pgrpgt2nabl  48857  lindslinindimp2lem4  48952  lincresunit3  48972  fldivexpfllog2  49056  digexp  49098  naryfvalelfv  49123  affinecomb1  49193  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  eenglngeehlnm  49230  itscnhlc0yqe  49250  itsclc0yqsol  49255  itscnhlc0xyqsol  49256  itschlc0xyqsol1  49257  itschlc0xyqsol  49258  itsclquadeu  49268  inlinecirc02plem  49277  inlinecirc02p  49278  pm4.71da  49280  mofsn  49334  seposep  49416  resipos  49465  idmon  49510  idepi  49511  prsthinc  49954  grptcmon  50083  grptcepi  50084  spd  50168  spcdvw  50169  setrec2fun  50182