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  7033  fveqressseq  7053  fmptsng  7144  fmptsnd  7145  fnprb  7184  fntpb  7185  fpr3g  8266  frrlem4  8270  1ellim  8464  isfsuppd  9323  fdmfifsupp  9332  fczfsuppd  9343  fsuppmptif  9356  fsuppco2  9360  fsuppcor  9361  dffi3  9388  suppr  9429  infpr  9462  ordtypelem7  9483  cantnf0  9634  cantnfp1lem1  9637  cantnfp1lem2  9638  cantnfp1lem3  9639  cantnflem1a  9644  cantnflem1d  9647  cantnflem1  9648  cantnf  9652  rankpwi  9782  carduni  9940  fin23lem32  10303  fpwwe2lem5  10594  fpwwe2lem11  10600  fpwwe2lem12  10601  fpwwe2  10602  inttsk  10733  grutsk1  10780  add20  11696  supaddc  12156  supadd  12157  supmul  12161  suprzcl  12620  uzid  12814  uzwo3  12908  rpnnen1lem5  12946  xrletrid  13121  xrre  13135  xrre3  13137  xleadd1a  13219  xlemul1a  13254  elioc2  13376  elico2  13377  elicc2  13378  elfz1eq  13502  fzadd2  13526  fznatpl1  13545  elfz1uz  13561  nn0fz0  13592  fzctr  13607  fzo1fzo0n0  13682  fzoaddel  13684  elincfzoext  13690  flid  13776  flval3  13783  fladdz  13793  fldiv  13828  modid  13864  hashf1lem1  14426  pfxccatin12d  14716  repswpfx  14756  2cshw  14784  pfx2  14919  wwlktovf1  14929  sqeqd  15138  01sqrexlem7  15220  max0add  15282  abs2difabs  15307  rddif  15313  fzomaxdiflem  15315  rexico  15326  icodiamlt  15410  limsupgre  15453  rlim3  15470  icco1  15512  rlimclim  15518  rlimuni  15522  rlimresb  15537  isercolllem2  15638  isercolllem3  15639  isercoll  15640  caucvgrlem  15645  caurcvgr  15646  iseraltlem3  15656  fsum00  15770  o1fsum  15785  bitsfzolem  16410  bitsfzo  16411  bitsmod  16412  bitscmp  16414  gcd0id  16495  gcdneg  16498  bezoutlem4  16518  nn0seqcvgd  16546  lcmneg  16579  lcmfunsnlem2lem2  16615  qredeq  16633  prmind2  16661  eulerthlem2  16758  pcpremul  16820  pcidlem  16849  pcgcd1  16854  fldivp1  16874  pcfaclem  16875  4sqlem17  16938  vdwlem1  16958  vdwlem6  16963  vdwlem12  16969  vdwlem13  16970  0ram  16997  ram0  16999  ramub1lem1  17003  invco  17739  sectmon  17750  monsect  17751  invid  17755  ssctr  17793  ssceq  17794  0ssc  17805  0subcat  17806  catsubcat  17807  issubc3  17817  fullsubc  17818  funcinv  17841  fthmon  17897  fuccocl  17935  fucidcl  17936  invfuc  17945  2initoinv  17978  2termoinv  17985  elhomai  18001  setcmon  18055  setcepi  18056  catcisolem  18078  curf2cl  18198  yonedalem4c  18244  yonedalem3  18247  yoniso  18252  lublecl  18326  isacs3lem  18507  tsrdir  18569  rabsubmgmd  18637  submgmid  18639  subsubmgm  18643  mgmhmima  18648  mgmhmeql  18649  mndpfsupp  18700  mnd1  18712  sgrp2nmndlem4  18861  sgrp2nmndlem5  18862  0subg  19089  nmznsg  19106  ghmpreima  19176  ghmeql  19177  ghmnsgpreima  19179  kerf1ghm  19185  cntzsgrpcl  19272  cntzsubm  19276  cntzsubg  19277  cntzmhm  19279  symgextfo  19358  symgfixf1  19373  symgfixfolem1  19374  odlem2  19475  finodsubmsubg  19503  gexlem2  19518  gexcl2  19525  sylow1lem5  19538  subgslw  19552  slwhash  19560  fislw  19561  sylow3lem1  19563  lsmsubg  19590  efgredlemd  19680  efgredlem  19683  efgcpbllemb  19691  frgpuplem  19708  cyggeninv  19819  iscygd  19823  iscygodd  19824  gsumzadd  19858  gsumconst  19870  gsumpt  19898  gsum2dlem2  19907  gsum2d  19908  gsum2d2lem  19909  dprdfcntz  19953  eldprdi  19956  subgdmdprd  19972  subgdprd  19973  dprdpr  19988  ablfac1c  20009  ablfac1eu  20011  ablfaclem3  20025  ring1  20225  subrngint  20475  rhmimasubrng  20481  cntzsubrng  20482  rhmeql  20518  rhmima  20519  cntzsubr  20521  rnghmsscmap2  20544  rnghmsscmap  20545  rnghmsubcsetc  20548  zrzeroorngc  20559  rhmsscmap2  20573  rhmsscmap  20574  rhmsubcsetc  20577  rhmsscrnghm  20580  rhmsubcrngc  20583  srhmsubc  20595  rhmsubc  20604  issubdrg  20695  fldhmsubc  20700  imadrhmcl  20712  isabvd  20727  abvdiv  20744  lsslsp  20927  lsslspOLD  20928  lmhmima  20960  lmhmpreima  20961  lmhmeql  20968  lsmcl  20996  lspfixed  21044  rnglidlrng  21163  rngqiprngim  21220  rng2idl1cntr  21221  qsssubdrg  21349  gzrngunit  21356  pzriprnglem8  21404  evpmodpmf1o  21511  ocvpj  21632  dsmm0cl  21655  dsmmacl  21656  dsmmsubg  21658  dsmmlss  21659  frlmsplit2  21688  uvcff  21706  lindfrn  21736  f1lindf  21737  lindsss  21739  issubassa  21782  issubassa2  21807  snifpsrbag  21835  psrbaglesupp  21837  psrbaglecl  21838  psrbagaddcl  21839  psrbagcon  21840  mplsubglem  21914  mpllsslem  21915  mplassa  21937  subrgmpl  21945  mplcoe5  21953  mplbas2  21955  mplind  21983  mpfind  22020  ismhp2  22034  mhpmulcl  22042  mhplss  22048  ply1assa  22090  coe1tmmul2  22168  coe1tmmul  22169  cply1coe0bi  22195  dmatid  22388  dmatsubcl  22391  dmatscmcl  22396  scmatid  22407  scmataddcl  22409  scmatsubcl  22410  scmatmulcl  22411  smatvscl  22417  scmatrhmcl  22421  mat0scmat  22431  mat1scmat  22432  mdet0pr  22485  chmaidscmat  22741  distop  22888  indistopon  22894  ppttop  22900  epttop  22902  mretopd  22985  toponmre  22986  neiss  23002  opnneissb  23007  ssnei2  23009  innei  23018  neiptoptop  23024  ordtcld1  23090  ordtcld2  23091  lmconst  23154  cnpnei  23157  iscncl  23162  cnss1  23169  cnss2  23170  cncnpi  23171  cncnp  23173  cnconst2  23176  cnrest  23178  cnpresti  23181  cnpdis  23186  paste  23187  lmcnp  23197  cnhaus  23247  hauscmp  23300  2ndcomap  23351  1stcelcls  23354  1stccnp  23355  llyrest  23378  nllyrest  23379  llyidm  23381  nllyidm  23382  ssref  23405  reftr  23407  refun0  23408  dissnref  23421  kgentopon  23431  kgenidm  23440  kgencn3  23451  txcld  23496  neitx  23500  tx1cn  23502  tx2cn  23503  ptcld  23506  xkoccn  23512  txcnp  23513  ptcnp  23515  txcnmpt  23517  ptcn  23520  txdis1cn  23528  ptrescn  23532  txkgen  23545  xkoco1cn  23550  xkoco2cn  23551  xkococn  23553  xkoinjcn  23580  qtoptop2  23592  qtopuni  23595  qtopid  23598  qtopkgen  23603  basqtop  23604  tgqtop  23605  qtopss  23608  qtopeu  23609  qtoprest  23610  kqopn  23627  kqcld  23628  kqreglem2  23635  reghmph  23686  ordthmeolem  23694  qtopf1  23709  opnfbas  23735  isfil2  23749  fbasweak  23758  fsubbas  23760  filconn  23776  fbasrn  23777  rnelfmlem  23845  flimss2  23865  flimss1  23866  hausflim  23874  flimclslem  23877  flimsncls  23879  cnpflfi  23892  flfcnp2  23900  fclsfnflim  23920  cnextfvval  23958  cnextfres1  23961  symgtgp  23999  opnsubg  24001  ghmcnp  24008  qustgpopn  24013  qustgplem  24014  qustgphaus  24016  tsmsfbas  24021  ustfilxp  24106  utoptop  24128  utopbas  24129  restutopopn  24132  iducn  24176  cstucnd  24177  ucncn  24178  fmucnd  24185  cfilufg  24186  trcfilu  24187  cfiluweak  24188  neipcfilu  24189  psmetres2  24208  isxmetd  24220  xmetpsmet  24242  imasf1oxmet  24269  xblss2ps  24295  xblss2  24296  xblcntrps  24304  xblcntr  24305  blcld  24399  metustfbas  24451  cfilucfil  24453  restmetu  24464  ngptgp  24530  tngngpd  24547  nrmtngnrm  24552  tngnrg  24568  nlmvscn  24581  nrginvrcn  24586  nmo0  24629  nmoeq0  24630  nmoid  24636  nghmcn  24639  0nmhm  24649  blcvx  24692  iccntr  24716  xrge0tsms  24729  xmetdcn2  24732  metdstri  24746  metdscn  24751  rescncf  24796  cncfco  24806  oprpiece1res2  24856  cnheibor  24860  cnllycmp  24861  bndth  24863  ishtpyd  24880  isphtpyd  24891  pcoval2  24922  nmhmcn  25026  ipcn  25152  lmnn  25169  cfilss  25176  iscfil3  25179  cfilfcls  25180  cmetcaulem  25194  iscmet3lem2  25198  cfilres  25202  lmcau  25219  flimcfil  25220  cncmet  25228  rlmbn  25267  minveclem3b  25334  pjthlem1  25343  pjth2  25346  ivthlem3  25360  ovolssnul  25394  ovolctb  25397  ovoliunnul  25414  ovolsca  25422  ovolicopnf  25431  voliunlem2  25458  volsup  25463  dyadmaxlem  25504  vitalilem5  25519  mbfres  25551  mbfss  25553  mbfmulc2re  25555  mbfadd  25568  mbfmulc2  25570  mbflim  25575  i1faddlem  25600  i1fmullem  25601  mbfmul  25633  itg2mulc  25654  itg2cnlem1  25668  ibl0  25694  iblposlem  25699  itgreval  25704  iblneg  25710  iblss  25712  iblss2  25713  itgle  25717  iblconst  25725  iblabs  25736  iblabsr  25737  iblmulc2  25738  bddmulibl  25746  limciun  25801  limcun  25802  dvres2lem  25817  dvidlem  25822  dvcnp2  25827  dvcnp2OLD  25828  dvcn  25829  cpnres  25845  dvaddbr  25846  dvmulbr  25847  dvmulbrOLD  25848  dvcobr  25855  dvcobrOLD  25856  dvcjbr  25859  dvrec  25865  dvcnvlem  25886  dvferm  25898  dvlip2  25906  dveq0  25911  dv11cn  25912  dvivthlem1  25919  lhop1  25925  lhop2  25926  lhop  25927  dvcnvre  25930  dvfsumlem3  25941  dvfsumlem4  25942  dvfsumrlim  25944  dvfsum2  25947  ftc1a  25950  ftc1lem4  25952  ftc1lem6  25954  ftc1  25955  coe1mul3  26010  deg1addle2  26013  deg1sublt  26021  fta1blem  26082  drnguc1p  26085  ig1prsp  26092  plyco0  26103  plyeq0lem  26121  dgrub  26145  dgreq  26155  dgradd2  26180  dgrmul  26182  dgrcolem2  26186  dgrco  26187  plycpn  26203  plydivlem4  26210  plydiveu  26212  vieta1lem2  26225  vieta1  26226  aalioulem2  26247  aalioulem3  26248  aaliou3lem7  26263  tayl0  26275  ulmcn  26314  ulmdvlem3  26317  psercn  26342  abelth  26357  pilem3  26369  efif1olem1  26457  abslogimle  26488  argregt0  26525  argrege0  26526  logf1o2  26565  cxpsqrtlem  26617  cxpcn3  26664  abscxpbnd  26669  logreclem  26678  ang180lem2  26726  ang180lem3  26727  xrlimcnp  26884  harmonicbnd4  26927  fsumharmonic  26928  lgamgulmlem5  26949  lgambdd  26953  basellem4  27000  dvdsppwf1o  27102  dvdsflf1o  27103  fsumfldivdiaglem  27105  chpeq0  27125  chteq0  27126  chtub  27129  chpub  27137  dchrelbasd  27156  dchrmulcl  27166  dchrinv  27178  bposlem1  27201  bposlem2  27202  lgsdirprm  27248  lgsqrlem2  27264  lgsqrlem3  27265  lgsdchr  27272  lgseisenlem1  27292  lgseisenlem2  27293  lgseisenlem3  27294  lgsquadlem1  27297  2sqlem8  27343  2sqblem  27348  2sqmod  27353  chebbnd1lem1  27386  dchrisumlem1  27406  dchrisumlem2  27407  dchrisumlem3  27408  dchrisum0fno1  27428  pntrmax  27481  pntpbnd1a  27502  pntibndlem3  27509  pntlemn  27517  pntlemi  27521  pntlem3  27526  pntleml  27528  ostth1  27550  ostth2  27554  ostth3  27555  nosepon  27583  nolesgn2ores  27590  nogesgn1ores  27592  nosupres  27625  nosupbnd1lem2  27627  nosupbnd2lem1  27633  noinfres  27640  noinfbnd1lem2  27642  noinfbnd2lem1  27648  cofcutrtime  27841  divmuldivsd  28140  divdivs1d  28141  nnsgt0  28237  ercgrg  28450  motco  28473  cnvmot  28474  legso  28532  mirmot  28608  colopp  28702  hphl  28704  lmicom  28721  lmimid  28727  lmimot  28731  hypcgrlem1  28732  hypcgrlem2  28733  trgcopyeulem  28738  inagswap  28774  inaghl  28778  cgrg3col4  28786  brbtwn2  28838  axlowdimlem3  28877  axlowdimlem16  28890  axcontlem8  28904  fusgrfis  29263  nbgr2vtx1edg  29283  0vtxrgr  29510  0vtxrusgr  29511  ewlkle  29539  wlk1ewlk  29574  uspgr2wlkeq2  29581  wlkp1lem8  29614  trlontrl  29645  pthonpth  29684  pthdlem2  29704  wlklnwwlkln1  29804  wlknewwlksn  29823  wwlksnred  29828  wwlksnredwwlkn0  29832  2trlond  29875  2pthond  29878  elwwlks2ons3im  29890  clwlkclwwlklem2a1  29927  clwlkclwwlkf1  29945  clwwlkel  29981  clwwlkwwlksb  29989  wwlksext2clwwlk  29992  1ewlk  30050  0trlon  30059  0pthon  30062  1pthond  30079  3trlond  30108  3pthond  30110  3spthond  30112  eupthres  30150  2clwwlk2clwwlk  30285  numclwwlk1lem2foa  30289  numclwwlk1lem2f1  30292  nvabs  30607  vacn  30629  nmcvcn  30630  nmblore  30721  0lno  30725  0blo  30727  nmlno0lem  30728  occl  31239  pjhthlem1  31326  pjpjpre  31354  nmopre  31805  nmlnop0iALT  31930  nmophmi  31966  leoprf2  32062  stlesi  32176  disjdifprg  32510  disjun0  32530  fsuppcurry1  32654  fsuppcurry2  32655  fpwrelmap  32662  fzspl  32718  dfmgc2lem  32927  pwrssmgc  32932  xrge0tsmsd  33008  ogrpaddlt  33037  ogrpsublt  33041  psgnfzto1stlem  33063  fzto1st1  33065  evpmid  33111  pnfinf  33143  rmfsupp2  33195  fracfld  33264  ornglmullt  33291  orngrmullt  33292  orngmullt  33293  ofldlt1  33297  isarchiofld  33301  dvdsruassoi  33361  nsgmgc  33389  drngidl  33410  qsdrngi  33472  deg1addlt  33571  ply1degltdimlem  33624  lbsdiflsp0  33628  fedgmul  33633  fldexttr  33660  fldextid  33661  irngnzply1lem  33691  minplyelirng  33711  irredminply  33712  algextdeglem8  33720  rtelextdg2lem  33722  constrsslem  33737  constrllcllem  33748  constrlccllem  33749  constrcccllem  33750  qtopt1  33831  reff  33835  locfinreflem  33836  metideq  33889  metider  33890  pstmxmet  33893  qqhval2lem  33977  qqhcn  33987  qqhucn  33988  pwsiga  34126  prsiga  34127  measle0  34204  mbfmcst  34256  1stmbfm  34257  2ndmbfm  34258  imambfm  34259  cnmbfm  34260  mbfmco  34261  mbfmco2  34262  0elcarsg  34304  carsgclctun  34318  sibfof  34337  oddpwdc  34351  eulerpartlemmf  34372  eulerpartlemgs2  34377  0rrv  34448  ballotlemfc0  34490  ballotlemfcc  34491  signstfveq0  34574  breprexplemc  34629  bnj1452  35048  usgrgt2cycl  35117  acycgr1v  35136  derangen  35159  subfacval3  35176  cvmseu  35263  cvmliftmolem2  35269  cvmliftlem7  35278  cvmliftlem15  35285  cvmlift2lem9a  35290  cvmlift2lem9  35298  cvmlift2lem10  35299  cvmlift2lem11  35300  cvmlift2lem12  35301  cvmlift3lem6  35311  cvmlift3lem8  35313  ex-sategoelel  35408  ex-sategoelelomsuc  35413  mclsppslem  35570  mclspps  35571  wsuclem  35808  fness  36332  fnetr  36334  fnessref  36340  refssfne  36341  neibastop1  36342  neibastop2  36344  tailfb  36360  filnetlem3  36363  weiunfrlem  36447  bj-finsumval0  37268  bj-rvecvec  37282  dfgcd3  37307  lindsadd  37602  poimirlem13  37622  poimirlem15  37624  poimirlem24  37633  poimirlem28  37637  mblfinlem2  37647  ovoliunnfl  37651  volsupnfl  37654  mbfresfi  37655  iblabsnc  37673  iblmulc2nc  37674  ftc1cnnclem  37680  ftc1cnnc  37681  ftc1anc  37690  sdclem2  37731  metf1o  37744  ismtyhmeolem  37793  ismtyres  37797  heibor1lem  37798  bfplem2  37812  bfp  37813  rrncmslem  37821  iccbnd  37829  icccmpALT  37830  rngogrphom  37960  rngoisoco  37971  keridl  38021  lsmcv2  39017  lsatcv0  39019  lcvexchlem4  39025  lcvexchlem5  39026  l1cvpat  39042  lfl0f  39057  lfladdcl  39059  lflnegcl  39063  lkrlss  39083  eqlkr  39087  lkrlsp  39090  lkrlsp2  39091  lshpkrcl  39104  lkrin  39152  1cvrjat  39464  llni  39497  llnle  39507  lplni  39521  lplnle  39529  llncvrlpln2  39546  2atmat  39550  lvoli  39564  lplncvrlvol2  39604  elpaddri  39791  paddclN  39831  pclclN  39880  pclfinN  39889  0psubclN  39932  1psubclN  39933  atpsubclN  39934  pmapsubclN  39935  osumclN  39956  pexmidN  39958  pexmidlem6N  39964  lhp2lt  39990  lautcnv  40079  idlaut  40085  lautco  40086  idldil  40103  ldilcnv  40104  ldilco  40105  ltrncnv  40135  idltrn  40139  cdleme16d  40270  cdleme50laut  40536  cdleme50ldil  40537  cdleme50ltrn  40546  ltrnco  40708  dian0  41028  dia0eldmN  41029  dia1eldmN  41030  dialss  41035  diaintclN  41047  docaclN  41113  doca2N  41115  djajN  41126  dibintclN  41156  diblss  41159  dicvaddcl  41179  dicvscacl  41180  dicn0  41181  cdlemn11a  41196  dihord2cN  41210  dihord11b  41211  dihord6apre  41245  dihmeetlem1N  41279  dihglblem5apreN  41280  dihpN  41325  dihjatcclem4  41410  dochkr1  41467  islpoldN  41473  lcfrlem31  41562  mapdpglem18  41678  mapdheq2  41718  mapdheq4  41721  mapdh6aN  41724  hdmap1l6a  41798  hdmap14lem4a  41860  lcmineqlem4  42015  frlmfzoccat  42486  drnginvmuld  42508  psrbagres  42527  evlselvlem  42567  evlselv  42568  fsuppind  42571  fsuppssind  42574  prjspvs  42591  irrapxlem4  42806  pell1234qrdich  42842  pell1qr1  42852  pell14qrgap  42856  pellqrexplicit  42858  rmspecfund  42890  fzmaxdif  42963  acongeq  42965  jm2.23  42978  jm3.1  43002  lmhmlnmsplit  43069  hbt  43112  dgrsub2  43117  proot1ex  43178  cantnfub  43303  cantnfresb  43306  cantnf2  43307  tfsconcatfv2  43322  tfsconcatrn  43324  tfsconcatb0  43326  naddcnff  43344  naddcnffo  43346  naddcnfid1  43349  naddcnfid2  43350  clublem  43592  dftrcl3  43702  mnugrud  44266  hashnzfz2  44303  dvconstbi  44316  ubelsupr  45007  restopn3  45138  wessf1ornlem  45172  lefldiveq  45283  iccintsng  45514  climsuse  45599  mullimc  45607  limcdm0  45609  limccog  45611  mullimcf  45614  constlimc  45615  idlimc  45617  limcperiod  45619  limsupre  45632  limcleqr  45635  neglimc  45638  addlimc  45639  0ellimcdiv  45640  xlimliminflimsup  45853  cncfshift  45865  cncfperiod  45870  cncfuni  45877  icccncfext  45878  cncfiooicclem1  45884  fperdvper  45910  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  mbfres2cn  45949  iblsplit  45957  stoweidlem7  45998  stoweidlem13  46004  stoweidlem26  46017  wallispilem3  46058  stirlinglem6  46070  stirlinglem10  46074  dirkercncf  46098  fourierdlem6  46104  fourierdlem11  46109  fourierdlem12  46110  fourierdlem15  46113  fourierdlem26  46124  fourierdlem42  46140  fourierdlem50  46147  fourierdlem51  46148  fourierdlem52  46149  fourierdlem54  46151  fourierdlem62  46159  fourierdlem79  46176  fourierdlem102  46199  fourierdlem114  46211  etransclem23  46248  3f1oss1  47066  zgeltp1eq  47300  setsnidel  47368  preimafvsnel  47370  iccpartres  47409  prpair  47492  fpprel2  47732  isubgrsubgr  47859  grimidvtxedg  47875  grimcnv  47878  isuspgrim  47886  upgrimpthslem2  47898  stgrnbgr0  47953  uhgrimgrlim  47976  gpg5nbgrvtx03starlem2  48050  gpg5nbgrvtx13starlem2  48053  isassintop  48188  rhmsubcALTV  48263  srhmsubcALTV  48303  fldhmsubcALTV  48311  rmfsupp  48351  scmfsupp  48353  mptcfsupp  48355  lcoel0  48407  lincsumcl  48410  lincscmcl  48411  lcoss  48415  lindsrng01  48447  lincreslvec3  48461  lindssnlvec  48465  zgtp1leeq  48500  lubsscl  48938  glbsscl  48939  idmon  48999  idepi  49000  iinfssc  49036  iinfsubc  49037  discsubc  49043  nelsubclem  49046  imassc  49132  imasubc3  49135  isnatd  49202  swapfiso  49264  fucoppc  49389  thinciso  49449  diagciso  49518  termolmd  49649