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  7031  fveqressseq  7051  fmptsng  7142  fmptsnd  7143  fnprb  7182  fntpb  7183  fpr3g  8264  frrlem4  8268  1ellim  8462  isfsuppd  9317  fdmfifsupp  9326  fczfsuppd  9337  fsuppmptif  9350  fsuppco2  9354  fsuppcor  9355  dffi3  9382  suppr  9423  infpr  9456  ordtypelem7  9477  cantnf0  9628  cantnfp1lem1  9631  cantnfp1lem2  9632  cantnfp1lem3  9633  cantnflem1a  9638  cantnflem1d  9641  cantnflem1  9642  cantnf  9646  rankpwi  9776  carduni  9934  fin23lem32  10297  fpwwe2lem5  10588  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  inttsk  10727  grutsk1  10774  add20  11690  supaddc  12150  supadd  12151  supmul  12155  suprzcl  12614  uzid  12808  uzwo3  12902  rpnnen1lem5  12940  xrletrid  13115  xrre  13129  xrre3  13131  xleadd1a  13213  xlemul1a  13248  elioc2  13370  elico2  13371  elicc2  13372  elfz1eq  13496  fzadd2  13520  fznatpl1  13539  elfz1uz  13555  nn0fz0  13586  fzctr  13601  fzo1fzo0n0  13676  fzoaddel  13678  elincfzoext  13684  flid  13770  flval3  13777  fladdz  13787  fldiv  13822  modid  13858  hashf1lem1  14420  pfxccatin12d  14710  repswpfx  14750  2cshw  14778  pfx2  14913  wwlktovf1  14923  sqeqd  15132  01sqrexlem7  15214  max0add  15276  abs2difabs  15301  rddif  15307  fzomaxdiflem  15309  rexico  15320  icodiamlt  15404  limsupgre  15447  rlim3  15464  icco1  15506  rlimclim  15512  rlimuni  15516  rlimresb  15531  isercolllem2  15632  isercolllem3  15633  isercoll  15634  caucvgrlem  15639  caurcvgr  15640  iseraltlem3  15650  fsum00  15764  o1fsum  15779  bitsfzolem  16404  bitsfzo  16405  bitsmod  16406  bitscmp  16408  gcd0id  16489  gcdneg  16492  bezoutlem4  16512  nn0seqcvgd  16540  lcmneg  16573  lcmfunsnlem2lem2  16609  qredeq  16627  prmind2  16655  eulerthlem2  16752  pcpremul  16814  pcidlem  16843  pcgcd1  16848  fldivp1  16868  pcfaclem  16869  4sqlem17  16932  vdwlem1  16952  vdwlem6  16957  vdwlem12  16963  vdwlem13  16964  0ram  16991  ram0  16993  ramub1lem1  16997  invco  17733  sectmon  17744  monsect  17745  invid  17749  ssctr  17787  ssceq  17788  0ssc  17799  0subcat  17800  catsubcat  17801  issubc3  17811  fullsubc  17812  funcinv  17835  fthmon  17891  fuccocl  17929  fucidcl  17930  invfuc  17939  2initoinv  17972  2termoinv  17979  elhomai  17995  setcmon  18049  setcepi  18050  catcisolem  18072  curf2cl  18192  yonedalem4c  18238  yonedalem3  18241  yoniso  18246  lublecl  18320  isacs3lem  18501  tsrdir  18563  rabsubmgmd  18631  submgmid  18633  subsubmgm  18637  mgmhmima  18642  mgmhmeql  18643  mndpfsupp  18694  mnd1  18706  sgrp2nmndlem4  18855  sgrp2nmndlem5  18856  0subg  19083  nmznsg  19100  ghmpreima  19170  ghmeql  19171  ghmnsgpreima  19173  kerf1ghm  19179  cntzsgrpcl  19266  cntzsubm  19270  cntzsubg  19271  cntzmhm  19273  symgextfo  19352  symgfixf1  19367  symgfixfolem1  19368  odlem2  19469  finodsubmsubg  19497  gexlem2  19512  gexcl2  19519  sylow1lem5  19532  subgslw  19546  slwhash  19554  fislw  19555  sylow3lem1  19557  lsmsubg  19584  efgredlemd  19674  efgredlem  19677  efgcpbllemb  19685  frgpuplem  19702  cyggeninv  19813  iscygd  19817  iscygodd  19818  gsumzadd  19852  gsumconst  19864  gsumpt  19892  gsum2dlem2  19901  gsum2d  19902  gsum2d2lem  19903  dprdfcntz  19947  eldprdi  19950  subgdmdprd  19966  subgdprd  19967  dprdpr  19982  ablfac1c  20003  ablfac1eu  20005  ablfaclem3  20019  ring1  20219  subrngint  20469  rhmimasubrng  20475  cntzsubrng  20476  rhmeql  20512  rhmima  20513  cntzsubr  20515  rnghmsscmap2  20538  rnghmsscmap  20539  rnghmsubcsetc  20542  zrzeroorngc  20553  rhmsscmap2  20567  rhmsscmap  20568  rhmsubcsetc  20571  rhmsscrnghm  20574  rhmsubcrngc  20577  srhmsubc  20589  rhmsubc  20598  issubdrg  20689  fldhmsubc  20694  imadrhmcl  20706  isabvd  20721  abvdiv  20738  lsslsp  20921  lsslspOLD  20922  lmhmima  20954  lmhmpreima  20955  lmhmeql  20962  lsmcl  20990  lspfixed  21038  rnglidlrng  21157  rngqiprngim  21214  rng2idl1cntr  21215  qsssubdrg  21343  gzrngunit  21350  pzriprnglem8  21398  evpmodpmf1o  21505  ocvpj  21626  dsmm0cl  21649  dsmmacl  21650  dsmmsubg  21652  dsmmlss  21653  frlmsplit2  21682  uvcff  21700  lindfrn  21730  f1lindf  21731  lindsss  21733  issubassa  21776  issubassa2  21801  snifpsrbag  21829  psrbaglesupp  21831  psrbaglecl  21832  psrbagaddcl  21833  psrbagcon  21834  mplsubglem  21908  mpllsslem  21909  mplassa  21931  subrgmpl  21939  mplcoe5  21947  mplbas2  21949  mplind  21977  mpfind  22014  ismhp2  22028  mhpmulcl  22036  mhplss  22042  ply1assa  22084  coe1tmmul2  22162  coe1tmmul  22163  cply1coe0bi  22189  dmatid  22382  dmatsubcl  22385  dmatscmcl  22390  scmatid  22401  scmataddcl  22403  scmatsubcl  22404  scmatmulcl  22405  smatvscl  22411  scmatrhmcl  22415  mat0scmat  22425  mat1scmat  22426  mdet0pr  22479  chmaidscmat  22735  distop  22882  indistopon  22888  ppttop  22894  epttop  22896  mretopd  22979  toponmre  22980  neiss  22996  opnneissb  23001  ssnei2  23003  innei  23012  neiptoptop  23018  ordtcld1  23084  ordtcld2  23085  lmconst  23148  cnpnei  23151  iscncl  23156  cnss1  23163  cnss2  23164  cncnpi  23165  cncnp  23167  cnconst2  23170  cnrest  23172  cnpresti  23175  cnpdis  23180  paste  23181  lmcnp  23191  cnhaus  23241  hauscmp  23294  2ndcomap  23345  1stcelcls  23348  1stccnp  23349  llyrest  23372  nllyrest  23373  llyidm  23375  nllyidm  23376  ssref  23399  reftr  23401  refun0  23402  dissnref  23415  kgentopon  23425  kgenidm  23434  kgencn3  23445  txcld  23490  neitx  23494  tx1cn  23496  tx2cn  23497  ptcld  23500  xkoccn  23506  txcnp  23507  ptcnp  23509  txcnmpt  23511  ptcn  23514  txdis1cn  23522  ptrescn  23526  txkgen  23539  xkoco1cn  23544  xkoco2cn  23545  xkococn  23547  xkoinjcn  23574  qtoptop2  23586  qtopuni  23589  qtopid  23592  qtopkgen  23597  basqtop  23598  tgqtop  23599  qtopss  23602  qtopeu  23603  qtoprest  23604  kqopn  23621  kqcld  23622  kqreglem2  23629  reghmph  23680  ordthmeolem  23688  qtopf1  23703  opnfbas  23729  isfil2  23743  fbasweak  23752  fsubbas  23754  filconn  23770  fbasrn  23771  rnelfmlem  23839  flimss2  23859  flimss1  23860  hausflim  23868  flimclslem  23871  flimsncls  23873  cnpflfi  23886  flfcnp2  23894  fclsfnflim  23914  cnextfvval  23952  cnextfres1  23955  symgtgp  23993  opnsubg  23995  ghmcnp  24002  qustgpopn  24007  qustgplem  24008  qustgphaus  24010  tsmsfbas  24015  ustfilxp  24100  utoptop  24122  utopbas  24123  restutopopn  24126  iducn  24170  cstucnd  24171  ucncn  24172  fmucnd  24179  cfilufg  24180  trcfilu  24181  cfiluweak  24182  neipcfilu  24183  psmetres2  24202  isxmetd  24214  xmetpsmet  24236  imasf1oxmet  24263  xblss2ps  24289  xblss2  24290  xblcntrps  24298  xblcntr  24299  blcld  24393  metustfbas  24445  cfilucfil  24447  restmetu  24458  ngptgp  24524  tngngpd  24541  nrmtngnrm  24546  tngnrg  24562  nlmvscn  24575  nrginvrcn  24580  nmo0  24623  nmoeq0  24624  nmoid  24630  nghmcn  24633  0nmhm  24643  blcvx  24686  iccntr  24710  xrge0tsms  24723  xmetdcn2  24726  metdstri  24740  metdscn  24745  rescncf  24790  cncfco  24800  oprpiece1res2  24850  cnheibor  24854  cnllycmp  24855  bndth  24857  ishtpyd  24874  isphtpyd  24885  pcoval2  24916  nmhmcn  25020  ipcn  25146  lmnn  25163  cfilss  25170  iscfil3  25173  cfilfcls  25174  cmetcaulem  25188  iscmet3lem2  25192  cfilres  25196  lmcau  25213  flimcfil  25214  cncmet  25222  rlmbn  25261  minveclem3b  25328  pjthlem1  25337  pjth2  25340  ivthlem3  25354  ovolssnul  25388  ovolctb  25391  ovoliunnul  25408  ovolsca  25416  ovolicopnf  25425  voliunlem2  25452  volsup  25457  dyadmaxlem  25498  vitalilem5  25513  mbfres  25545  mbfss  25547  mbfmulc2re  25549  mbfadd  25562  mbfmulc2  25564  mbflim  25569  i1faddlem  25594  i1fmullem  25595  mbfmul  25627  itg2mulc  25648  itg2cnlem1  25662  ibl0  25688  iblposlem  25693  itgreval  25698  iblneg  25704  iblss  25706  iblss2  25707  itgle  25711  iblconst  25719  iblabs  25730  iblabsr  25731  iblmulc2  25732  bddmulibl  25740  limciun  25795  limcun  25796  dvres2lem  25811  dvidlem  25816  dvcnp2  25821  dvcnp2OLD  25822  dvcn  25823  cpnres  25839  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcobr  25849  dvcobrOLD  25850  dvcjbr  25853  dvrec  25859  dvcnvlem  25880  dvferm  25892  dvlip2  25900  dveq0  25905  dv11cn  25906  dvivthlem1  25913  lhop1  25919  lhop2  25920  lhop  25921  dvcnvre  25924  dvfsumlem3  25935  dvfsumlem4  25936  dvfsumrlim  25938  dvfsum2  25941  ftc1a  25944  ftc1lem4  25946  ftc1lem6  25948  ftc1  25949  coe1mul3  26004  deg1addle2  26007  deg1sublt  26015  fta1blem  26076  drnguc1p  26079  ig1prsp  26086  plyco0  26097  plyeq0lem  26115  dgrub  26139  dgreq  26149  dgradd2  26174  dgrmul  26176  dgrcolem2  26180  dgrco  26181  plycpn  26197  plydivlem4  26204  plydiveu  26206  vieta1lem2  26219  vieta1  26220  aalioulem2  26241  aalioulem3  26242  aaliou3lem7  26257  tayl0  26269  ulmcn  26308  ulmdvlem3  26311  psercn  26336  abelth  26351  pilem3  26363  efif1olem1  26451  abslogimle  26482  argregt0  26519  argrege0  26520  logf1o2  26559  cxpsqrtlem  26611  cxpcn3  26658  abscxpbnd  26663  logreclem  26672  ang180lem2  26720  ang180lem3  26721  xrlimcnp  26878  harmonicbnd4  26921  fsumharmonic  26922  lgamgulmlem5  26943  lgambdd  26947  basellem4  26994  dvdsppwf1o  27096  dvdsflf1o  27097  fsumfldivdiaglem  27099  chpeq0  27119  chteq0  27120  chtub  27123  chpub  27131  dchrelbasd  27150  dchrmulcl  27160  dchrinv  27172  bposlem1  27195  bposlem2  27196  lgsdirprm  27242  lgsqrlem2  27258  lgsqrlem3  27259  lgsdchr  27266  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgsquadlem1  27291  2sqlem8  27337  2sqblem  27342  2sqmod  27347  chebbnd1lem1  27380  dchrisumlem1  27400  dchrisumlem2  27401  dchrisumlem3  27402  dchrisum0fno1  27422  pntrmax  27475  pntpbnd1a  27496  pntibndlem3  27503  pntlemn  27511  pntlemi  27515  pntlem3  27520  pntleml  27522  ostth1  27544  ostth2  27548  ostth3  27549  nosepon  27577  nolesgn2ores  27584  nogesgn1ores  27586  nosupres  27619  nosupbnd1lem2  27621  nosupbnd2lem1  27627  noinfres  27634  noinfbnd1lem2  27636  noinfbnd2lem1  27642  cofcutrtime  27835  divmuldivsd  28134  divdivs1d  28135  nnsgt0  28231  ercgrg  28444  motco  28467  cnvmot  28468  legso  28526  mirmot  28602  colopp  28696  hphl  28698  lmicom  28715  lmimid  28721  lmimot  28725  hypcgrlem1  28726  hypcgrlem2  28727  trgcopyeulem  28732  inagswap  28768  inaghl  28772  cgrg3col4  28780  brbtwn2  28832  axlowdimlem3  28871  axlowdimlem16  28884  axcontlem8  28898  fusgrfis  29257  nbgr2vtx1edg  29277  0vtxrgr  29504  0vtxrusgr  29505  ewlkle  29533  wlk1ewlk  29568  uspgr2wlkeq2  29575  wlkp1lem8  29608  trlontrl  29639  pthonpth  29678  pthdlem2  29698  wlklnwwlkln1  29798  wlknewwlksn  29817  wwlksnred  29822  wwlksnredwwlkn0  29826  2trlond  29869  2pthond  29872  elwwlks2ons3im  29884  clwlkclwwlklem2a1  29921  clwlkclwwlkf1  29939  clwwlkel  29975  clwwlkwwlksb  29983  wwlksext2clwwlk  29986  1ewlk  30044  0trlon  30053  0pthon  30056  1pthond  30073  3trlond  30102  3pthond  30104  3spthond  30106  eupthres  30144  2clwwlk2clwwlk  30279  numclwwlk1lem2foa  30283  numclwwlk1lem2f1  30286  nvabs  30601  vacn  30623  nmcvcn  30624  nmblore  30715  0lno  30719  0blo  30721  nmlno0lem  30722  occl  31233  pjhthlem1  31320  pjpjpre  31348  nmopre  31799  nmlnop0iALT  31924  nmophmi  31960  leoprf2  32056  stlesi  32170  disjdifprg  32504  disjun0  32524  fsuppcurry1  32648  fsuppcurry2  32649  fpwrelmap  32656  fzspl  32712  dfmgc2lem  32921  pwrssmgc  32926  xrge0tsmsd  33002  ogrpaddlt  33031  ogrpsublt  33035  psgnfzto1stlem  33057  fzto1st1  33059  evpmid  33105  pnfinf  33137  rmfsupp2  33189  fracfld  33258  ornglmullt  33285  orngrmullt  33286  orngmullt  33287  ofldlt1  33291  isarchiofld  33295  dvdsruassoi  33355  nsgmgc  33383  drngidl  33404  qsdrngi  33466  deg1addlt  33565  ply1degltdimlem  33618  lbsdiflsp0  33622  fedgmul  33627  fldexttr  33654  fldextid  33655  irngnzply1lem  33685  minplyelirng  33705  irredminply  33706  algextdeglem8  33714  rtelextdg2lem  33716  constrsslem  33731  constrllcllem  33742  constrlccllem  33743  constrcccllem  33744  qtopt1  33825  reff  33829  locfinreflem  33830  metideq  33883  metider  33884  pstmxmet  33887  qqhval2lem  33971  qqhcn  33981  qqhucn  33982  pwsiga  34120  prsiga  34121  measle0  34198  mbfmcst  34250  1stmbfm  34251  2ndmbfm  34252  imambfm  34253  cnmbfm  34254  mbfmco  34255  mbfmco2  34256  0elcarsg  34298  carsgclctun  34312  sibfof  34331  oddpwdc  34345  eulerpartlemmf  34366  eulerpartlemgs2  34371  0rrv  34442  ballotlemfc0  34484  ballotlemfcc  34485  signstfveq0  34568  breprexplemc  34623  bnj1452  35042  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  35813  fness  36337  fnetr  36339  fnessref  36345  refssfne  36346  neibastop1  36347  neibastop2  36349  tailfb  36365  filnetlem3  36368  weiunfrlem  36452  bj-finsumval0  37273  bj-rvecvec  37287  dfgcd3  37312  lindsadd  37607  poimirlem13  37627  poimirlem15  37629  poimirlem24  37638  poimirlem28  37642  mblfinlem2  37652  ovoliunnfl  37656  volsupnfl  37659  mbfresfi  37660  iblabsnc  37678  iblmulc2nc  37679  ftc1cnnclem  37685  ftc1cnnc  37686  ftc1anc  37695  sdclem2  37736  metf1o  37749  ismtyhmeolem  37798  ismtyres  37802  heibor1lem  37803  bfplem2  37817  bfp  37818  rrncmslem  37826  iccbnd  37834  icccmpALT  37835  rngogrphom  37965  rngoisoco  37976  keridl  38026  lsmcv2  39022  lsatcv0  39024  lcvexchlem4  39030  lcvexchlem5  39031  l1cvpat  39047  lfl0f  39062  lfladdcl  39064  lflnegcl  39068  lkrlss  39088  eqlkr  39092  lkrlsp  39095  lkrlsp2  39096  lshpkrcl  39109  lkrin  39157  1cvrjat  39469  llni  39502  llnle  39512  lplni  39526  lplnle  39534  llncvrlpln2  39551  2atmat  39555  lvoli  39569  lplncvrlvol2  39609  elpaddri  39796  paddclN  39836  pclclN  39885  pclfinN  39894  0psubclN  39937  1psubclN  39938  atpsubclN  39939  pmapsubclN  39940  osumclN  39961  pexmidN  39963  pexmidlem6N  39969  lhp2lt  39995  lautcnv  40084  idlaut  40090  lautco  40091  idldil  40108  ldilcnv  40109  ldilco  40110  ltrncnv  40140  idltrn  40144  cdleme16d  40275  cdleme50laut  40541  cdleme50ldil  40542  cdleme50ltrn  40551  ltrnco  40713  dian0  41033  dia0eldmN  41034  dia1eldmN  41035  dialss  41040  diaintclN  41052  docaclN  41118  doca2N  41120  djajN  41131  dibintclN  41161  diblss  41164  dicvaddcl  41184  dicvscacl  41185  dicn0  41186  cdlemn11a  41201  dihord2cN  41215  dihord11b  41216  dihord6apre  41250  dihmeetlem1N  41284  dihglblem5apreN  41285  dihpN  41330  dihjatcclem4  41415  dochkr1  41472  islpoldN  41478  lcfrlem31  41567  mapdpglem18  41683  mapdheq2  41723  mapdheq4  41726  mapdh6aN  41729  hdmap1l6a  41803  hdmap14lem4a  41865  lcmineqlem4  42020  frlmfzoccat  42493  drnginvmuld  42515  psrbagres  42534  evlselvlem  42574  evlselv  42575  fsuppind  42578  fsuppssind  42581  prjspvs  42598  irrapxlem4  42813  pell1234qrdich  42849  pell1qr1  42859  pell14qrgap  42863  pellqrexplicit  42865  rmspecfund  42897  fzmaxdif  42970  acongeq  42972  jm2.23  42985  jm3.1  43009  lmhmlnmsplit  43076  hbt  43119  dgrsub2  43124  proot1ex  43185  cantnfub  43310  cantnfresb  43313  cantnf2  43314  tfsconcatfv2  43329  tfsconcatrn  43331  tfsconcatb0  43333  naddcnff  43351  naddcnffo  43353  naddcnfid1  43356  naddcnfid2  43357  clublem  43599  dftrcl3  43709  mnugrud  44273  hashnzfz2  44310  dvconstbi  44323  ubelsupr  45014  restopn3  45145  wessf1ornlem  45179  lefldiveq  45290  iccintsng  45521  climsuse  45606  mullimc  45614  limcdm0  45616  limccog  45618  mullimcf  45621  constlimc  45622  idlimc  45624  limcperiod  45626  limsupre  45639  limcleqr  45642  neglimc  45645  addlimc  45646  0ellimcdiv  45647  xlimliminflimsup  45860  cncfshift  45872  cncfperiod  45877  cncfuni  45884  icccncfext  45885  cncfiooicclem1  45891  fperdvper  45917  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  mbfres2cn  45956  iblsplit  45964  stoweidlem7  46005  stoweidlem13  46011  stoweidlem26  46024  wallispilem3  46065  stirlinglem6  46077  stirlinglem10  46081  dirkercncf  46105  fourierdlem6  46111  fourierdlem11  46116  fourierdlem12  46117  fourierdlem15  46120  fourierdlem26  46131  fourierdlem42  46147  fourierdlem50  46154  fourierdlem51  46155  fourierdlem52  46156  fourierdlem54  46158  fourierdlem62  46166  fourierdlem79  46183  fourierdlem102  46206  fourierdlem114  46218  etransclem23  46255  3f1oss1  47076  zgeltp1eq  47310  setsnidel  47378  preimafvsnel  47380  iccpartres  47419  prpair  47502  fpprel2  47742  isubgrsubgr  47869  grimidvtxedg  47885  grimcnv  47888  isuspgrim  47896  upgrimpthslem2  47908  stgrnbgr0  47963  uhgrimgrlim  47986  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx13starlem2  48063  isassintop  48198  rhmsubcALTV  48273  srhmsubcALTV  48313  fldhmsubcALTV  48321  rmfsupp  48361  scmfsupp  48363  mptcfsupp  48365  lcoel0  48417  lincsumcl  48420  lincscmcl  48421  lcoss  48425  lindsrng01  48457  lincreslvec3  48471  lindssnlvec  48475  zgtp1leeq  48510  lubsscl  48948  glbsscl  48949  idmon  49009  idepi  49010  iinfssc  49046  iinfsubc  49047  discsubc  49053  nelsubclem  49056  imassc  49142  imasubc3  49145  isnatd  49212  swapfiso  49274  fucoppc  49399  thinciso  49459  diagciso  49528  termolmd  49659