Theorem mpbir2and 725

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 520	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 260	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  elpreimad  7054  fveqressseq  7074  fmptsng  7166  fmptsnd  7167  fnprb  7206  fntpb  7207  fpr3g  8281  frrlem4  8285  1ellim  8482  isfsuppd  9325  fdmfifsupp  9334  fsuppmptif  9358  fsuppco2  9362  fsuppcor  9363  dffi3  9390  suppr  9431  infpr  9464  ordtypelem7  9485  cantnf0  9643  cantnfp1lem1  9646  cantnfp1lem2  9647  cantnfp1lem3  9648  cantnflem1a  9653  cantnflem1d  9656  cantnflem1  9657  cantnf  9661  rankpwi  9794  carduni  9966  fin23lem32  10327  fpwwe2lem5  10619  fpwwe2lem11  10625  fpwwe2lem12  10626  fpwwe2  10627  inttsk  10758  grutsk1  10805  add20  11725  supaddc  12181  supadd  12182  supmul  12186  suprzcl  12675  uzid  12876  uzwo3  12966  rpnnen1lem5  13004  xrletrid  13179  xrre  13194  xrre3  13196  xleadd1a  13278  xlemul1a  13313  elioc2  13435  elico2  13436  elicc2  13437  elfz1eq  13562  fzadd2  13586  fznatpl1  13605  elfz1uz  13621  nn0fz0  13652  fzctr  13667  fzo1fzo0n0  13743  fzoaddel  13745  elincfzoext  13751  flid  13840  flval3  13847  fladdz  13857  fldiv  13892  modid  13928  hashf1lem1  14491  pfxccatin12d  14781  repswpfx  14821  2cshw  14849  pfx2  14983  wwlktovf1  14993  sqeqd  15216  01sqrexlem7  15298  max0add  15360  abs2difabs  15385  rddif  15391  fzomaxdiflem  15393  rexico  15404  icodiamlt  15488  limsupgre  15531  rlim3  15548  icco1  15590  rlimclim  15596  rlimuni  15600  rlimresb  15615  isercolllem2  15716  isercolllem3  15717  isercoll  15718  caucvgrlem  15723  caurcvgr  15724  iseraltlem3  15734  fsum00  15849  o1fsum  15864  bitsfzolem  16491  bitsfzo  16492  bitsmod  16493  bitscmp  16495  gcd0id  16576  gcdneg  16579  bezoutlem4  16599  nn0seqcvgd  16627  lcmneg  16660  lcmfunsnlem2lem2  16696  qredeq  16714  prmind2  16742  eulerthlem2  16840  pcpremul  16902  pcidlem  16931  pcgcd1  16936  fldivp1  16956  pcfaclem  16957  4sqlem17  17020  vdwlem1  17040  vdwlem6  17045  vdwlem12  17051  vdwlem13  17052  0ram  17079  ram0  17081  ramub1lem1  17085  invco  17827  sectmon  17838  monsect  17839  invid  17843  ssctr  17881  ssceq  17882  0ssc  17893  0subcat  17894  catsubcat  17895  issubc3  17905  fullsubc  17906  funcinv  17929  fthmon  17985  fuccocl  18023  fucidcl  18024  invfuc  18033  2initoinv  18066  2termoinv  18073  elhomai  18089  setcmon  18143  setcepi  18144  catcisolem  18166  curf2cl  18286  yonedalem4c  18332  yonedalem3  18335  yoniso  18340  lublecl  18414  isacs3lem  18597  tsrdir  18659  chnccat  18681  rabsubmgmd  18761  submgmid  18763  subsubmgm  18767  mgmhmima  18772  mgmhmeql  18773  mndpfsupp  18824  mnd1  18836  sgrp2nmndlem4  18989  sgrp2nmndlem5  18990  0subg  19217  nmznsg  19233  ghmpreima  19307  ghmeql  19308  ghmnsgpreima  19310  kerf1ghm  19316  cntzsgrpcl  19403  cntzsubm  19407  cntzsubg  19408  cntzmhm  19410  symgextfo  19491  symgfixf1  19506  symgfixfolem1  19507  odlem2  19608  finodsubmsubg  19636  gexlem2  19651  gexcl2  19658  sylow1lem5  19671  subgslw  19685  slwhash  19693  fislw  19694  sylow3lem1  19696  lsmsubg  19723  efgredlemd  19813  efgredlem  19816  efgcpbllemb  19824  frgpuplem  19841  cyggeninv  19952  iscygd  19956  iscygodd  19957  gsumzadd  19991  gsumconst  20003  gsumpt  20031  gsum2dlem2  20040  gsum2d  20041  gsum2d2lem  20042  dprdfcntz  20086  eldprdi  20089  subgdmdprd  20105  subgdprd  20106  dprdpr  20121  ablfac1c  20142  ablfac1eu  20144  ablfaclem3  20158  ogrpaddlt  20207  ogrpsublt  20211  ring1  20392  subrngint  20644  rhmimasubrng  20650  cntzsubrng  20651  rhmeql  20687  rhmima  20688  cntzsubr  20690  rnghmsscmap2  20713  rnghmsscmap  20714  rnghmsubcsetc  20717  zrzeroorngc  20728  rhmsscmap2  20742  rhmsscmap  20743  rhmsubcsetc  20746  rhmsscrnghm  20749  rhmsubcrngc  20752  srhmsubc  20764  rhmsubc  20773  issubdrg  20862  fldhmsubc  20867  imadrhmcl  20879  isabvd  20894  abvdiv  20911  ornglmullt  20951  orngrmullt  20952  orngmullt  20953  ofldlt1  20957  lsslsp  21115  lmhmima  21147  lmhmpreima  21148  lmhmeql  21155  lsmcl  21183  lspfixed  21231  rnglidlrng  21360  drngidl  21364  rngqiprngim  21423  rng2idl1cntr  21424  qsssubdrg  21555  gzrngunit  21562  pzriprnglem8  21617  evpmodpmf1o  21725  ocvpj  21846  dsmm0cl  21869  dsmmacl  21870  dsmmsubg  21872  dsmmlss  21873  frlmsplit2  21902  uvcff  21920  lindfrn  21950  f1lindf  21951  lindsss  21953  issubassa  21996  issubassa2  22021  snifpsrbag  22049  psrbaglesupp  22051  psrbaglecl  22052  psrbagaddcl  22053  psrbagcon  22054  psrbagres  22059  mplsubglem  22127  mpllsslem  22128  mplassa  22150  subrgmpl  22161  mplcoe5  22170  mplbas2  22172  mplind  22200  mpfind  22245  ismhp2  22283  mhpmulcl  22291  mhplss  22297  ply1assa  22338  coe1tmmul2  22416  coe1tmmul  22417  cply1coe0bi  22441  dmatid  22631  dmatsubcl  22634  dmatscmcl  22639  scmatid  22650  scmataddcl  22652  scmatsubcl  22653  scmatmulcl  22654  smatvscl  22660  scmatrhmcl  22664  mat0scmat  22674  mat1scmat  22675  mdet0pr  22728  chmaidscmat  22984  distop  23131  indistopon  23137  ppttop  23143  epttop  23145  mretopd  23228  toponmre  23229  neiss  23245  opnneissb  23250  ssnei2  23252  innei  23261  neiptoptop  23267  ordtcld1  23333  ordtcld2  23334  lmconst  23397  cnpnei  23400  iscncl  23405  cnss1  23412  cnss2  23413  cncnpi  23414  cncnp  23416  cnconst2  23419  cnrest  23421  cnpresti  23424  cnpdis  23429  paste  23430  lmcnp  23440  cnhaus  23490  hauscmp  23543  2ndcomap  23594  1stcelcls  23597  1stccnp  23598  llyrest  23621  nllyrest  23622  llyidm  23624  nllyidm  23625  ssref  23648  reftr  23650  refun0  23651  dissnref  23664  kgentopon  23674  kgenidm  23683  kgencn3  23694  txcld  23739  neitx  23743  tx1cn  23745  tx2cn  23746  ptcld  23749  xkoccn  23755  txcnp  23756  ptcnp  23758  txcnmpt  23760  ptcn  23763  txdis1cn  23771  ptrescn  23775  txkgen  23788  xkoco1cn  23793  xkoco2cn  23794  xkococn  23796  xkoinjcn  23823  qtoptop2  23835  qtopuni  23838  qtopid  23841  qtopkgen  23846  basqtop  23847  tgqtop  23848  qtopss  23851  qtopeu  23852  qtoprest  23853  kqopn  23870  kqcld  23871  kqreglem2  23878  reghmph  23929  ordthmeolem  23937  qtopf1  23952  opnfbas  23978  isfil2  23992  fbasweak  24001  fsubbas  24003  filconn  24019  fbasrn  24020  rnelfmlem  24088  flimss2  24108  flimss1  24109  hausflim  24117  flimclslem  24120  flimsncls  24122  cnpflfi  24135  flfcnp2  24143  fclsfnflim  24163  cnextfvval  24201  cnextfres1  24204  symgtgp  24242  opnsubg  24244  ghmcnp  24251  qustgpopn  24256  qustgplem  24257  qustgphaus  24259  tsmsfbas  24264  ustfilxp  24349  utoptop  24370  utopbas  24371  restutopopn  24374  iducn  24418  cstucnd  24419  ucncn  24420  fmucnd  24427  cfilufg  24428  trcfilu  24429  cfiluweak  24430  neipcfilu  24431  psmetres2  24450  isxmetd  24462  xmetpsmet  24484  imasf1oxmet  24511  xblss2ps  24537  xblss2  24538  xblcntrps  24546  xblcntr  24547  blcld  24641  metustfbas  24693  cfilucfil  24695  restmetu  24706  ngptgp  24772  tngngpd  24789  nrmtngnrm  24794  tngnrg  24810  nlmvscn  24823  nrginvrcn  24828  nmo0  24871  nmoeq0  24872  nmoid  24878  nghmcn  24881  0nmhm  24891  blcvx  24934  iccntr  24958  xrge0tsms  24971  xmetdcn2  24974  metdstri  24988  metdscn  24993  rescncf  25035  cncfco  25045  oprpiece1res2  25090  cnheibor  25093  cnllycmp  25094  bndth  25096  ishtpyd  25113  isphtpyd  25124  pcoval2  25154  nmhmcn  25258  ipcn  25384  lmnn  25401  cfilss  25408  iscfil3  25411  cfilfcls  25412  cmetcaulem  25426  iscmet3lem2  25430  cfilres  25434  lmcau  25451  flimcfil  25452  cncmet  25460  rlmbn  25499  minveclem3b  25566  pjthlem1  25575  pjth2  25578  ivthlem3  25591  ovolssnul  25625  ovolctb  25628  ovoliunnul  25645  ovolsca  25653  ovolicopnf  25662  voliunlem2  25689  volsup  25694  dyadmaxlem  25735  vitalilem5  25750  mbfres  25782  mbfss  25784  mbfmulc2re  25786  mbfadd  25799  mbfmulc2  25801  mbflim  25806  i1faddlem  25831  i1fmullem  25832  mbfmul  25864  itg2mulc  25885  itg2cnlem1  25899  ibl0  25925  iblposlem  25930  itgreval  25935  iblneg  25941  iblss  25943  iblss2  25944  itgle  25948  iblconst  25956  iblabs  25967  iblabsr  25968  iblmulc2  25969  bddmulibl  25977  limciun  26032  limcun  26033  dvres2lem  26048  dvidlem  26053  dvcnp2  26058  dvcn  26059  cpnres  26075  dvaddbr  26076  dvmulbr  26077  dvcobr  26084  dvcjbr  26087  dvrec  26093  dvcnvlem  26114  dvferm  26126  dvlip2  26133  dveq0  26138  dv11cn  26139  dvivthlem1  26146  lhop1  26152  lhop2  26153  lhop  26154  dvcnvre  26157  dvfsumlem3  26166  dvfsumlem4  26167  dvfsumrlim  26169  dvfsum2  26172  ftc1a  26175  ftc1lem4  26177  ftc1lem6  26179  ftc1  26180  coe1mul3  26235  deg1addle2  26238  deg1sublt  26246  fta1blem  26307  drnguc1p  26310  ig1prsp  26317  plyco0  26328  plyeq0lem  26346  dgrub  26370  dgreq  26380  dgradd2  26404  dgrmul  26406  dgrcolem2  26410  dgrco  26411  plycpn  26429  plydivlem4  26436  plydiveu  26438  vieta1lem2  26451  vieta1  26452  aalioulem2  26473  aalioulem3  26474  aaliou3lem7  26489  tayl0  26501  ulmcn  26538  ulmdvlem3  26541  psercn  26565  abelth  26580  pilem3  26592  efif1olem1  26683  abslogimle  26714  argregt0  26751  argrege0  26752  logf1o2  26791  cxpsqrtlem  26843  cxpcn3  26889  abscxpbnd  26894  logreclem  26903  ang180lem2  26951  ang180lem3  26952  xrlimcnp  27109  harmonicbnd4  27151  fsumharmonic  27152  lgamgulmlem5  27173  lgambdd  27177  basellem4  27224  dvdsppwf1o  27326  dvdsflf1o  27327  fsumfldivdiaglem  27329  chpeq0  27348  chteq0  27349  chtub  27352  chpub  27360  dchrelbasd  27379  dchrmulcl  27389  dchrinv  27401  bposlem1  27424  bposlem2  27425  lgsdirprm  27471  lgsqrlem2  27487  lgsqrlem3  27488  lgsdchr  27495  lgseisenlem1  27515  lgseisenlem2  27516  lgseisenlem3  27517  lgsquadlem1  27520  2sqlem8  27566  2sqblem  27571  2sqmod  27576  chebbnd1lem1  27609  dchrisumlem1  27629  dchrisumlem2  27630  dchrisumlem3  27631  dchrisum0fno1  27651  pntrmax  27704  pntpbnd1a  27725  pntibndlem3  27732  pntlemn  27740  pntlemi  27744  pntlem3  27749  pntleml  27751  ostth1  27773  ostth2  27777  ostth3  27778  nosepon  27805  nolesgn2ores  27812  nogesgn1ores  27814  nosupres  27847  nosupbnd1lem2  27849  nosupbnd2lem1  27855  noinfres  27862  noinfbnd1lem2  27864  noinfbnd2lem1  27870  eqcuts3  27973  cofcutrtime  28096  divmuldivsd  28401  divdivs1d  28402  onsbnd  28450  nnsgt0  28508  bdayfinbndlem1  28636  ercgrg  28762  motco  28785  cnvmot  28786  legso  28844  mirmot  28928  colopp  29026  hphl  29028  lmicom  29071  lmimid  29077  lmimot  29081  hypcgrlem1  29082  hypcgrlem2  29083  trgcopyeulem  29089  inagswap  29131  inaghl  29135  cgrg3col4  29143  prlngd  29162  prlngref  29163  dfprlng2  29170  brbtwn2  29221  axlowdimlem3  29260  axlowdimlem16  29273  axcontlem8  29287  fusgrfis  29646  nbgr2vtx1edg  29666  0vtxrgr  29892  0vtxrusgr  29893  ewlkle  29921  wlk1ewlk  29955  uspgr2wlkeq2  29962  wlkp1lem8  29994  trlontrl  30024  pthonpth  30063  pthdlem2  30083  wlklnwwlkln1  30183  wlknewwlksn  30202  wwlksnred  30207  wwlksnredwwlkn0  30211  2trlond  30254  2pthond  30257  elwwlks2ons3im  30269  clwlkclwwlklem2a1  30309  clwlkclwwlkf1  30327  clwwlkel  30363  clwwlkwwlksb  30371  wwlksext2clwwlk  30374  1ewlk  30432  0trlon  30441  0pthon  30444  1pthond  30461  3trlond  30490  3pthond  30492  3spthond  30494  eupthres  30532  2clwwlk2clwwlk  30667  numclwwlk1lem2foa  30671  numclwwlk1lem2f1  30674  nvabs  30990  vacn  31012  nmcvcn  31013  nmblore  31104  0lno  31108  0blo  31110  nmlno0lem  31111  occl  31622  pjhthlem1  31709  pjpjpre  31737  nmopre  32188  nmlnop0iALT  32313  nmophmi  32349  leoprf2  32445  stlesi  32559  disjdifprg  32886  disjun0  32906  fsuppcurry1  33035  fsuppcurry2  33036  fpwrelmap  33044  fzspl  33100  dfmgc2lem  33281  pwrssmgc  33286  xrge0tsmsd  33359  psgnfzto1stlem  33386  fzto1st1  33388  evpmid  33434  pnfinf  33469  isarchiofld  33485  rmfsupp2  33523  fracfld  33595  dvdsruassoi  33663  nsgmgc  33687  qsdrngi  33743  deg1addlt  33856  ply1degltdimlem  33978  lbsdiflsp0  33982  fedgmul  33987  fldexttr  34014  fldextid  34015  irngnzply1lem  34046  finextalg  34054  minplyelirng  34071  irredminply  34072  algextdeglem8  34080  rtelextdg2lem  34082  constrsslem  34097  constrllcllem  34108  constrlccllem  34109  constrcccllem  34110  qtopt1  34191  reff  34195  locfinreflem  34196  metideq  34249  metider  34250  pstmxmet  34253  qqhval2lem  34337  qqhcn  34347  qqhucn  34348  pwsiga  34486  prsiga  34487  measle0  34564  mbfmcst  34615  1stmbfm  34616  2ndmbfm  34617  imambfm  34618  cnmbfm  34619  mbfmco  34620  mbfmco2  34621  0elcarsg  34663  carsgclctun  34677  sibfof  34696  oddpwdc  34710  eulerpartlemmf  34731  eulerpartlemgs2  34736  0rrv  34807  ballotlemfc0  34849  ballotlemfcc  34850  signstfveq0  34930  breprexplemc  34985  bnj1452  35406  usgrgt2cycl  35576  acycgr1v  35595  derangen  35618  subfacval3  35635  cvmseu  35722  cvmliftmolem2  35728  cvmliftlem7  35737  cvmliftlem15  35744  cvmlift2lem9a  35749  cvmlift2lem9  35757  cvmlift2lem10  35758  cvmlift2lem11  35759  cvmlift2lem12  35760  cvmlift3lem6  35770  cvmlift3lem8  35772  ex-sategoelel  35867  ex-sategoelelomsuc  35872  mclsppslem  36029  mclspps  36030  wsuclem  36269  fness  36804  fnetr  36806  fnessref  36812  refssfne  36813  neibastop1  36814  neibastop2  36816  tailfb  36832  filnetlem3  36835  weiunfrlem  36919  bj-finsumval0  37873  bj-rvecvec  37887  dfgcd3  37912  lindsadd  38208  poimirlem13  38228  poimirlem15  38230  poimirlem24  38239  poimirlem28  38243  mblfinlem2  38253  ovoliunnfl  38257  volsupnfl  38260  mbfresfi  38261  iblabsnc  38279  iblmulc2nc  38280  ftc1cnnclem  38286  ftc1cnnc  38287  ftc1anc  38296  sdclem2  38337  metf1o  38350  ismtyhmeolem  38399  ismtyres  38403  heibor1lem  38404  bfplem2  38418  bfp  38419  rrncmslem  38427  iccbnd  38435  icccmpALT  38436  rngogrphom  38566  rngoisoco  38577  keridl  38627  lsmcv2  39749  lsatcv0  39751  lcvexchlem4  39757  lcvexchlem5  39758  l1cvpat  39774  lfl0f  39789  lfladdcl  39791  lflnegcl  39795  lkrlss  39815  eqlkr  39819  lkrlsp  39822  lkrlsp2  39823  lshpkrcl  39836  lkrin  39884  1cvrjat  40195  llni  40228  llnle  40238  lplni  40252  lplnle  40260  llncvrlpln2  40277  2atmat  40281  lvoli  40295  lplncvrlvol2  40335  elpaddri  40522  paddclN  40562  pclclN  40611  pclfinN  40620  0psubclN  40663  1psubclN  40664  atpsubclN  40665  pmapsubclN  40666  osumclN  40687  pexmidN  40689  pexmidlem6N  40695  lhp2lt  40721  lautcnv  40810  idlaut  40816  lautco  40817  idldil  40834  ldilcnv  40835  ldilco  40836  ltrncnv  40866  idltrn  40870  cdleme16d  41001  cdleme50laut  41267  cdleme50ldil  41268  cdleme50ltrn  41277  ltrnco  41439  dian0  41759  dia0eldmN  41760  dia1eldmN  41761  dialss  41766  diaintclN  41778  docaclN  41844  doca2N  41846  djajN  41857  dibintclN  41887  diblss  41890  dicvaddcl  41910  dicvscacl  41911  dicn0  41912  cdlemn11a  41927  dihord2cN  41941  dihord11b  41942  dihord6apre  41976  dihmeetlem1N  42010  dihglblem5apreN  42011  dihpN  42056  dihjatcclem4  42141  dochkr1  42198  islpoldN  42204  lcfrlem31  42293  mapdpglem18  42409  mapdheq2  42449  mapdheq4  42452  mapdh6aN  42455  hdmap1l6a  42529  hdmap14lem4a  42591  lcmineqlem4  42745  frlmfzoccat  43225  drnginvmuld  43243  evlselvlem  43268  evlselv  43269  fsuppind  43270  fsuppssind  43273  prjspvs  43290  irrapxlem4  43500  pell1234qrdich  43536  pell1qr1  43546  pell14qrgap  43550  pellqrexplicit  43552  rmspecfund  43584  fzmaxdif  43656  acongeq  43658  jm2.23  43671  jm3.1  43695  lmhmlnmsplit  43762  hbt  43805  dgrsub2  43810  proot1ex  43871  cantnfub  43996  cantnfresb  43999  cantnf2  44000  tfsconcatfv2  44015  tfsconcatrn  44017  tfsconcatb0  44019  naddcnff  44037  naddcnffo  44039  naddcnfid1  44042  naddcnfid2  44043  clublem  44284  dftrcl3  44394  mnugrud  44942  hashnzfz2  44979  dvconstbi  44992  ubelsupr  45688  restopn3  45817  wessf1ornlem  45851  lefldiveq  45959  iccintsng  46187  climsuse  46272  mullimc  46280  limcdm0  46282  limccog  46284  mullimcf  46287  constlimc  46288  idlimc  46290  limcperiod  46292  limsupre  46303  limcleqr  46306  neglimc  46309  addlimc  46310  0ellimcdiv  46311  xlimliminflimsup  46524  cncfshift  46536  cncfperiod  46541  cncfuni  46548  icccncfext  46549  cncfiooicclem1  46555  fperdvper  46581  ioodvbdlimc1lem2  46594  ioodvbdlimc2lem  46596  mbfres2cn  46620  iblsplit  46628  stoweidlem7  46669  stoweidlem13  46675  stoweidlem26  46688  wallispilem3  46729  stirlinglem6  46741  stirlinglem10  46745  dirkercncf  46769  fourierdlem6  46775  fourierdlem11  46780  fourierdlem12  46781  fourierdlem15  46784  fourierdlem26  46795  fourierdlem42  46811  fourierdlem50  46818  fourierdlem51  46819  fourierdlem52  46820  fourierdlem54  46822  fourierdlem62  46830  fourierdlem79  46847  fourierdlem102  46870  fourierdlem114  46882  etransclem23  46919  chnsubseq  47544  3f1oss1  47757  zgeltp1eq  47991  nnmul2  48012  setsnidel  48071  preimafvsnel  48073  iccpartres  48112  prpair  48195  fpprel2  48451  isubgrsubgr  48579  grimidvtxedg  48595  grimcnv  48598  isuspgrim  48606  upgrimpthslem2  48618  stgrnbgr0  48674  uhgrimgrlim  48697  clnbgr3stgrgrlim  48729  gpg5nbgrvtx03starlem2  48779  gpg5nbgrvtx13starlem2  48782  gpg5edgnedg  48840  isassintop  48920  rhmsubcALTV  48995  srhmsubcALTV  49035  fldhmsubcALTV  49043  rmfsupp  49098  scmfsupp  49100  mptcfsupp  49102  lcoel0  49153  lincsumcl  49156  lincscmcl  49157  lcoss  49161  lindsrng01  49193  lincreslvec3  49207  lindssnlvec  49211  zgtp1leeq  49246  lubsscl  49683  glbsscl  49684  idmon  49743  idepi  49744  iinfssc  49780  iinfsubc  49781  discsubc  49787  nelsubclem  49790  imassc  49876  imasubc3  49879  isnatd  49946  swapfiso  50008  fucoppc  50133  thinciso  50193  diagciso  50262  termolmd  50393