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  7048  fveqressseq  7068  fmptsng  7159  fmptsnd  7160  fnprb  7199  fntpb  7200  fpr3g  8282  frrlem4  8286  1ellim  8508  isfsuppd  9376  fdmfifsupp  9385  fczfsuppd  9396  fsuppmptif  9409  fsuppco2  9413  fsuppcor  9414  dffi3  9441  suppr  9482  infpr  9515  ordtypelem7  9536  cantnf0  9687  cantnfp1lem1  9690  cantnfp1lem2  9691  cantnfp1lem3  9692  cantnflem1a  9697  cantnflem1d  9700  cantnflem1  9701  cantnf  9705  rankpwi  9835  carduni  9993  fin23lem32  10356  fpwwe2lem5  10647  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  inttsk  10786  grutsk1  10833  add20  11747  supaddc  12207  supadd  12208  supmul  12212  suprzcl  12671  uzid  12865  uzwo3  12957  rpnnen1lem5  12995  xrletrid  13169  xrre  13183  xrre3  13185  xleadd1a  13267  xlemul1a  13302  elioc2  13424  elico2  13425  elicc2  13426  elfz1eq  13550  fzadd2  13574  fznatpl1  13593  elfz1uz  13609  nn0fz0  13640  fzctr  13655  fzo1fzo0n0  13729  fzoaddel  13731  elincfzoext  13737  flid  13823  flval3  13830  fladdz  13840  fldiv  13875  modid  13911  hashf1lem1  14471  pfxccatin12d  14761  repswpfx  14801  2cshw  14829  pfx2  14964  wwlktovf1  14974  sqeqd  15183  01sqrexlem7  15265  max0add  15327  abs2difabs  15351  rddif  15357  fzomaxdiflem  15359  rexico  15370  icodiamlt  15452  limsupgre  15495  rlim3  15512  icco1  15554  rlimclim  15560  rlimuni  15564  rlimresb  15579  isercolllem2  15680  isercolllem3  15681  isercoll  15682  caucvgrlem  15687  caurcvgr  15688  iseraltlem3  15698  fsum00  15812  o1fsum  15827  bitsfzolem  16451  bitsfzo  16452  bitsmod  16453  bitscmp  16455  gcd0id  16536  gcdneg  16539  bezoutlem4  16559  nn0seqcvgd  16587  lcmneg  16620  lcmfunsnlem2lem2  16656  qredeq  16674  prmind2  16702  eulerthlem2  16799  pcpremul  16861  pcidlem  16890  pcgcd1  16895  fldivp1  16915  pcfaclem  16916  4sqlem17  16979  vdwlem1  16999  vdwlem6  17004  vdwlem12  17010  vdwlem13  17011  0ram  17038  ram0  17040  ramub1lem1  17044  invco  17782  sectmon  17793  monsect  17794  invid  17798  ssctr  17836  ssceq  17837  0ssc  17848  0subcat  17849  catsubcat  17850  issubc3  17860  fullsubc  17861  funcinv  17884  fthmon  17940  fuccocl  17978  fucidcl  17979  invfuc  17988  2initoinv  18021  2termoinv  18028  elhomai  18044  setcmon  18098  setcepi  18099  catcisolem  18121  curf2cl  18241  yonedalem4c  18287  yonedalem3  18290  yoniso  18295  lublecl  18369  isacs3lem  18550  tsrdir  18612  rabsubmgmd  18680  submgmid  18682  subsubmgm  18686  mgmhmima  18691  mgmhmeql  18692  mndpfsupp  18743  mnd1  18755  sgrp2nmndlem4  18904  sgrp2nmndlem5  18905  0subg  19132  nmznsg  19149  ghmpreima  19219  ghmeql  19220  ghmnsgpreima  19222  kerf1ghm  19228  cntzsgrpcl  19315  cntzsubm  19319  cntzsubg  19320  cntzmhm  19322  symgextfo  19401  symgfixf1  19416  symgfixfolem1  19417  odlem2  19518  finodsubmsubg  19546  gexlem2  19561  gexcl2  19568  sylow1lem5  19581  subgslw  19595  slwhash  19603  fislw  19604  sylow3lem1  19606  lsmsubg  19633  efgredlemd  19723  efgredlem  19726  efgcpbllemb  19734  frgpuplem  19751  cyggeninv  19862  iscygd  19866  iscygodd  19867  gsumzadd  19901  gsumconst  19913  gsumpt  19941  gsum2dlem2  19950  gsum2d  19951  gsum2d2lem  19952  dprdfcntz  19996  eldprdi  19999  subgdmdprd  20015  subgdprd  20016  dprdpr  20031  ablfac1c  20052  ablfac1eu  20054  ablfaclem3  20068  ring1  20268  subrngint  20518  rhmimasubrng  20524  cntzsubrng  20525  rhmeql  20561  rhmima  20562  cntzsubr  20564  rnghmsscmap2  20587  rnghmsscmap  20588  rnghmsubcsetc  20591  zrzeroorngc  20602  rhmsscmap2  20616  rhmsscmap  20617  rhmsubcsetc  20620  rhmsscrnghm  20623  rhmsubcrngc  20626  srhmsubc  20638  rhmsubc  20647  issubdrg  20738  fldhmsubc  20743  imadrhmcl  20755  isabvd  20770  abvdiv  20787  lsslsp  20970  lsslspOLD  20971  lmhmima  21003  lmhmpreima  21004  lmhmeql  21011  lsmcl  21039  lspfixed  21087  rnglidlrng  21206  rngqiprngim  21263  rng2idl1cntr  21264  qsssubdrg  21392  gzrngunit  21399  pzriprnglem8  21447  evpmodpmf1o  21554  ocvpj  21675  dsmm0cl  21698  dsmmacl  21699  dsmmsubg  21701  dsmmlss  21702  frlmsplit2  21731  uvcff  21749  lindfrn  21779  f1lindf  21780  lindsss  21782  issubassa  21825  issubassa2  21850  snifpsrbag  21878  psrbaglesupp  21880  psrbaglecl  21881  psrbagaddcl  21882  psrbagcon  21883  mplsubglem  21957  mpllsslem  21958  mplassa  21980  subrgmpl  21988  mplcoe5  21996  mplbas2  21998  mplind  22026  mpfind  22063  ismhp2  22077  mhpmulcl  22085  mhplss  22091  ply1assa  22133  coe1tmmul2  22211  coe1tmmul  22212  cply1coe0bi  22238  dmatid  22431  dmatsubcl  22434  dmatscmcl  22439  scmatid  22450  scmataddcl  22452  scmatsubcl  22453  scmatmulcl  22454  smatvscl  22460  scmatrhmcl  22464  mat0scmat  22474  mat1scmat  22475  mdet0pr  22528  chmaidscmat  22784  distop  22931  indistopon  22937  ppttop  22943  epttop  22945  mretopd  23028  toponmre  23029  neiss  23045  opnneissb  23050  ssnei2  23052  innei  23061  neiptoptop  23067  ordtcld1  23133  ordtcld2  23134  lmconst  23197  cnpnei  23200  iscncl  23205  cnss1  23212  cnss2  23213  cncnpi  23214  cncnp  23216  cnconst2  23219  cnrest  23221  cnpresti  23224  cnpdis  23229  paste  23230  lmcnp  23240  cnhaus  23290  hauscmp  23343  2ndcomap  23394  1stcelcls  23397  1stccnp  23398  llyrest  23421  nllyrest  23422  llyidm  23424  nllyidm  23425  ssref  23448  reftr  23450  refun0  23451  dissnref  23464  kgentopon  23474  kgenidm  23483  kgencn3  23494  txcld  23539  neitx  23543  tx1cn  23545  tx2cn  23546  ptcld  23549  xkoccn  23555  txcnp  23556  ptcnp  23558  txcnmpt  23560  ptcn  23563  txdis1cn  23571  ptrescn  23575  txkgen  23588  xkoco1cn  23593  xkoco2cn  23594  xkococn  23596  xkoinjcn  23623  qtoptop2  23635  qtopuni  23638  qtopid  23641  qtopkgen  23646  basqtop  23647  tgqtop  23648  qtopss  23651  qtopeu  23652  qtoprest  23653  kqopn  23670  kqcld  23671  kqreglem2  23678  reghmph  23729  ordthmeolem  23737  qtopf1  23752  opnfbas  23778  isfil2  23792  fbasweak  23801  fsubbas  23803  filconn  23819  fbasrn  23820  rnelfmlem  23888  flimss2  23908  flimss1  23909  hausflim  23917  flimclslem  23920  flimsncls  23922  cnpflfi  23935  flfcnp2  23943  fclsfnflim  23963  cnextfvval  24001  cnextfres1  24004  symgtgp  24042  opnsubg  24044  ghmcnp  24051  qustgpopn  24056  qustgplem  24057  qustgphaus  24059  tsmsfbas  24064  ustfilxp  24149  utoptop  24171  utopbas  24172  restutopopn  24175  iducn  24219  cstucnd  24220  ucncn  24221  fmucnd  24228  cfilufg  24229  trcfilu  24230  cfiluweak  24231  neipcfilu  24232  psmetres2  24251  isxmetd  24263  xmetpsmet  24285  imasf1oxmet  24312  xblss2ps  24338  xblss2  24339  xblcntrps  24347  xblcntr  24348  blcld  24442  metustfbas  24494  cfilucfil  24496  restmetu  24507  ngptgp  24573  tngngpd  24590  nrmtngnrm  24595  tngnrg  24611  nlmvscn  24624  nrginvrcn  24629  nmo0  24672  nmoeq0  24673  nmoid  24679  nghmcn  24682  0nmhm  24692  blcvx  24735  iccntr  24759  xrge0tsms  24772  xmetdcn2  24775  metdstri  24789  metdscn  24794  rescncf  24839  cncfco  24849  oprpiece1res2  24899  cnheibor  24903  cnllycmp  24904  bndth  24906  ishtpyd  24923  isphtpyd  24934  pcoval2  24965  nmhmcn  25069  ipcn  25196  lmnn  25213  cfilss  25220  iscfil3  25223  cfilfcls  25224  cmetcaulem  25238  iscmet3lem2  25242  cfilres  25246  lmcau  25263  flimcfil  25264  cncmet  25272  rlmbn  25311  minveclem3b  25378  pjthlem1  25387  pjth2  25390  ivthlem3  25404  ovolssnul  25438  ovolctb  25441  ovoliunnul  25458  ovolsca  25466  ovolicopnf  25475  voliunlem2  25502  volsup  25507  dyadmaxlem  25548  vitalilem5  25563  mbfres  25595  mbfss  25597  mbfmulc2re  25599  mbfadd  25612  mbfmulc2  25614  mbflim  25619  i1faddlem  25644  i1fmullem  25645  mbfmul  25677  itg2mulc  25698  itg2cnlem1  25712  ibl0  25738  iblposlem  25743  itgreval  25748  iblneg  25754  iblss  25756  iblss2  25757  itgle  25761  iblconst  25769  iblabs  25780  iblabsr  25781  iblmulc2  25782  bddmulibl  25790  limciun  25845  limcun  25846  dvres2lem  25861  dvidlem  25866  dvcnp2  25871  dvcnp2OLD  25872  dvcn  25873  cpnres  25889  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvcobr  25899  dvcobrOLD  25900  dvcjbr  25903  dvrec  25909  dvcnvlem  25930  dvferm  25942  dvlip2  25950  dveq0  25955  dv11cn  25956  dvivthlem1  25963  lhop1  25969  lhop2  25970  lhop  25971  dvcnvre  25974  dvfsumlem3  25985  dvfsumlem4  25986  dvfsumrlim  25988  dvfsum2  25991  ftc1a  25994  ftc1lem4  25996  ftc1lem6  25998  ftc1  25999  coe1mul3  26054  deg1addle2  26057  deg1sublt  26065  fta1blem  26126  drnguc1p  26129  ig1prsp  26136  plyco0  26147  plyeq0lem  26165  dgrub  26189  dgreq  26199  dgradd2  26224  dgrmul  26226  dgrcolem2  26230  dgrco  26231  plycpn  26247  plydivlem4  26254  plydiveu  26256  vieta1lem2  26269  vieta1  26270  aalioulem2  26291  aalioulem3  26292  aaliou3lem7  26307  tayl0  26319  ulmcn  26358  ulmdvlem3  26361  psercn  26386  abelth  26401  pilem3  26413  efif1olem1  26501  abslogimle  26532  argregt0  26569  argrege0  26570  logf1o2  26609  cxpsqrtlem  26661  cxpcn3  26708  abscxpbnd  26713  logreclem  26722  ang180lem2  26770  ang180lem3  26771  xrlimcnp  26928  harmonicbnd4  26971  fsumharmonic  26972  lgamgulmlem5  26993  lgambdd  26997  basellem4  27044  dvdsppwf1o  27146  dvdsflf1o  27147  fsumfldivdiaglem  27149  chpeq0  27169  chteq0  27170  chtub  27173  chpub  27181  dchrelbasd  27200  dchrmulcl  27210  dchrinv  27222  bposlem1  27245  bposlem2  27246  lgsdirprm  27292  lgsqrlem2  27308  lgsqrlem3  27309  lgsdchr  27316  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgsquadlem1  27341  2sqlem8  27387  2sqblem  27392  2sqmod  27397  chebbnd1lem1  27430  dchrisumlem1  27450  dchrisumlem2  27451  dchrisumlem3  27452  dchrisum0fno1  27472  pntrmax  27525  pntpbnd1a  27546  pntibndlem3  27553  pntlemn  27561  pntlemi  27565  pntlem3  27570  pntleml  27572  ostth1  27594  ostth2  27598  ostth3  27599  nosepon  27627  nolesgn2ores  27634  nogesgn1ores  27636  nosupres  27669  nosupbnd1lem2  27671  nosupbnd2lem1  27677  noinfres  27684  noinfbnd1lem2  27686  noinfbnd2lem1  27692  cofcutrtime  27878  divmuldivsd  28173  divdivs1d  28174  nnsgt0  28259  ercgrg  28442  motco  28465  cnvmot  28466  legso  28524  mirmot  28600  colopp  28694  hphl  28696  lmicom  28713  lmimid  28719  lmimot  28723  hypcgrlem1  28724  hypcgrlem2  28725  trgcopyeulem  28730  inagswap  28766  inaghl  28770  cgrg3col4  28778  brbtwn2  28830  axlowdimlem3  28869  axlowdimlem16  28882  axcontlem8  28896  fusgrfis  29255  nbgr2vtx1edg  29275  0vtxrgr  29502  0vtxrusgr  29503  ewlkle  29531  wlk1ewlk  29566  uspgr2wlkeq2  29573  wlkp1lem8  29606  trlontrl  29637  pthonpth  29676  pthdlem2  29696  wlklnwwlkln1  29796  wlknewwlksn  29815  wwlksnred  29820  wwlksnredwwlkn0  29824  2trlond  29867  2pthond  29870  elwwlks2ons3im  29882  clwlkclwwlklem2a1  29919  clwlkclwwlkf1  29937  clwwlkel  29973  clwwlkwwlksb  29981  wwlksext2clwwlk  29984  1ewlk  30042  0trlon  30051  0pthon  30054  1pthond  30071  3trlond  30100  3pthond  30102  3spthond  30104  eupthres  30142  2clwwlk2clwwlk  30277  numclwwlk1lem2foa  30281  numclwwlk1lem2f1  30284  nvabs  30599  vacn  30621  nmcvcn  30622  nmblore  30713  0lno  30717  0blo  30719  nmlno0lem  30720  occl  31231  pjhthlem1  31318  pjpjpre  31346  nmopre  31797  nmlnop0iALT  31922  nmophmi  31958  leoprf2  32054  stlesi  32168  disjdifprg  32502  disjun0  32522  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  33127  rmfsupp2  33179  fracfld  33248  ornglmullt  33275  orngrmullt  33276  orngmullt  33277  ofldlt1  33281  isarchiofld  33285  dvdsruassoi  33345  nsgmgc  33373  drngidl  33394  qsdrngi  33456  deg1addlt  33555  ply1degltdimlem  33608  lbsdiflsp0  33612  fedgmul  33617  fldexttr  33646  fldextid  33647  irngnzply1lem  33677  minplyelirng  33695  irredminply  33696  algextdeglem8  33704  rtelextdg2lem  33706  constrsslem  33721  constrllcllem  33732  constrlccllem  33733  constrcccllem  33734  qtopt1  33812  reff  33816  locfinreflem  33817  metideq  33870  metider  33871  pstmxmet  33874  qqhval2lem  33958  qqhcn  33968  qqhucn  33969  pwsiga  34107  prsiga  34108  measle0  34185  mbfmcst  34237  1stmbfm  34238  2ndmbfm  34239  imambfm  34240  cnmbfm  34241  mbfmco  34242  mbfmco2  34243  0elcarsg  34285  carsgclctun  34299  sibfof  34318  oddpwdc  34332  eulerpartlemmf  34353  eulerpartlemgs2  34358  0rrv  34429  ballotlemfc0  34471  ballotlemfcc  34472  signstfveq0  34555  breprexplemc  34610  bnj1452  35029  usgrgt2cycl  35098  acycgr1v  35117  derangen  35140  subfacval3  35157  cvmseu  35244  cvmliftmolem2  35250  cvmliftlem7  35259  cvmliftlem15  35266  cvmlift2lem9a  35271  cvmlift2lem9  35279  cvmlift2lem10  35280  cvmlift2lem11  35281  cvmlift2lem12  35282  cvmlift3lem6  35292  cvmlift3lem8  35294  ex-sategoelel  35389  ex-sategoelelomsuc  35394  mclsppslem  35551  mclspps  35552  wsuclem  35789  fness  36313  fnetr  36315  fnessref  36321  refssfne  36322  neibastop1  36323  neibastop2  36325  tailfb  36341  filnetlem3  36344  weiunfrlem  36428  bj-finsumval0  37249  bj-rvecvec  37263  dfgcd3  37288  lindsadd  37583  poimirlem13  37603  poimirlem15  37605  poimirlem24  37614  poimirlem28  37618  mblfinlem2  37628  ovoliunnfl  37632  volsupnfl  37635  mbfresfi  37636  iblabsnc  37654  iblmulc2nc  37655  ftc1cnnclem  37661  ftc1cnnc  37662  ftc1anc  37671  sdclem2  37712  metf1o  37725  ismtyhmeolem  37774  ismtyres  37778  heibor1lem  37779  bfplem2  37793  bfp  37794  rrncmslem  37802  iccbnd  37810  icccmpALT  37811  rngogrphom  37941  rngoisoco  37952  keridl  38002  lsmcv2  38993  lsatcv0  38995  lcvexchlem4  39001  lcvexchlem5  39002  l1cvpat  39018  lfl0f  39033  lfladdcl  39035  lflnegcl  39039  lkrlss  39059  eqlkr  39063  lkrlsp  39066  lkrlsp2  39067  lshpkrcl  39080  lkrin  39128  1cvrjat  39440  llni  39473  llnle  39483  lplni  39497  lplnle  39505  llncvrlpln2  39522  2atmat  39526  lvoli  39540  lplncvrlvol2  39580  elpaddri  39767  paddclN  39807  pclclN  39856  pclfinN  39865  0psubclN  39908  1psubclN  39909  atpsubclN  39910  pmapsubclN  39911  osumclN  39932  pexmidN  39934  pexmidlem6N  39940  lhp2lt  39966  lautcnv  40055  idlaut  40061  lautco  40062  idldil  40079  ldilcnv  40080  ldilco  40081  ltrncnv  40111  idltrn  40115  cdleme16d  40246  cdleme50laut  40512  cdleme50ldil  40513  cdleme50ltrn  40522  ltrnco  40684  dian0  41004  dia0eldmN  41005  dia1eldmN  41006  dialss  41011  diaintclN  41023  docaclN  41089  doca2N  41091  djajN  41102  dibintclN  41132  diblss  41135  dicvaddcl  41155  dicvscacl  41156  dicn0  41157  cdlemn11a  41172  dihord2cN  41186  dihord11b  41187  dihord6apre  41221  dihmeetlem1N  41255  dihglblem5apreN  41256  dihpN  41301  dihjatcclem4  41386  dochkr1  41443  islpoldN  41449  lcfrlem31  41538  mapdpglem18  41654  mapdheq2  41694  mapdheq4  41697  mapdh6aN  41700  hdmap1l6a  41774  hdmap14lem4a  41836  lcmineqlem4  41991  frlmfzoccat  42475  drnginvmuld  42497  psrbagres  42516  evlselvlem  42556  evlselv  42557  fsuppind  42560  fsuppssind  42563  prjspvs  42580  irrapxlem4  42795  pell1234qrdich  42831  pell1qr1  42841  pell14qrgap  42845  pellqrexplicit  42847  rmspecfund  42879  fzmaxdif  42952  acongeq  42954  jm2.23  42967  jm3.1  42991  lmhmlnmsplit  43058  hbt  43101  dgrsub2  43106  proot1ex  43167  cantnfub  43292  cantnfresb  43295  cantnf2  43296  tfsconcatfv2  43311  tfsconcatrn  43313  tfsconcatb0  43315  naddcnff  43333  naddcnffo  43335  naddcnfid1  43338  naddcnfid2  43339  clublem  43581  dftrcl3  43691  mnugrud  44256  hashnzfz2  44293  dvconstbi  44306  ubelsupr  44992  restopn3  45123  wessf1ornlem  45157  lefldiveq  45269  iccintsng  45500  climsuse  45585  mullimc  45593  limcdm0  45595  limccog  45597  mullimcf  45600  constlimc  45601  idlimc  45603  limcperiod  45605  limsupre  45618  limcleqr  45621  neglimc  45624  addlimc  45625  0ellimcdiv  45626  xlimliminflimsup  45839  cncfshift  45851  cncfperiod  45856  cncfuni  45863  icccncfext  45864  cncfiooicclem1  45870  fperdvper  45896  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  mbfres2cn  45935  iblsplit  45943  stoweidlem7  45984  stoweidlem13  45990  stoweidlem26  46003  wallispilem3  46044  stirlinglem6  46056  stirlinglem10  46060  dirkercncf  46084  fourierdlem6  46090  fourierdlem11  46095  fourierdlem12  46096  fourierdlem15  46099  fourierdlem26  46110  fourierdlem42  46126  fourierdlem50  46133  fourierdlem51  46134  fourierdlem52  46135  fourierdlem54  46137  fourierdlem62  46145  fourierdlem79  46162  fourierdlem102  46185  fourierdlem114  46197  etransclem23  46234  3f1oss1  47052  zgeltp1eq  47286  setsnidel  47339  preimafvsnel  47341  iccpartres  47380  prpair  47463  fpprel2  47703  isubgrsubgr  47830  grimidvtxedg  47846  grimcnv  47849  isuspgrim  47857  upgrimpthslem2  47869  stgrnbgr0  47924  uhgrimgrlim  47947  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx13starlem2  48022  isassintop  48133  rhmsubcALTV  48208  srhmsubcALTV  48248  fldhmsubcALTV  48256  rmfsupp  48296  scmfsupp  48298  mptcfsupp  48300  lcoel0  48352  lincsumcl  48355  lincscmcl  48356  lcoss  48360  lindsrng01  48392  lincreslvec3  48406  lindssnlvec  48410  zgtp1leeq  48445  lubsscl  48882  glbsscl  48883  idmon  48943  idepi  48944  iinfssc  48972  iinfsubc  48973  discsubc  48979  nelsubclem  48982  imassc  49041  imasubc3  49044  isnatd  49091  swapfiso  49150  thinciso  49304  diagciso  49372