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  6997  fveqressseq  7017  fmptsng  7108  fmptsnd  7109  fnprb  7148  fntpb  7149  fpr3g  8225  frrlem4  8229  1ellim  8423  isfsuppd  9275  fdmfifsupp  9284  fczfsuppd  9295  fsuppmptif  9308  fsuppco2  9312  fsuppcor  9313  dffi3  9340  suppr  9381  infpr  9414  ordtypelem7  9435  cantnf0  9590  cantnfp1lem1  9593  cantnfp1lem2  9594  cantnfp1lem3  9595  cantnflem1a  9600  cantnflem1d  9603  cantnflem1  9604  cantnf  9608  rankpwi  9738  carduni  9896  fin23lem32  10257  fpwwe2lem5  10548  fpwwe2lem11  10554  fpwwe2lem12  10555  fpwwe2  10556  inttsk  10687  grutsk1  10734  add20  11650  supaddc  12110  supadd  12111  supmul  12115  suprzcl  12574  uzid  12768  uzwo3  12862  rpnnen1lem5  12900  xrletrid  13075  xrre  13089  xrre3  13091  xleadd1a  13173  xlemul1a  13208  elioc2  13330  elico2  13331  elicc2  13332  elfz1eq  13456  fzadd2  13480  fznatpl1  13499  elfz1uz  13515  nn0fz0  13546  fzctr  13561  fzo1fzo0n0  13636  fzoaddel  13638  elincfzoext  13644  flid  13730  flval3  13737  fladdz  13747  fldiv  13782  modid  13818  hashf1lem1  14380  pfxccatin12d  14669  repswpfx  14709  2cshw  14737  pfx2  14872  wwlktovf1  14882  sqeqd  15091  01sqrexlem7  15173  max0add  15235  abs2difabs  15260  rddif  15266  fzomaxdiflem  15268  rexico  15279  icodiamlt  15363  limsupgre  15406  rlim3  15423  icco1  15465  rlimclim  15471  rlimuni  15475  rlimresb  15490  isercolllem2  15591  isercolllem3  15592  isercoll  15593  caucvgrlem  15598  caurcvgr  15599  iseraltlem3  15609  fsum00  15723  o1fsum  15738  bitsfzolem  16363  bitsfzo  16364  bitsmod  16365  bitscmp  16367  gcd0id  16448  gcdneg  16451  bezoutlem4  16471  nn0seqcvgd  16499  lcmneg  16532  lcmfunsnlem2lem2  16568  qredeq  16586  prmind2  16614  eulerthlem2  16711  pcpremul  16773  pcidlem  16802  pcgcd1  16807  fldivp1  16827  pcfaclem  16828  4sqlem17  16891  vdwlem1  16911  vdwlem6  16916  vdwlem12  16922  vdwlem13  16923  0ram  16950  ram0  16952  ramub1lem1  16956  invco  17696  sectmon  17707  monsect  17708  invid  17712  ssctr  17750  ssceq  17751  0ssc  17762  0subcat  17763  catsubcat  17764  issubc3  17774  fullsubc  17775  funcinv  17798  fthmon  17854  fuccocl  17892  fucidcl  17893  invfuc  17902  2initoinv  17935  2termoinv  17942  elhomai  17958  setcmon  18012  setcepi  18013  catcisolem  18035  curf2cl  18155  yonedalem4c  18201  yonedalem3  18204  yoniso  18209  lublecl  18283  isacs3lem  18466  tsrdir  18528  rabsubmgmd  18596  submgmid  18598  subsubmgm  18602  mgmhmima  18607  mgmhmeql  18608  mndpfsupp  18659  mnd1  18671  sgrp2nmndlem4  18820  sgrp2nmndlem5  18821  0subg  19048  nmznsg  19065  ghmpreima  19135  ghmeql  19136  ghmnsgpreima  19138  kerf1ghm  19144  cntzsgrpcl  19231  cntzsubm  19235  cntzsubg  19236  cntzmhm  19238  symgextfo  19319  symgfixf1  19334  symgfixfolem1  19335  odlem2  19436  finodsubmsubg  19464  gexlem2  19479  gexcl2  19486  sylow1lem5  19499  subgslw  19513  slwhash  19521  fislw  19522  sylow3lem1  19524  lsmsubg  19551  efgredlemd  19641  efgredlem  19644  efgcpbllemb  19652  frgpuplem  19669  cyggeninv  19780  iscygd  19784  iscygodd  19785  gsumzadd  19819  gsumconst  19831  gsumpt  19859  gsum2dlem2  19868  gsum2d  19869  gsum2d2lem  19870  dprdfcntz  19914  eldprdi  19917  subgdmdprd  19933  subgdprd  19934  dprdpr  19949  ablfac1c  19970  ablfac1eu  19972  ablfaclem3  19986  ogrpaddlt  20035  ogrpsublt  20039  ring1  20213  subrngint  20463  rhmimasubrng  20469  cntzsubrng  20470  rhmeql  20506  rhmima  20507  cntzsubr  20509  rnghmsscmap2  20532  rnghmsscmap  20533  rnghmsubcsetc  20536  zrzeroorngc  20547  rhmsscmap2  20561  rhmsscmap  20562  rhmsubcsetc  20565  rhmsscrnghm  20568  rhmsubcrngc  20571  srhmsubc  20583  rhmsubc  20592  issubdrg  20683  fldhmsubc  20688  imadrhmcl  20700  isabvd  20715  abvdiv  20732  ornglmullt  20772  orngrmullt  20773  orngmullt  20774  ofldlt1  20778  lsslsp  20936  lsslspOLD  20937  lmhmima  20969  lmhmpreima  20970  lmhmeql  20977  lsmcl  21005  lspfixed  21053  rnglidlrng  21172  rngqiprngim  21229  rng2idl1cntr  21230  qsssubdrg  21351  gzrngunit  21358  pzriprnglem8  21413  evpmodpmf1o  21521  ocvpj  21642  dsmm0cl  21665  dsmmacl  21666  dsmmsubg  21668  dsmmlss  21669  frlmsplit2  21698  uvcff  21716  lindfrn  21746  f1lindf  21747  lindsss  21749  issubassa  21792  issubassa2  21817  snifpsrbag  21845  psrbaglesupp  21847  psrbaglecl  21848  psrbagaddcl  21849  psrbagcon  21850  mplsubglem  21924  mpllsslem  21925  mplassa  21947  subrgmpl  21955  mplcoe5  21963  mplbas2  21965  mplind  21993  mpfind  22030  ismhp2  22044  mhpmulcl  22052  mhplss  22058  ply1assa  22100  coe1tmmul2  22178  coe1tmmul  22179  cply1coe0bi  22205  dmatid  22398  dmatsubcl  22401  dmatscmcl  22406  scmatid  22417  scmataddcl  22419  scmatsubcl  22420  scmatmulcl  22421  smatvscl  22427  scmatrhmcl  22431  mat0scmat  22441  mat1scmat  22442  mdet0pr  22495  chmaidscmat  22751  distop  22898  indistopon  22904  ppttop  22910  epttop  22912  mretopd  22995  toponmre  22996  neiss  23012  opnneissb  23017  ssnei2  23019  innei  23028  neiptoptop  23034  ordtcld1  23100  ordtcld2  23101  lmconst  23164  cnpnei  23167  iscncl  23172  cnss1  23179  cnss2  23180  cncnpi  23181  cncnp  23183  cnconst2  23186  cnrest  23188  cnpresti  23191  cnpdis  23196  paste  23197  lmcnp  23207  cnhaus  23257  hauscmp  23310  2ndcomap  23361  1stcelcls  23364  1stccnp  23365  llyrest  23388  nllyrest  23389  llyidm  23391  nllyidm  23392  ssref  23415  reftr  23417  refun0  23418  dissnref  23431  kgentopon  23441  kgenidm  23450  kgencn3  23461  txcld  23506  neitx  23510  tx1cn  23512  tx2cn  23513  ptcld  23516  xkoccn  23522  txcnp  23523  ptcnp  23525  txcnmpt  23527  ptcn  23530  txdis1cn  23538  ptrescn  23542  txkgen  23555  xkoco1cn  23560  xkoco2cn  23561  xkococn  23563  xkoinjcn  23590  qtoptop2  23602  qtopuni  23605  qtopid  23608  qtopkgen  23613  basqtop  23614  tgqtop  23615  qtopss  23618  qtopeu  23619  qtoprest  23620  kqopn  23637  kqcld  23638  kqreglem2  23645  reghmph  23696  ordthmeolem  23704  qtopf1  23719  opnfbas  23745  isfil2  23759  fbasweak  23768  fsubbas  23770  filconn  23786  fbasrn  23787  rnelfmlem  23855  flimss2  23875  flimss1  23876  hausflim  23884  flimclslem  23887  flimsncls  23889  cnpflfi  23902  flfcnp2  23910  fclsfnflim  23930  cnextfvval  23968  cnextfres1  23971  symgtgp  24009  opnsubg  24011  ghmcnp  24018  qustgpopn  24023  qustgplem  24024  qustgphaus  24026  tsmsfbas  24031  ustfilxp  24116  utoptop  24138  utopbas  24139  restutopopn  24142  iducn  24186  cstucnd  24187  ucncn  24188  fmucnd  24195  cfilufg  24196  trcfilu  24197  cfiluweak  24198  neipcfilu  24199  psmetres2  24218  isxmetd  24230  xmetpsmet  24252  imasf1oxmet  24279  xblss2ps  24305  xblss2  24306  xblcntrps  24314  xblcntr  24315  blcld  24409  metustfbas  24461  cfilucfil  24463  restmetu  24474  ngptgp  24540  tngngpd  24557  nrmtngnrm  24562  tngnrg  24578  nlmvscn  24591  nrginvrcn  24596  nmo0  24639  nmoeq0  24640  nmoid  24646  nghmcn  24649  0nmhm  24659  blcvx  24702  iccntr  24726  xrge0tsms  24739  xmetdcn2  24742  metdstri  24756  metdscn  24761  rescncf  24806  cncfco  24816  oprpiece1res2  24866  cnheibor  24870  cnllycmp  24871  bndth  24873  ishtpyd  24890  isphtpyd  24901  pcoval2  24932  nmhmcn  25036  ipcn  25162  lmnn  25179  cfilss  25186  iscfil3  25189  cfilfcls  25190  cmetcaulem  25204  iscmet3lem2  25208  cfilres  25212  lmcau  25229  flimcfil  25230  cncmet  25238  rlmbn  25277  minveclem3b  25344  pjthlem1  25353  pjth2  25356  ivthlem3  25370  ovolssnul  25404  ovolctb  25407  ovoliunnul  25424  ovolsca  25432  ovolicopnf  25441  voliunlem2  25468  volsup  25473  dyadmaxlem  25514  vitalilem5  25529  mbfres  25561  mbfss  25563  mbfmulc2re  25565  mbfadd  25578  mbfmulc2  25580  mbflim  25585  i1faddlem  25610  i1fmullem  25611  mbfmul  25643  itg2mulc  25664  itg2cnlem1  25678  ibl0  25704  iblposlem  25709  itgreval  25714  iblneg  25720  iblss  25722  iblss2  25723  itgle  25727  iblconst  25735  iblabs  25746  iblabsr  25747  iblmulc2  25748  bddmulibl  25756  limciun  25811  limcun  25812  dvres2lem  25827  dvidlem  25832  dvcnp2  25837  dvcnp2OLD  25838  dvcn  25839  cpnres  25855  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvcobr  25865  dvcobrOLD  25866  dvcjbr  25869  dvrec  25875  dvcnvlem  25896  dvferm  25908  dvlip2  25916  dveq0  25921  dv11cn  25922  dvivthlem1  25929  lhop1  25935  lhop2  25936  lhop  25937  dvcnvre  25940  dvfsumlem3  25951  dvfsumlem4  25952  dvfsumrlim  25954  dvfsum2  25957  ftc1a  25960  ftc1lem4  25962  ftc1lem6  25964  ftc1  25965  coe1mul3  26020  deg1addle2  26023  deg1sublt  26031  fta1blem  26092  drnguc1p  26095  ig1prsp  26102  plyco0  26113  plyeq0lem  26131  dgrub  26155  dgreq  26165  dgradd2  26190  dgrmul  26192  dgrcolem2  26196  dgrco  26197  plycpn  26213  plydivlem4  26220  plydiveu  26222  vieta1lem2  26235  vieta1  26236  aalioulem2  26257  aalioulem3  26258  aaliou3lem7  26273  tayl0  26285  ulmcn  26324  ulmdvlem3  26327  psercn  26352  abelth  26367  pilem3  26379  efif1olem1  26467  abslogimle  26498  argregt0  26535  argrege0  26536  logf1o2  26575  cxpsqrtlem  26627  cxpcn3  26674  abscxpbnd  26679  logreclem  26688  ang180lem2  26736  ang180lem3  26737  xrlimcnp  26894  harmonicbnd4  26937  fsumharmonic  26938  lgamgulmlem5  26959  lgambdd  26963  basellem4  27010  dvdsppwf1o  27112  dvdsflf1o  27113  fsumfldivdiaglem  27115  chpeq0  27135  chteq0  27136  chtub  27139  chpub  27147  dchrelbasd  27166  dchrmulcl  27176  dchrinv  27188  bposlem1  27211  bposlem2  27212  lgsdirprm  27258  lgsqrlem2  27274  lgsqrlem3  27275  lgsdchr  27282  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem3  27304  lgsquadlem1  27307  2sqlem8  27353  2sqblem  27358  2sqmod  27363  chebbnd1lem1  27396  dchrisumlem1  27416  dchrisumlem2  27417  dchrisumlem3  27418  dchrisum0fno1  27438  pntrmax  27491  pntpbnd1a  27512  pntibndlem3  27519  pntlemn  27527  pntlemi  27531  pntlem3  27536  pntleml  27538  ostth1  27560  ostth2  27564  ostth3  27565  nosepon  27593  nolesgn2ores  27600  nogesgn1ores  27602  nosupres  27635  nosupbnd1lem2  27637  nosupbnd2lem1  27643  noinfres  27650  noinfbnd1lem2  27652  noinfbnd2lem1  27658  eqscut3  27753  cofcutrtime  27858  divmuldivsd  28157  divdivs1d  28158  nnsgt0  28254  ercgrg  28480  motco  28503  cnvmot  28504  legso  28562  mirmot  28638  colopp  28732  hphl  28734  lmicom  28751  lmimid  28757  lmimot  28761  hypcgrlem1  28762  hypcgrlem2  28763  trgcopyeulem  28768  inagswap  28804  inaghl  28808  cgrg3col4  28816  brbtwn2  28868  axlowdimlem3  28907  axlowdimlem16  28920  axcontlem8  28934  fusgrfis  29293  nbgr2vtx1edg  29313  0vtxrgr  29540  0vtxrusgr  29541  ewlkle  29569  wlk1ewlk  29603  uspgr2wlkeq2  29610  wlkp1lem8  29642  trlontrl  29672  pthonpth  29711  pthdlem2  29731  wlklnwwlkln1  29831  wlknewwlksn  29850  wwlksnred  29855  wwlksnredwwlkn0  29859  2trlond  29902  2pthond  29905  elwwlks2ons3im  29917  clwlkclwwlklem2a1  29954  clwlkclwwlkf1  29972  clwwlkel  30008  clwwlkwwlksb  30016  wwlksext2clwwlk  30019  1ewlk  30077  0trlon  30086  0pthon  30089  1pthond  30106  3trlond  30135  3pthond  30137  3spthond  30139  eupthres  30177  2clwwlk2clwwlk  30312  numclwwlk1lem2foa  30316  numclwwlk1lem2f1  30319  nvabs  30634  vacn  30656  nmcvcn  30657  nmblore  30748  0lno  30752  0blo  30754  nmlno0lem  30755  occl  31266  pjhthlem1  31353  pjpjpre  31381  nmopre  31832  nmlnop0iALT  31957  nmophmi  31993  leoprf2  32089  stlesi  32203  disjdifprg  32537  disjun0  32557  fsuppcurry1  32681  fsuppcurry2  32682  fpwrelmap  32689  fzspl  32745  dfmgc2lem  32950  pwrssmgc  32955  xrge0tsmsd  33028  psgnfzto1stlem  33055  fzto1st1  33057  evpmid  33103  pnfinf  33135  isarchiofld  33151  rmfsupp2  33188  fracfld  33257  dvdsruassoi  33331  nsgmgc  33359  drngidl  33380  qsdrngi  33442  deg1addlt  33541  ply1degltdimlem  33594  lbsdiflsp0  33598  fedgmul  33603  fldexttr  33630  fldextid  33631  irngnzply1lem  33661  minplyelirng  33681  irredminply  33682  algextdeglem8  33690  rtelextdg2lem  33692  constrsslem  33707  constrllcllem  33718  constrlccllem  33719  constrcccllem  33720  qtopt1  33801  reff  33805  locfinreflem  33806  metideq  33859  metider  33860  pstmxmet  33863  qqhval2lem  33947  qqhcn  33957  qqhucn  33958  pwsiga  34096  prsiga  34097  measle0  34174  mbfmcst  34226  1stmbfm  34227  2ndmbfm  34228  imambfm  34229  cnmbfm  34230  mbfmco  34231  mbfmco2  34232  0elcarsg  34274  carsgclctun  34288  sibfof  34307  oddpwdc  34321  eulerpartlemmf  34342  eulerpartlemgs2  34347  0rrv  34418  ballotlemfc0  34460  ballotlemfcc  34461  signstfveq0  34544  breprexplemc  34599  bnj1452  35018  usgrgt2cycl  35102  acycgr1v  35121  derangen  35144  subfacval3  35161  cvmseu  35248  cvmliftmolem2  35254  cvmliftlem7  35263  cvmliftlem15  35270  cvmlift2lem9a  35275  cvmlift2lem9  35283  cvmlift2lem10  35284  cvmlift2lem11  35285  cvmlift2lem12  35286  cvmlift3lem6  35296  cvmlift3lem8  35298  ex-sategoelel  35393  ex-sategoelelomsuc  35398  mclsppslem  35555  mclspps  35556  wsuclem  35798  fness  36322  fnetr  36324  fnessref  36330  refssfne  36331  neibastop1  36332  neibastop2  36334  tailfb  36350  filnetlem3  36353  weiunfrlem  36437  bj-finsumval0  37258  bj-rvecvec  37272  dfgcd3  37297  lindsadd  37592  poimirlem13  37612  poimirlem15  37614  poimirlem24  37623  poimirlem28  37627  mblfinlem2  37637  ovoliunnfl  37641  volsupnfl  37644  mbfresfi  37645  iblabsnc  37663  iblmulc2nc  37664  ftc1cnnclem  37670  ftc1cnnc  37671  ftc1anc  37680  sdclem2  37721  metf1o  37734  ismtyhmeolem  37783  ismtyres  37787  heibor1lem  37788  bfplem2  37802  bfp  37803  rrncmslem  37811  iccbnd  37819  icccmpALT  37820  rngogrphom  37950  rngoisoco  37961  keridl  38011  lsmcv2  39007  lsatcv0  39009  lcvexchlem4  39015  lcvexchlem5  39016  l1cvpat  39032  lfl0f  39047  lfladdcl  39049  lflnegcl  39053  lkrlss  39073  eqlkr  39077  lkrlsp  39080  lkrlsp2  39081  lshpkrcl  39094  lkrin  39142  1cvrjat  39454  llni  39487  llnle  39497  lplni  39511  lplnle  39519  llncvrlpln2  39536  2atmat  39540  lvoli  39554  lplncvrlvol2  39594  elpaddri  39781  paddclN  39821  pclclN  39870  pclfinN  39879  0psubclN  39922  1psubclN  39923  atpsubclN  39924  pmapsubclN  39925  osumclN  39946  pexmidN  39948  pexmidlem6N  39954  lhp2lt  39980  lautcnv  40069  idlaut  40075  lautco  40076  idldil  40093  ldilcnv  40094  ldilco  40095  ltrncnv  40125  idltrn  40129  cdleme16d  40260  cdleme50laut  40526  cdleme50ldil  40527  cdleme50ltrn  40536  ltrnco  40698  dian0  41018  dia0eldmN  41019  dia1eldmN  41020  dialss  41025  diaintclN  41037  docaclN  41103  doca2N  41105  djajN  41116  dibintclN  41146  diblss  41149  dicvaddcl  41169  dicvscacl  41170  dicn0  41171  cdlemn11a  41186  dihord2cN  41200  dihord11b  41201  dihord6apre  41235  dihmeetlem1N  41269  dihglblem5apreN  41270  dihpN  41315  dihjatcclem4  41400  dochkr1  41457  islpoldN  41463  lcfrlem31  41552  mapdpglem18  41668  mapdheq2  41708  mapdheq4  41711  mapdh6aN  41714  hdmap1l6a  41788  hdmap14lem4a  41850  lcmineqlem4  42005  frlmfzoccat  42478  drnginvmuld  42500  psrbagres  42519  evlselvlem  42559  evlselv  42560  fsuppind  42563  fsuppssind  42566  prjspvs  42583  irrapxlem4  42798  pell1234qrdich  42834  pell1qr1  42844  pell14qrgap  42848  pellqrexplicit  42850  rmspecfund  42882  fzmaxdif  42954  acongeq  42956  jm2.23  42969  jm3.1  42993  lmhmlnmsplit  43060  hbt  43103  dgrsub2  43108  proot1ex  43169  cantnfub  43294  cantnfresb  43297  cantnf2  43298  tfsconcatfv2  43313  tfsconcatrn  43315  tfsconcatb0  43317  naddcnff  43335  naddcnffo  43337  naddcnfid1  43340  naddcnfid2  43341  clublem  43583  dftrcl3  43693  mnugrud  44257  hashnzfz2  44294  dvconstbi  44307  ubelsupr  44998  restopn3  45129  wessf1ornlem  45163  lefldiveq  45274  iccintsng  45505  climsuse  45590  mullimc  45598  limcdm0  45600  limccog  45602  mullimcf  45605  constlimc  45606  idlimc  45608  limcperiod  45610  limsupre  45623  limcleqr  45626  neglimc  45629  addlimc  45630  0ellimcdiv  45631  xlimliminflimsup  45844  cncfshift  45856  cncfperiod  45861  cncfuni  45868  icccncfext  45869  cncfiooicclem1  45875  fperdvper  45901  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  mbfres2cn  45940  iblsplit  45948  stoweidlem7  45989  stoweidlem13  45995  stoweidlem26  46008  wallispilem3  46049  stirlinglem6  46061  stirlinglem10  46065  dirkercncf  46089  fourierdlem6  46095  fourierdlem11  46100  fourierdlem12  46101  fourierdlem15  46104  fourierdlem26  46115  fourierdlem42  46131  fourierdlem50  46138  fourierdlem51  46139  fourierdlem52  46140  fourierdlem54  46142  fourierdlem62  46150  fourierdlem79  46167  fourierdlem102  46190  fourierdlem114  46202  etransclem23  46239  3f1oss1  47060  zgeltp1eq  47294  setsnidel  47362  preimafvsnel  47364  iccpartres  47403  prpair  47486  fpprel2  47726  isubgrsubgr  47853  grimidvtxedg  47869  grimcnv  47872  isuspgrim  47880  upgrimpthslem2  47892  stgrnbgr0  47947  uhgrimgrlim  47970  gpg5nbgrvtx03starlem2  48044  gpg5nbgrvtx13starlem2  48047  isassintop  48182  rhmsubcALTV  48257  srhmsubcALTV  48297  fldhmsubcALTV  48305  rmfsupp  48345  scmfsupp  48347  mptcfsupp  48349  lcoel0  48401  lincsumcl  48404  lincscmcl  48405  lcoss  48409  lindsrng01  48441  lincreslvec3  48455  lindssnlvec  48459  zgtp1leeq  48494  lubsscl  48932  glbsscl  48933  idmon  48993  idepi  48994  iinfssc  49030  iinfsubc  49031  discsubc  49037  nelsubclem  49040  imassc  49126  imasubc3  49129  isnatd  49196  swapfiso  49258  fucoppc  49383  thinciso  49443  diagciso  49512  termolmd  49643