Theorem mpbir2and 714

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  7003  fveqressseq  7023  fmptsng  7114  fmptsnd  7115  fnprb  7154  fntpb  7155  fpr3g  8226  frrlem4  8230  1ellim  8424  isfsuppd  9270  fdmfifsupp  9279  fczfsuppd  9290  fsuppmptif  9303  fsuppco2  9307  fsuppcor  9308  dffi3  9335  suppr  9376  infpr  9409  ordtypelem7  9430  cantnf0  9585  cantnfp1lem1  9588  cantnfp1lem2  9589  cantnfp1lem3  9590  cantnflem1a  9595  cantnflem1d  9598  cantnflem1  9599  cantnf  9603  rankpwi  9736  carduni  9894  fin23lem32  10255  fpwwe2lem5  10547  fpwwe2lem11  10553  fpwwe2lem12  10554  fpwwe2  10555  inttsk  10686  grutsk1  10733  add20  11650  supaddc  12110  supadd  12111  supmul  12115  suprzcl  12573  uzid  12767  uzwo3  12857  rpnnen1lem5  12895  xrletrid  13070  xrre  13085  xrre3  13087  xleadd1a  13169  xlemul1a  13204  elioc2  13326  elico2  13327  elicc2  13328  elfz1eq  13452  fzadd2  13476  fznatpl1  13495  elfz1uz  13511  nn0fz0  13542  fzctr  13557  fzo1fzo0n0  13632  fzoaddel  13634  elincfzoext  13640  flid  13729  flval3  13736  fladdz  13746  fldiv  13781  modid  13817  hashf1lem1  14379  pfxccatin12d  14669  repswpfx  14709  2cshw  14737  pfx2  14871  wwlktovf1  14881  sqeqd  15090  01sqrexlem7  15172  max0add  15234  abs2difabs  15259  rddif  15265  fzomaxdiflem  15267  rexico  15278  icodiamlt  15362  limsupgre  15405  rlim3  15422  icco1  15464  rlimclim  15470  rlimuni  15474  rlimresb  15489  isercolllem2  15590  isercolllem3  15591  isercoll  15592  caucvgrlem  15597  caurcvgr  15598  iseraltlem3  15608  fsum00  15722  o1fsum  15737  bitsfzolem  16362  bitsfzo  16363  bitsmod  16364  bitscmp  16366  gcd0id  16447  gcdneg  16450  bezoutlem4  16470  nn0seqcvgd  16498  lcmneg  16531  lcmfunsnlem2lem2  16567  qredeq  16585  prmind2  16613  eulerthlem2  16710  pcpremul  16772  pcidlem  16801  pcgcd1  16806  fldivp1  16826  pcfaclem  16827  4sqlem17  16890  vdwlem1  16910  vdwlem6  16915  vdwlem12  16921  vdwlem13  16922  0ram  16949  ram0  16951  ramub1lem1  16955  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  chnccat  18550  rabsubmgmd  18630  submgmid  18632  subsubmgm  18636  mgmhmima  18641  mgmhmeql  18642  mndpfsupp  18693  mnd1  18705  sgrp2nmndlem4  18857  sgrp2nmndlem5  18858  0subg  19085  nmznsg  19101  ghmpreima  19171  ghmeql  19172  ghmnsgpreima  19174  kerf1ghm  19180  cntzsgrpcl  19267  cntzsubm  19271  cntzsubg  19272  cntzmhm  19274  symgextfo  19355  symgfixf1  19370  symgfixfolem1  19371  odlem2  19472  finodsubmsubg  19500  gexlem2  19515  gexcl2  19522  sylow1lem5  19535  subgslw  19549  slwhash  19557  fislw  19558  sylow3lem1  19560  lsmsubg  19587  efgredlemd  19677  efgredlem  19680  efgcpbllemb  19688  frgpuplem  19705  cyggeninv  19816  iscygd  19820  iscygodd  19821  gsumzadd  19855  gsumconst  19867  gsumpt  19895  gsum2dlem2  19904  gsum2d  19905  gsum2d2lem  19906  dprdfcntz  19950  eldprdi  19953  subgdmdprd  19969  subgdprd  19970  dprdpr  19985  ablfac1c  20006  ablfac1eu  20008  ablfaclem3  20022  ogrpaddlt  20071  ogrpsublt  20075  ring1  20249  subrngint  20495  rhmimasubrng  20501  cntzsubrng  20502  rhmeql  20538  rhmima  20539  cntzsubr  20541  rnghmsscmap2  20564  rnghmsscmap  20565  rnghmsubcsetc  20568  zrzeroorngc  20579  rhmsscmap2  20593  rhmsscmap  20594  rhmsubcsetc  20597  rhmsscrnghm  20600  rhmsubcrngc  20603  srhmsubc  20615  rhmsubc  20624  issubdrg  20715  fldhmsubc  20720  imadrhmcl  20732  isabvd  20747  abvdiv  20764  ornglmullt  20804  orngrmullt  20805  orngmullt  20806  ofldlt1  20810  lsslsp  20968  lsslspOLD  20969  lmhmima  21001  lmhmpreima  21002  lmhmeql  21009  lsmcl  21037  lspfixed  21085  rnglidlrng  21204  rngqiprngim  21261  rng2idl1cntr  21262  qsssubdrg  21383  gzrngunit  21390  pzriprnglem8  21445  evpmodpmf1o  21553  ocvpj  21674  dsmm0cl  21697  dsmmacl  21698  dsmmsubg  21700  dsmmlss  21701  frlmsplit2  21730  uvcff  21748  lindfrn  21778  f1lindf  21779  lindsss  21781  issubassa  21824  issubassa2  21849  snifpsrbag  21877  psrbaglesupp  21879  psrbaglecl  21880  psrbagaddcl  21881  psrbagcon  21882  mplsubglem  21955  mpllsslem  21956  mplassa  21978  subrgmpl  21988  mplcoe5  21996  mplbas2  21998  mplind  22026  mpfind  22071  ismhp2  22085  mhpmulcl  22093  mhplss  22099  ply1assa  22141  coe1tmmul2  22219  coe1tmmul  22220  cply1coe0bi  22245  dmatid  22438  dmatsubcl  22441  dmatscmcl  22446  scmatid  22457  scmataddcl  22459  scmatsubcl  22460  scmatmulcl  22461  smatvscl  22467  scmatrhmcl  22471  mat0scmat  22481  mat1scmat  22482  mdet0pr  22535  chmaidscmat  22791  distop  22938  indistopon  22944  ppttop  22950  epttop  22952  mretopd  23035  toponmre  23036  neiss  23052  opnneissb  23057  ssnei2  23059  innei  23068  neiptoptop  23074  ordtcld1  23140  ordtcld2  23141  lmconst  23204  cnpnei  23207  iscncl  23212  cnss1  23219  cnss2  23220  cncnpi  23221  cncnp  23223  cnconst2  23226  cnrest  23228  cnpresti  23231  cnpdis  23236  paste  23237  lmcnp  23247  cnhaus  23297  hauscmp  23350  2ndcomap  23401  1stcelcls  23404  1stccnp  23405  llyrest  23428  nllyrest  23429  llyidm  23431  nllyidm  23432  ssref  23455  reftr  23457  refun0  23458  dissnref  23471  kgentopon  23481  kgenidm  23490  kgencn3  23501  txcld  23546  neitx  23550  tx1cn  23552  tx2cn  23553  ptcld  23556  xkoccn  23562  txcnp  23563  ptcnp  23565  txcnmpt  23567  ptcn  23570  txdis1cn  23578  ptrescn  23582  txkgen  23595  xkoco1cn  23600  xkoco2cn  23601  xkococn  23603  xkoinjcn  23630  qtoptop2  23642  qtopuni  23645  qtopid  23648  qtopkgen  23653  basqtop  23654  tgqtop  23655  qtopss  23658  qtopeu  23659  qtoprest  23660  kqopn  23677  kqcld  23678  kqreglem2  23685  reghmph  23736  ordthmeolem  23744  qtopf1  23759  opnfbas  23785  isfil2  23799  fbasweak  23808  fsubbas  23810  filconn  23826  fbasrn  23827  rnelfmlem  23895  flimss2  23915  flimss1  23916  hausflim  23924  flimclslem  23927  flimsncls  23929  cnpflfi  23942  flfcnp2  23950  fclsfnflim  23970  cnextfvval  24008  cnextfres1  24011  symgtgp  24049  opnsubg  24051  ghmcnp  24058  qustgpopn  24063  qustgplem  24064  qustgphaus  24066  tsmsfbas  24071  ustfilxp  24156  utoptop  24177  utopbas  24178  restutopopn  24181  iducn  24225  cstucnd  24226  ucncn  24227  fmucnd  24234  cfilufg  24235  trcfilu  24236  cfiluweak  24237  neipcfilu  24238  psmetres2  24257  isxmetd  24269  xmetpsmet  24291  imasf1oxmet  24318  xblss2ps  24344  xblss2  24345  xblcntrps  24353  xblcntr  24354  blcld  24448  metustfbas  24500  cfilucfil  24502  restmetu  24513  ngptgp  24579  tngngpd  24596  nrmtngnrm  24601  tngnrg  24617  nlmvscn  24630  nrginvrcn  24635  nmo0  24678  nmoeq0  24679  nmoid  24685  nghmcn  24688  0nmhm  24698  blcvx  24741  iccntr  24765  xrge0tsms  24778  xmetdcn2  24781  metdstri  24795  metdscn  24800  rescncf  24842  cncfco  24852  oprpiece1res2  24897  cnheibor  24900  cnllycmp  24901  bndth  24903  ishtpyd  24920  isphtpyd  24931  pcoval2  24961  nmhmcn  25065  ipcn  25191  lmnn  25208  cfilss  25215  iscfil3  25218  cfilfcls  25219  cmetcaulem  25233  iscmet3lem2  25237  cfilres  25241  lmcau  25258  flimcfil  25259  cncmet  25267  rlmbn  25306  minveclem3b  25373  pjthlem1  25382  pjth2  25385  ivthlem3  25398  ovolssnul  25432  ovolctb  25435  ovoliunnul  25452  ovolsca  25460  ovolicopnf  25469  voliunlem2  25496  volsup  25501  dyadmaxlem  25542  vitalilem5  25557  mbfres  25589  mbfss  25591  mbfmulc2re  25593  mbfadd  25606  mbfmulc2  25608  mbflim  25613  i1faddlem  25638  i1fmullem  25639  mbfmul  25671  itg2mulc  25692  itg2cnlem1  25706  ibl0  25732  iblposlem  25737  itgreval  25742  iblneg  25748  iblss  25750  iblss2  25751  itgle  25755  iblconst  25763  iblabs  25774  iblabsr  25775  iblmulc2  25776  bddmulibl  25784  limciun  25839  limcun  25840  dvres2lem  25855  dvidlem  25860  dvcnp2  25865  dvcn  25866  cpnres  25882  dvaddbr  25883  dvmulbr  25884  dvcobr  25891  dvcjbr  25894  dvrec  25900  dvcnvlem  25921  dvferm  25933  dvlip2  25941  dveq0  25946  dv11cn  25947  dvivthlem1  25954  lhop1  25960  lhop2  25961  lhop  25962  dvcnvre  25965  dvfsumlem3  25976  dvfsumlem4  25977  dvfsumrlim  25979  dvfsum2  25982  ftc1a  25985  ftc1lem4  25987  ftc1lem6  25989  ftc1  25990  coe1mul3  26045  deg1addle2  26048  deg1sublt  26056  fta1blem  26117  drnguc1p  26120  ig1prsp  26127  plyco0  26138  plyeq0lem  26156  dgrub  26180  dgreq  26190  dgradd2  26214  dgrmul  26216  dgrcolem2  26220  dgrco  26221  plycpn  26237  plydivlem4  26244  plydiveu  26246  vieta1lem2  26259  vieta1  26260  aalioulem2  26281  aalioulem3  26282  aaliou3lem7  26297  tayl0  26309  ulmcn  26348  ulmdvlem3  26351  psercn  26376  abelth  26391  pilem3  26403  efif1olem1  26491  abslogimle  26522  argregt0  26559  argrege0  26560  logf1o2  26599  cxpsqrtlem  26651  cxpcn3  26698  abscxpbnd  26703  logreclem  26712  ang180lem2  26760  ang180lem3  26761  xrlimcnp  26918  harmonicbnd4  26961  fsumharmonic  26962  lgamgulmlem5  26983  lgambdd  26987  basellem4  27034  dvdsppwf1o  27136  dvdsflf1o  27137  fsumfldivdiaglem  27139  chpeq0  27159  chteq0  27160  chtub  27163  chpub  27171  dchrelbasd  27190  dchrmulcl  27200  dchrinv  27212  bposlem1  27235  bposlem2  27236  lgsdirprm  27282  lgsqrlem2  27298  lgsqrlem3  27299  lgsdchr  27306  lgseisenlem1  27326  lgseisenlem2  27327  lgseisenlem3  27328  lgsquadlem1  27331  2sqlem8  27377  2sqblem  27382  2sqmod  27387  chebbnd1lem1  27420  dchrisumlem1  27440  dchrisumlem2  27441  dchrisumlem3  27442  dchrisum0fno1  27462  pntrmax  27515  pntpbnd1a  27536  pntibndlem3  27543  pntlemn  27551  pntlemi  27555  pntlem3  27560  pntleml  27562  ostth1  27584  ostth2  27588  ostth3  27589  nosepon  27617  nolesgn2ores  27624  nogesgn1ores  27626  nosupres  27659  nosupbnd1lem2  27661  nosupbnd2lem1  27667  noinfres  27674  noinfbnd1lem2  27676  noinfbnd2lem1  27682  eqcuts3  27784  cofcutrtime  27907  divmuldivsd  28212  divdivs1d  28213  onsbnd  28261  nnsgt0  28319  bdayfinbndlem1  28447  ercgrg  28573  motco  28596  cnvmot  28597  legso  28655  mirmot  28731  colopp  28825  hphl  28827  lmicom  28844  lmimid  28850  lmimot  28854  hypcgrlem1  28855  hypcgrlem2  28856  trgcopyeulem  28861  inagswap  28897  inaghl  28901  cgrg3col4  28909  brbtwn2  28962  axlowdimlem3  29001  axlowdimlem16  29014  axcontlem8  29028  fusgrfis  29387  nbgr2vtx1edg  29407  0vtxrgr  29634  0vtxrusgr  29635  ewlkle  29663  wlk1ewlk  29697  uspgr2wlkeq2  29704  wlkp1lem8  29736  trlontrl  29766  pthonpth  29805  pthdlem2  29825  wlklnwwlkln1  29925  wlknewwlksn  29944  wwlksnred  29949  wwlksnredwwlkn0  29953  2trlond  29996  2pthond  29999  elwwlks2ons3im  30011  clwlkclwwlklem2a1  30051  clwlkclwwlkf1  30069  clwwlkel  30105  clwwlkwwlksb  30113  wwlksext2clwwlk  30116  1ewlk  30174  0trlon  30183  0pthon  30186  1pthond  30203  3trlond  30232  3pthond  30234  3spthond  30236  eupthres  30274  2clwwlk2clwwlk  30409  numclwwlk1lem2foa  30413  numclwwlk1lem2f1  30416  nvabs  30732  vacn  30754  nmcvcn  30755  nmblore  30846  0lno  30850  0blo  30852  nmlno0lem  30853  occl  31364  pjhthlem1  31451  pjpjpre  31479  nmopre  31930  nmlnop0iALT  32055  nmophmi  32091  leoprf2  32187  stlesi  32301  disjdifprg  32634  disjun0  32654  fsuppcurry1  32786  fsuppcurry2  32787  fpwrelmap  32795  fzspl  32852  dfmgc2lem  33060  pwrssmgc  33065  xrge0tsmsd  33139  psgnfzto1stlem  33166  fzto1st1  33168  evpmid  33214  pnfinf  33249  isarchiofld  33265  rmfsupp2  33304  fracfld  33374  dvdsruassoi  33449  nsgmgc  33477  drngidl  33498  qsdrngi  33560  deg1addlt  33665  ply1degltdimlem  33772  lbsdiflsp0  33776  fedgmul  33781  fldexttr  33808  fldextid  33809  irngnzply1lem  33840  finextalg  33848  minplyelirng  33865  irredminply  33866  algextdeglem8  33874  rtelextdg2lem  33876  constrsslem  33891  constrllcllem  33902  constrlccllem  33903  constrcccllem  33904  qtopt1  33985  reff  33989  locfinreflem  33990  metideq  34043  metider  34044  pstmxmet  34047  qqhval2lem  34131  qqhcn  34141  qqhucn  34142  pwsiga  34280  prsiga  34281  measle0  34358  mbfmcst  34409  1stmbfm  34410  2ndmbfm  34411  imambfm  34412  cnmbfm  34413  mbfmco  34414  mbfmco2  34415  0elcarsg  34457  carsgclctun  34471  sibfof  34490  oddpwdc  34504  eulerpartlemmf  34525  eulerpartlemgs2  34530  0rrv  34601  ballotlemfc0  34643  ballotlemfcc  34644  signstfveq0  34727  breprexplemc  34782  bnj1452  35200  usgrgt2cycl  35318  acycgr1v  35337  derangen  35360  subfacval3  35377  cvmseu  35464  cvmliftmolem2  35470  cvmliftlem7  35479  cvmliftlem15  35486  cvmlift2lem9a  35491  cvmlift2lem9  35499  cvmlift2lem10  35500  cvmlift2lem11  35501  cvmlift2lem12  35502  cvmlift3lem6  35512  cvmlift3lem8  35514  ex-sategoelel  35609  ex-sategoelelomsuc  35614  mclsppslem  35771  mclspps  35772  wsuclem  36011  fness  36537  fnetr  36539  fnessref  36545  refssfne  36546  neibastop1  36547  neibastop2  36549  tailfb  36565  filnetlem3  36568  weiunfrlem  36652  bj-finsumval0  37597  bj-rvecvec  37611  dfgcd3  37636  lindsadd  37925  poimirlem13  37945  poimirlem15  37947  poimirlem24  37956  poimirlem28  37960  mblfinlem2  37970  ovoliunnfl  37974  volsupnfl  37977  mbfresfi  37978  iblabsnc  37996  iblmulc2nc  37997  ftc1cnnclem  38003  ftc1cnnc  38004  ftc1anc  38013  sdclem2  38054  metf1o  38067  ismtyhmeolem  38116  ismtyres  38120  heibor1lem  38121  bfplem2  38135  bfp  38136  rrncmslem  38144  iccbnd  38152  icccmpALT  38153  rngogrphom  38283  rngoisoco  38294  keridl  38344  lsmcv2  39466  lsatcv0  39468  lcvexchlem4  39474  lcvexchlem5  39475  l1cvpat  39491  lfl0f  39506  lfladdcl  39508  lflnegcl  39512  lkrlss  39532  eqlkr  39536  lkrlsp  39539  lkrlsp2  39540  lshpkrcl  39553  lkrin  39601  1cvrjat  39912  llni  39945  llnle  39955  lplni  39969  lplnle  39977  llncvrlpln2  39994  2atmat  39998  lvoli  40012  lplncvrlvol2  40052  elpaddri  40239  paddclN  40279  pclclN  40328  pclfinN  40337  0psubclN  40380  1psubclN  40381  atpsubclN  40382  pmapsubclN  40383  osumclN  40404  pexmidN  40406  pexmidlem6N  40412  lhp2lt  40438  lautcnv  40527  idlaut  40533  lautco  40534  idldil  40551  ldilcnv  40552  ldilco  40553  ltrncnv  40583  idltrn  40587  cdleme16d  40718  cdleme50laut  40984  cdleme50ldil  40985  cdleme50ltrn  40994  ltrnco  41156  dian0  41476  dia0eldmN  41477  dia1eldmN  41478  dialss  41483  diaintclN  41495  docaclN  41561  doca2N  41563  djajN  41574  dibintclN  41604  diblss  41607  dicvaddcl  41627  dicvscacl  41628  dicn0  41629  cdlemn11a  41644  dihord2cN  41658  dihord11b  41659  dihord6apre  41693  dihmeetlem1N  41727  dihglblem5apreN  41728  dihpN  41773  dihjatcclem4  41858  dochkr1  41915  islpoldN  41921  lcfrlem31  42010  mapdpglem18  42126  mapdheq2  42166  mapdheq4  42169  mapdh6aN  42172  hdmap1l6a  42246  hdmap14lem4a  42308  lcmineqlem4  42463  frlmfzoccat  42949  drnginvmuld  42971  psrbagres  42988  evlselvlem  43018  evlselv  43019  fsuppind  43022  fsuppssind  43025  prjspvs  43042  irrapxlem4  43256  pell1234qrdich  43292  pell1qr1  43302  pell14qrgap  43306  pellqrexplicit  43308  rmspecfund  43340  fzmaxdif  43412  acongeq  43414  jm2.23  43427  jm3.1  43451  lmhmlnmsplit  43518  hbt  43561  dgrsub2  43566  proot1ex  43627  cantnfub  43752  cantnfresb  43755  cantnf2  43756  tfsconcatfv2  43771  tfsconcatrn  43773  tfsconcatb0  43775  naddcnff  43793  naddcnffo  43795  naddcnfid1  43798  naddcnfid2  43799  clublem  44040  dftrcl3  44150  mnugrud  44714  hashnzfz2  44751  dvconstbi  44764  ubelsupr  45454  restopn3  45584  wessf1ornlem  45618  lefldiveq  45728  iccintsng  45957  climsuse  46042  mullimc  46050  limcdm0  46052  limccog  46054  mullimcf  46057  constlimc  46058  idlimc  46060  limcperiod  46062  limsupre  46073  limcleqr  46076  neglimc  46079  addlimc  46080  0ellimcdiv  46081  xlimliminflimsup  46294  cncfshift  46306  cncfperiod  46311  cncfuni  46318  icccncfext  46319  cncfiooicclem1  46325  fperdvper  46351  ioodvbdlimc1lem2  46364  ioodvbdlimc2lem  46366  mbfres2cn  46390  iblsplit  46398  stoweidlem7  46439  stoweidlem13  46445  stoweidlem26  46458  wallispilem3  46499  stirlinglem6  46511  stirlinglem10  46515  dirkercncf  46539  fourierdlem6  46545  fourierdlem11  46550  fourierdlem12  46551  fourierdlem15  46554  fourierdlem26  46565  fourierdlem42  46581  fourierdlem50  46588  fourierdlem51  46589  fourierdlem52  46590  fourierdlem54  46592  fourierdlem62  46600  fourierdlem79  46617  fourierdlem102  46640  fourierdlem114  46652  etransclem23  46689  chnsubseq  47312  3f1oss1  47509  zgeltp1eq  47743  setsnidel  47811  preimafvsnel  47813  iccpartres  47852  prpair  47935  fpprel2  48175  isubgrsubgr  48303  grimidvtxedg  48319  grimcnv  48322  isuspgrim  48330  upgrimpthslem2  48342  stgrnbgr0  48398  uhgrimgrlim  48421  clnbgr3stgrgrlim  48453  gpg5nbgrvtx03starlem2  48503  gpg5nbgrvtx13starlem2  48506  gpg5edgnedg  48564  isassintop  48644  rhmsubcALTV  48719  srhmsubcALTV  48759  fldhmsubcALTV  48767  rmfsupp  48807  scmfsupp  48809  mptcfsupp  48811  lcoel0  48862  lincsumcl  48865  lincscmcl  48866  lcoss  48870  lindsrng01  48902  lincreslvec3  48916  lindssnlvec  48920  zgtp1leeq  48955  lubsscl  49393  glbsscl  49394  idmon  49453  idepi  49454  iinfssc  49490  iinfsubc  49491  discsubc  49497  nelsubclem  49500  imassc  49586  imasubc3  49589  isnatd  49656  swapfiso  49718  fucoppc  49843  thinciso  49903  diagciso  49972  termolmd  50103