Theorem mpbir2and 713

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypotheses

Ref	Expression
mpbir2and.1	⊢ (𝜑 → 𝜒)
mpbir2and.2	⊢ (𝜑 → 𝜃)
mpbir2and.3	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
mpbir2and	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbir2and

Step	Hyp	Ref	Expression
1		mpbir2and.1	. . 3 ⊢ (𝜑 → 𝜒)
2		mpbir2and.2	. . 3 ⊢ (𝜑 → 𝜃)
3	1, 2	jca 511	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 257	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  elpreimad  6987  fveqressseq  7007  fmptsng  7097  fmptsnd  7098  fnprb  7137  fntpb  7138  fpr3g  8210  frrlem4  8214  1ellim  8408  isfsuppd  9245  fdmfifsupp  9254  fczfsuppd  9265  fsuppmptif  9278  fsuppco2  9282  fsuppcor  9283  dffi3  9310  suppr  9351  infpr  9384  ordtypelem7  9405  cantnf0  9560  cantnfp1lem1  9563  cantnfp1lem2  9564  cantnfp1lem3  9565  cantnflem1a  9570  cantnflem1d  9573  cantnflem1  9574  cantnf  9578  rankpwi  9708  carduni  9866  fin23lem32  10227  fpwwe2lem5  10518  fpwwe2lem11  10524  fpwwe2lem12  10525  fpwwe2  10526  inttsk  10657  grutsk1  10704  add20  11621  supaddc  12081  supadd  12082  supmul  12086  suprzcl  12545  uzid  12739  uzwo3  12833  rpnnen1lem5  12871  xrletrid  13046  xrre  13060  xrre3  13062  xleadd1a  13144  xlemul1a  13179  elioc2  13301  elico2  13302  elicc2  13303  elfz1eq  13427  fzadd2  13451  fznatpl1  13470  elfz1uz  13486  nn0fz0  13517  fzctr  13532  fzo1fzo0n0  13607  fzoaddel  13609  elincfzoext  13615  flid  13704  flval3  13711  fladdz  13721  fldiv  13756  modid  13792  hashf1lem1  14354  pfxccatin12d  14644  repswpfx  14684  2cshw  14712  pfx2  14846  wwlktovf1  14856  sqeqd  15065  01sqrexlem7  15147  max0add  15209  abs2difabs  15234  rddif  15240  fzomaxdiflem  15242  rexico  15253  icodiamlt  15337  limsupgre  15380  rlim3  15397  icco1  15439  rlimclim  15445  rlimuni  15449  rlimresb  15464  isercolllem2  15565  isercolllem3  15566  isercoll  15567  caucvgrlem  15572  caurcvgr  15573  iseraltlem3  15583  fsum00  15697  o1fsum  15712  bitsfzolem  16337  bitsfzo  16338  bitsmod  16339  bitscmp  16341  gcd0id  16422  gcdneg  16425  bezoutlem4  16445  nn0seqcvgd  16473  lcmneg  16506  lcmfunsnlem2lem2  16542  qredeq  16560  prmind2  16588  eulerthlem2  16685  pcpremul  16747  pcidlem  16776  pcgcd1  16781  fldivp1  16801  pcfaclem  16802  4sqlem17  16865  vdwlem1  16885  vdwlem6  16890  vdwlem12  16896  vdwlem13  16897  0ram  16924  ram0  16926  ramub1lem1  16930  invco  17670  sectmon  17681  monsect  17682  invid  17686  ssctr  17724  ssceq  17725  0ssc  17736  0subcat  17737  catsubcat  17738  issubc3  17748  fullsubc  17749  funcinv  17772  fthmon  17828  fuccocl  17866  fucidcl  17867  invfuc  17876  2initoinv  17909  2termoinv  17916  elhomai  17932  setcmon  17986  setcepi  17987  catcisolem  18009  curf2cl  18129  yonedalem4c  18175  yonedalem3  18178  yoniso  18183  lublecl  18257  isacs3lem  18440  tsrdir  18502  chnccat  18524  rabsubmgmd  18604  submgmid  18606  subsubmgm  18610  mgmhmima  18615  mgmhmeql  18616  mndpfsupp  18667  mnd1  18679  sgrp2nmndlem4  18828  sgrp2nmndlem5  18829  0subg  19056  nmznsg  19073  ghmpreima  19143  ghmeql  19144  ghmnsgpreima  19146  kerf1ghm  19152  cntzsgrpcl  19239  cntzsubm  19243  cntzsubg  19244  cntzmhm  19246  symgextfo  19327  symgfixf1  19342  symgfixfolem1  19343  odlem2  19444  finodsubmsubg  19472  gexlem2  19487  gexcl2  19494  sylow1lem5  19507  subgslw  19521  slwhash  19529  fislw  19530  sylow3lem1  19532  lsmsubg  19559  efgredlemd  19649  efgredlem  19652  efgcpbllemb  19660  frgpuplem  19677  cyggeninv  19788  iscygd  19792  iscygodd  19793  gsumzadd  19827  gsumconst  19839  gsumpt  19867  gsum2dlem2  19876  gsum2d  19877  gsum2d2lem  19878  dprdfcntz  19922  eldprdi  19925  subgdmdprd  19941  subgdprd  19942  dprdpr  19957  ablfac1c  19978  ablfac1eu  19980  ablfaclem3  19994  ogrpaddlt  20043  ogrpsublt  20047  ring1  20221  subrngint  20468  rhmimasubrng  20474  cntzsubrng  20475  rhmeql  20511  rhmima  20512  cntzsubr  20514  rnghmsscmap2  20537  rnghmsscmap  20538  rnghmsubcsetc  20541  zrzeroorngc  20552  rhmsscmap2  20566  rhmsscmap  20567  rhmsubcsetc  20570  rhmsscrnghm  20573  rhmsubcrngc  20576  srhmsubc  20588  rhmsubc  20597  issubdrg  20688  fldhmsubc  20693  imadrhmcl  20705  isabvd  20720  abvdiv  20737  ornglmullt  20777  orngrmullt  20778  orngmullt  20779  ofldlt1  20783  lsslsp  20941  lsslspOLD  20942  lmhmima  20974  lmhmpreima  20975  lmhmeql  20982  lsmcl  21010  lspfixed  21058  rnglidlrng  21177  rngqiprngim  21234  rng2idl1cntr  21235  qsssubdrg  21356  gzrngunit  21363  pzriprnglem8  21418  evpmodpmf1o  21526  ocvpj  21647  dsmm0cl  21670  dsmmacl  21671  dsmmsubg  21673  dsmmlss  21674  frlmsplit2  21703  uvcff  21721  lindfrn  21751  f1lindf  21752  lindsss  21754  issubassa  21797  issubassa2  21822  snifpsrbag  21850  psrbaglesupp  21852  psrbaglecl  21853  psrbagaddcl  21854  psrbagcon  21855  mplsubglem  21929  mpllsslem  21930  mplassa  21952  subrgmpl  21960  mplcoe5  21968  mplbas2  21970  mplind  21998  mpfind  22035  ismhp2  22049  mhpmulcl  22057  mhplss  22063  ply1assa  22105  coe1tmmul2  22183  coe1tmmul  22184  cply1coe0bi  22210  dmatid  22403  dmatsubcl  22406  dmatscmcl  22411  scmatid  22422  scmataddcl  22424  scmatsubcl  22425  scmatmulcl  22426  smatvscl  22432  scmatrhmcl  22436  mat0scmat  22446  mat1scmat  22447  mdet0pr  22500  chmaidscmat  22756  distop  22903  indistopon  22909  ppttop  22915  epttop  22917  mretopd  23000  toponmre  23001  neiss  23017  opnneissb  23022  ssnei2  23024  innei  23033  neiptoptop  23039  ordtcld1  23105  ordtcld2  23106  lmconst  23169  cnpnei  23172  iscncl  23177  cnss1  23184  cnss2  23185  cncnpi  23186  cncnp  23188  cnconst2  23191  cnrest  23193  cnpresti  23196  cnpdis  23201  paste  23202  lmcnp  23212  cnhaus  23262  hauscmp  23315  2ndcomap  23366  1stcelcls  23369  1stccnp  23370  llyrest  23393  nllyrest  23394  llyidm  23396  nllyidm  23397  ssref  23420  reftr  23422  refun0  23423  dissnref  23436  kgentopon  23446  kgenidm  23455  kgencn3  23466  txcld  23511  neitx  23515  tx1cn  23517  tx2cn  23518  ptcld  23521  xkoccn  23527  txcnp  23528  ptcnp  23530  txcnmpt  23532  ptcn  23535  txdis1cn  23543  ptrescn  23547  txkgen  23560  xkoco1cn  23565  xkoco2cn  23566  xkococn  23568  xkoinjcn  23595  qtoptop2  23607  qtopuni  23610  qtopid  23613  qtopkgen  23618  basqtop  23619  tgqtop  23620  qtopss  23623  qtopeu  23624  qtoprest  23625  kqopn  23642  kqcld  23643  kqreglem2  23650  reghmph  23701  ordthmeolem  23709  qtopf1  23724  opnfbas  23750  isfil2  23764  fbasweak  23773  fsubbas  23775  filconn  23791  fbasrn  23792  rnelfmlem  23860  flimss2  23880  flimss1  23881  hausflim  23889  flimclslem  23892  flimsncls  23894  cnpflfi  23907  flfcnp2  23915  fclsfnflim  23935  cnextfvval  23973  cnextfres1  23976  symgtgp  24014  opnsubg  24016  ghmcnp  24023  qustgpopn  24028  qustgplem  24029  qustgphaus  24031  tsmsfbas  24036  ustfilxp  24121  utoptop  24142  utopbas  24143  restutopopn  24146  iducn  24190  cstucnd  24191  ucncn  24192  fmucnd  24199  cfilufg  24200  trcfilu  24201  cfiluweak  24202  neipcfilu  24203  psmetres2  24222  isxmetd  24234  xmetpsmet  24256  imasf1oxmet  24283  xblss2ps  24309  xblss2  24310  xblcntrps  24318  xblcntr  24319  blcld  24413  metustfbas  24465  cfilucfil  24467  restmetu  24478  ngptgp  24544  tngngpd  24561  nrmtngnrm  24566  tngnrg  24582  nlmvscn  24595  nrginvrcn  24600  nmo0  24643  nmoeq0  24644  nmoid  24650  nghmcn  24653  0nmhm  24663  blcvx  24706  iccntr  24730  xrge0tsms  24743  xmetdcn2  24746  metdstri  24760  metdscn  24765  rescncf  24810  cncfco  24820  oprpiece1res2  24870  cnheibor  24874  cnllycmp  24875  bndth  24877  ishtpyd  24894  isphtpyd  24905  pcoval2  24936  nmhmcn  25040  ipcn  25166  lmnn  25183  cfilss  25190  iscfil3  25193  cfilfcls  25194  cmetcaulem  25208  iscmet3lem2  25212  cfilres  25216  lmcau  25233  flimcfil  25234  cncmet  25242  rlmbn  25281  minveclem3b  25348  pjthlem1  25357  pjth2  25360  ivthlem3  25374  ovolssnul  25408  ovolctb  25411  ovoliunnul  25428  ovolsca  25436  ovolicopnf  25445  voliunlem2  25472  volsup  25477  dyadmaxlem  25518  vitalilem5  25533  mbfres  25565  mbfss  25567  mbfmulc2re  25569  mbfadd  25582  mbfmulc2  25584  mbflim  25589  i1faddlem  25614  i1fmullem  25615  mbfmul  25647  itg2mulc  25668  itg2cnlem1  25682  ibl0  25708  iblposlem  25713  itgreval  25718  iblneg  25724  iblss  25726  iblss2  25727  itgle  25731  iblconst  25739  iblabs  25750  iblabsr  25751  iblmulc2  25752  bddmulibl  25760  limciun  25815  limcun  25816  dvres2lem  25831  dvidlem  25836  dvcnp2  25841  dvcnp2OLD  25842  dvcn  25843  cpnres  25859  dvaddbr  25860  dvmulbr  25861  dvmulbrOLD  25862  dvcobr  25869  dvcobrOLD  25870  dvcjbr  25873  dvrec  25879  dvcnvlem  25900  dvferm  25912  dvlip2  25920  dveq0  25925  dv11cn  25926  dvivthlem1  25933  lhop1  25939  lhop2  25940  lhop  25941  dvcnvre  25944  dvfsumlem3  25955  dvfsumlem4  25956  dvfsumrlim  25958  dvfsum2  25961  ftc1a  25964  ftc1lem4  25966  ftc1lem6  25968  ftc1  25969  coe1mul3  26024  deg1addle2  26027  deg1sublt  26035  fta1blem  26096  drnguc1p  26099  ig1prsp  26106  plyco0  26117  plyeq0lem  26135  dgrub  26159  dgreq  26169  dgradd2  26194  dgrmul  26196  dgrcolem2  26200  dgrco  26201  plycpn  26217  plydivlem4  26224  plydiveu  26226  vieta1lem2  26239  vieta1  26240  aalioulem2  26261  aalioulem3  26262  aaliou3lem7  26277  tayl0  26289  ulmcn  26328  ulmdvlem3  26331  psercn  26356  abelth  26371  pilem3  26383  efif1olem1  26471  abslogimle  26502  argregt0  26539  argrege0  26540  logf1o2  26579  cxpsqrtlem  26631  cxpcn3  26678  abscxpbnd  26683  logreclem  26692  ang180lem2  26740  ang180lem3  26741  xrlimcnp  26898  harmonicbnd4  26941  fsumharmonic  26942  lgamgulmlem5  26963  lgambdd  26967  basellem4  27014  dvdsppwf1o  27116  dvdsflf1o  27117  fsumfldivdiaglem  27119  chpeq0  27139  chteq0  27140  chtub  27143  chpub  27151  dchrelbasd  27170  dchrmulcl  27180  dchrinv  27192  bposlem1  27215  bposlem2  27216  lgsdirprm  27262  lgsqrlem2  27278  lgsqrlem3  27279  lgsdchr  27286  lgseisenlem1  27306  lgseisenlem2  27307  lgseisenlem3  27308  lgsquadlem1  27311  2sqlem8  27357  2sqblem  27362  2sqmod  27367  chebbnd1lem1  27400  dchrisumlem1  27420  dchrisumlem2  27421  dchrisumlem3  27422  dchrisum0fno1  27442  pntrmax  27495  pntpbnd1a  27516  pntibndlem3  27523  pntlemn  27531  pntlemi  27535  pntlem3  27540  pntleml  27542  ostth1  27564  ostth2  27568  ostth3  27569  nosepon  27597  nolesgn2ores  27604  nogesgn1ores  27606  nosupres  27639  nosupbnd1lem2  27641  nosupbnd2lem1  27647  noinfres  27654  noinfbnd1lem2  27656  noinfbnd2lem1  27662  eqscut3  27758  cofcutrtime  27864  divmuldivsd  28163  divdivs1d  28164  nnsgt0  28260  ercgrg  28488  motco  28511  cnvmot  28512  legso  28570  mirmot  28646  colopp  28740  hphl  28742  lmicom  28759  lmimid  28765  lmimot  28769  hypcgrlem1  28770  hypcgrlem2  28771  trgcopyeulem  28776  inagswap  28812  inaghl  28816  cgrg3col4  28824  brbtwn2  28876  axlowdimlem3  28915  axlowdimlem16  28928  axcontlem8  28942  fusgrfis  29301  nbgr2vtx1edg  29321  0vtxrgr  29548  0vtxrusgr  29549  ewlkle  29577  wlk1ewlk  29611  uspgr2wlkeq2  29618  wlkp1lem8  29650  trlontrl  29680  pthonpth  29719  pthdlem2  29739  wlklnwwlkln1  29839  wlknewwlksn  29858  wwlksnred  29863  wwlksnredwwlkn0  29867  2trlond  29910  2pthond  29913  elwwlks2ons3im  29925  clwlkclwwlklem2a1  29962  clwlkclwwlkf1  29980  clwwlkel  30016  clwwlkwwlksb  30024  wwlksext2clwwlk  30027  1ewlk  30085  0trlon  30094  0pthon  30097  1pthond  30114  3trlond  30143  3pthond  30145  3spthond  30147  eupthres  30185  2clwwlk2clwwlk  30320  numclwwlk1lem2foa  30324  numclwwlk1lem2f1  30327  nvabs  30642  vacn  30664  nmcvcn  30665  nmblore  30756  0lno  30760  0blo  30762  nmlno0lem  30763  occl  31274  pjhthlem1  31361  pjpjpre  31389  nmopre  31840  nmlnop0iALT  31965  nmophmi  32001  leoprf2  32097  stlesi  32211  disjdifprg  32545  disjun0  32565  fsuppcurry1  32697  fsuppcurry2  32698  fpwrelmap  32706  fzspl  32762  dfmgc2lem  32966  pwrssmgc  32971  xrge0tsmsd  33032  psgnfzto1stlem  33059  fzto1st1  33061  evpmid  33107  pnfinf  33142  isarchiofld  33158  rmfsupp2  33195  fracfld  33264  dvdsruassoi  33339  nsgmgc  33367  drngidl  33388  qsdrngi  33450  deg1addlt  33550  ply1degltdimlem  33625  lbsdiflsp0  33629  fedgmul  33634  fldexttr  33661  fldextid  33662  irngnzply1lem  33693  finextalg  33701  minplyelirng  33718  irredminply  33719  algextdeglem8  33727  rtelextdg2lem  33729  constrsslem  33744  constrllcllem  33755  constrlccllem  33756  constrcccllem  33757  qtopt1  33838  reff  33842  locfinreflem  33843  metideq  33896  metider  33897  pstmxmet  33900  qqhval2lem  33984  qqhcn  33994  qqhucn  33995  pwsiga  34133  prsiga  34134  measle0  34211  mbfmcst  34262  1stmbfm  34263  2ndmbfm  34264  imambfm  34265  cnmbfm  34266  mbfmco  34267  mbfmco2  34268  0elcarsg  34310  carsgclctun  34324  sibfof  34343  oddpwdc  34357  eulerpartlemmf  34378  eulerpartlemgs2  34383  0rrv  34454  ballotlemfc0  34496  ballotlemfcc  34497  signstfveq0  34580  breprexplemc  34635  bnj1452  35054  usgrgt2cycl  35142  acycgr1v  35161  derangen  35184  subfacval3  35201  cvmseu  35288  cvmliftmolem2  35294  cvmliftlem7  35303  cvmliftlem15  35310  cvmlift2lem9a  35315  cvmlift2lem9  35323  cvmlift2lem10  35324  cvmlift2lem11  35325  cvmlift2lem12  35326  cvmlift3lem6  35336  cvmlift3lem8  35338  ex-sategoelel  35433  ex-sategoelelomsuc  35438  mclsppslem  35595  mclspps  35596  wsuclem  35838  fness  36362  fnetr  36364  fnessref  36370  refssfne  36371  neibastop1  36372  neibastop2  36374  tailfb  36390  filnetlem3  36393  weiunfrlem  36477  bj-finsumval0  37298  bj-rvecvec  37312  dfgcd3  37337  lindsadd  37632  poimirlem13  37652  poimirlem15  37654  poimirlem24  37663  poimirlem28  37667  mblfinlem2  37677  ovoliunnfl  37681  volsupnfl  37684  mbfresfi  37685  iblabsnc  37703  iblmulc2nc  37704  ftc1cnnclem  37710  ftc1cnnc  37711  ftc1anc  37720  sdclem2  37761  metf1o  37774  ismtyhmeolem  37823  ismtyres  37827  heibor1lem  37828  bfplem2  37842  bfp  37843  rrncmslem  37851  iccbnd  37859  icccmpALT  37860  rngogrphom  37990  rngoisoco  38001  keridl  38051  lsmcv2  39047  lsatcv0  39049  lcvexchlem4  39055  lcvexchlem5  39056  l1cvpat  39072  lfl0f  39087  lfladdcl  39089  lflnegcl  39093  lkrlss  39113  eqlkr  39117  lkrlsp  39120  lkrlsp2  39121  lshpkrcl  39134  lkrin  39182  1cvrjat  39493  llni  39526  llnle  39536  lplni  39550  lplnle  39558  llncvrlpln2  39575  2atmat  39579  lvoli  39593  lplncvrlvol2  39633  elpaddri  39820  paddclN  39860  pclclN  39909  pclfinN  39918  0psubclN  39961  1psubclN  39962  atpsubclN  39963  pmapsubclN  39964  osumclN  39985  pexmidN  39987  pexmidlem6N  39993  lhp2lt  40019  lautcnv  40108  idlaut  40114  lautco  40115  idldil  40132  ldilcnv  40133  ldilco  40134  ltrncnv  40164  idltrn  40168  cdleme16d  40299  cdleme50laut  40565  cdleme50ldil  40566  cdleme50ltrn  40575  ltrnco  40737  dian0  41057  dia0eldmN  41058  dia1eldmN  41059  dialss  41064  diaintclN  41076  docaclN  41142  doca2N  41144  djajN  41155  dibintclN  41185  diblss  41188  dicvaddcl  41208  dicvscacl  41209  dicn0  41210  cdlemn11a  41225  dihord2cN  41239  dihord11b  41240  dihord6apre  41274  dihmeetlem1N  41308  dihglblem5apreN  41309  dihpN  41354  dihjatcclem4  41439  dochkr1  41496  islpoldN  41502  lcfrlem31  41591  mapdpglem18  41707  mapdheq2  41747  mapdheq4  41750  mapdh6aN  41753  hdmap1l6a  41827  hdmap14lem4a  41889  lcmineqlem4  42044  frlmfzoccat  42517  drnginvmuld  42539  psrbagres  42558  evlselvlem  42598  evlselv  42599  fsuppind  42602  fsuppssind  42605  prjspvs  42622  irrapxlem4  42837  pell1234qrdich  42873  pell1qr1  42883  pell14qrgap  42887  pellqrexplicit  42889  rmspecfund  42921  fzmaxdif  42993  acongeq  42995  jm2.23  43008  jm3.1  43032  lmhmlnmsplit  43099  hbt  43142  dgrsub2  43147  proot1ex  43208  cantnfub  43333  cantnfresb  43336  cantnf2  43337  tfsconcatfv2  43352  tfsconcatrn  43354  tfsconcatb0  43356  naddcnff  43374  naddcnffo  43376  naddcnfid1  43379  naddcnfid2  43380  clublem  43622  dftrcl3  43732  mnugrud  44296  hashnzfz2  44333  dvconstbi  44346  ubelsupr  45036  restopn3  45167  wessf1ornlem  45201  lefldiveq  45312  iccintsng  45542  climsuse  45627  mullimc  45635  limcdm0  45637  limccog  45639  mullimcf  45642  constlimc  45643  idlimc  45645  limcperiod  45647  limsupre  45658  limcleqr  45661  neglimc  45664  addlimc  45665  0ellimcdiv  45666  xlimliminflimsup  45879  cncfshift  45891  cncfperiod  45896  cncfuni  45903  icccncfext  45904  cncfiooicclem1  45910  fperdvper  45936  ioodvbdlimc1lem2  45949  ioodvbdlimc2lem  45951  mbfres2cn  45975  iblsplit  45983  stoweidlem7  46024  stoweidlem13  46030  stoweidlem26  46043  wallispilem3  46084  stirlinglem6  46096  stirlinglem10  46100  dirkercncf  46124  fourierdlem6  46130  fourierdlem11  46135  fourierdlem12  46136  fourierdlem15  46139  fourierdlem26  46150  fourierdlem42  46166  fourierdlem50  46173  fourierdlem51  46174  fourierdlem52  46175  fourierdlem54  46177  fourierdlem62  46185  fourierdlem79  46202  fourierdlem102  46225  fourierdlem114  46237  etransclem23  46274  3f1oss1  47085  zgeltp1eq  47319  setsnidel  47387  preimafvsnel  47389  iccpartres  47428  prpair  47511  fpprel2  47751  isubgrsubgr  47879  grimidvtxedg  47895  grimcnv  47898  isuspgrim  47906  upgrimpthslem2  47918  stgrnbgr0  47974  uhgrimgrlim  47997  clnbgr3stgrgrlim  48029  gpg5nbgrvtx03starlem2  48079  gpg5nbgrvtx13starlem2  48082  gpg5edgnedg  48140  isassintop  48220  rhmsubcALTV  48295  srhmsubcALTV  48335  fldhmsubcALTV  48343  rmfsupp  48383  scmfsupp  48385  mptcfsupp  48387  lcoel0  48439  lincsumcl  48442  lincscmcl  48443  lcoss  48447  lindsrng01  48479  lincreslvec3  48493  lindssnlvec  48497  zgtp1leeq  48532  lubsscl  48970  glbsscl  48971  idmon  49031  idepi  49032  iinfssc  49068  iinfsubc  49069  discsubc  49075  nelsubclem  49078  imassc  49164  imasubc3  49167  isnatd  49234  swapfiso  49296  fucoppc  49421  thinciso  49481  diagciso  49550  termolmd  49681