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  6992  fveqressseq  7012  fmptsng  7102  fmptsnd  7103  fnprb  7142  fntpb  7143  fpr3g  8215  frrlem4  8219  1ellim  8413  isfsuppd  9250  fdmfifsupp  9259  fczfsuppd  9270  fsuppmptif  9283  fsuppco2  9287  fsuppcor  9288  dffi3  9315  suppr  9356  infpr  9389  ordtypelem7  9410  cantnf0  9565  cantnfp1lem1  9568  cantnfp1lem2  9569  cantnfp1lem3  9570  cantnflem1a  9575  cantnflem1d  9578  cantnflem1  9579  cantnf  9583  rankpwi  9716  carduni  9874  fin23lem32  10235  fpwwe2lem5  10526  fpwwe2lem11  10532  fpwwe2lem12  10533  fpwwe2  10534  inttsk  10665  grutsk1  10712  add20  11629  supaddc  12089  supadd  12090  supmul  12094  suprzcl  12553  uzid  12747  uzwo3  12841  rpnnen1lem5  12879  xrletrid  13054  xrre  13068  xrre3  13070  xleadd1a  13152  xlemul1a  13187  elioc2  13309  elico2  13310  elicc2  13311  elfz1eq  13435  fzadd2  13459  fznatpl1  13478  elfz1uz  13494  nn0fz0  13525  fzctr  13540  fzo1fzo0n0  13615  fzoaddel  13617  elincfzoext  13623  flid  13712  flval3  13719  fladdz  13729  fldiv  13764  modid  13800  hashf1lem1  14362  pfxccatin12d  14652  repswpfx  14692  2cshw  14720  pfx2  14854  wwlktovf1  14864  sqeqd  15073  01sqrexlem7  15155  max0add  15217  abs2difabs  15242  rddif  15248  fzomaxdiflem  15250  rexico  15261  icodiamlt  15345  limsupgre  15388  rlim3  15405  icco1  15447  rlimclim  15453  rlimuni  15457  rlimresb  15472  isercolllem2  15573  isercolllem3  15574  isercoll  15575  caucvgrlem  15580  caurcvgr  15581  iseraltlem3  15591  fsum00  15705  o1fsum  15720  bitsfzolem  16345  bitsfzo  16346  bitsmod  16347  bitscmp  16349  gcd0id  16430  gcdneg  16433  bezoutlem4  16453  nn0seqcvgd  16481  lcmneg  16514  lcmfunsnlem2lem2  16550  qredeq  16568  prmind2  16596  eulerthlem2  16693  pcpremul  16755  pcidlem  16784  pcgcd1  16789  fldivp1  16809  pcfaclem  16810  4sqlem17  16873  vdwlem1  16893  vdwlem6  16898  vdwlem12  16904  vdwlem13  16905  0ram  16932  ram0  16934  ramub1lem1  16938  invco  17678  sectmon  17689  monsect  17690  invid  17694  ssctr  17732  ssceq  17733  0ssc  17744  0subcat  17745  catsubcat  17746  issubc3  17756  fullsubc  17757  funcinv  17780  fthmon  17836  fuccocl  17874  fucidcl  17875  invfuc  17884  2initoinv  17917  2termoinv  17924  elhomai  17940  setcmon  17994  setcepi  17995  catcisolem  18017  curf2cl  18137  yonedalem4c  18183  yonedalem3  18186  yoniso  18191  lublecl  18265  isacs3lem  18448  tsrdir  18510  chnccat  18532  rabsubmgmd  18612  submgmid  18614  subsubmgm  18618  mgmhmima  18623  mgmhmeql  18624  mndpfsupp  18675  mnd1  18687  sgrp2nmndlem4  18836  sgrp2nmndlem5  18837  0subg  19064  nmznsg  19080  ghmpreima  19150  ghmeql  19151  ghmnsgpreima  19153  kerf1ghm  19159  cntzsgrpcl  19246  cntzsubm  19250  cntzsubg  19251  cntzmhm  19253  symgextfo  19334  symgfixf1  19349  symgfixfolem1  19350  odlem2  19451  finodsubmsubg  19479  gexlem2  19494  gexcl2  19501  sylow1lem5  19514  subgslw  19528  slwhash  19536  fislw  19537  sylow3lem1  19539  lsmsubg  19566  efgredlemd  19656  efgredlem  19659  efgcpbllemb  19667  frgpuplem  19684  cyggeninv  19795  iscygd  19799  iscygodd  19800  gsumzadd  19834  gsumconst  19846  gsumpt  19874  gsum2dlem2  19883  gsum2d  19884  gsum2d2lem  19885  dprdfcntz  19929  eldprdi  19932  subgdmdprd  19948  subgdprd  19949  dprdpr  19964  ablfac1c  19985  ablfac1eu  19987  ablfaclem3  20001  ogrpaddlt  20050  ogrpsublt  20054  ring1  20228  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  ornglmullt  20784  orngrmullt  20785  orngmullt  20786  ofldlt1  20790  lsslsp  20948  lsslspOLD  20949  lmhmima  20981  lmhmpreima  20982  lmhmeql  20989  lsmcl  21017  lspfixed  21065  rnglidlrng  21184  rngqiprngim  21241  rng2idl1cntr  21242  qsssubdrg  21363  gzrngunit  21370  pzriprnglem8  21425  evpmodpmf1o  21533  ocvpj  21654  dsmm0cl  21677  dsmmacl  21678  dsmmsubg  21680  dsmmlss  21681  frlmsplit2  21710  uvcff  21728  lindfrn  21758  f1lindf  21759  lindsss  21761  issubassa  21804  issubassa2  21829  snifpsrbag  21857  psrbaglesupp  21859  psrbaglecl  21860  psrbagaddcl  21861  psrbagcon  21862  mplsubglem  21936  mpllsslem  21937  mplassa  21959  subrgmpl  21967  mplcoe5  21975  mplbas2  21977  mplind  22005  mpfind  22042  ismhp2  22056  mhpmulcl  22064  mhplss  22070  ply1assa  22112  coe1tmmul2  22190  coe1tmmul  22191  cply1coe0bi  22217  dmatid  22410  dmatsubcl  22413  dmatscmcl  22418  scmatid  22429  scmataddcl  22431  scmatsubcl  22432  scmatmulcl  22433  smatvscl  22439  scmatrhmcl  22443  mat0scmat  22453  mat1scmat  22454  mdet0pr  22507  chmaidscmat  22763  distop  22910  indistopon  22916  ppttop  22922  epttop  22924  mretopd  23007  toponmre  23008  neiss  23024  opnneissb  23029  ssnei2  23031  innei  23040  neiptoptop  23046  ordtcld1  23112  ordtcld2  23113  lmconst  23176  cnpnei  23179  iscncl  23184  cnss1  23191  cnss2  23192  cncnpi  23193  cncnp  23195  cnconst2  23198  cnrest  23200  cnpresti  23203  cnpdis  23208  paste  23209  lmcnp  23219  cnhaus  23269  hauscmp  23322  2ndcomap  23373  1stcelcls  23376  1stccnp  23377  llyrest  23400  nllyrest  23401  llyidm  23403  nllyidm  23404  ssref  23427  reftr  23429  refun0  23430  dissnref  23443  kgentopon  23453  kgenidm  23462  kgencn3  23473  txcld  23518  neitx  23522  tx1cn  23524  tx2cn  23525  ptcld  23528  xkoccn  23534  txcnp  23535  ptcnp  23537  txcnmpt  23539  ptcn  23542  txdis1cn  23550  ptrescn  23554  txkgen  23567  xkoco1cn  23572  xkoco2cn  23573  xkococn  23575  xkoinjcn  23602  qtoptop2  23614  qtopuni  23617  qtopid  23620  qtopkgen  23625  basqtop  23626  tgqtop  23627  qtopss  23630  qtopeu  23631  qtoprest  23632  kqopn  23649  kqcld  23650  kqreglem2  23657  reghmph  23708  ordthmeolem  23716  qtopf1  23731  opnfbas  23757  isfil2  23771  fbasweak  23780  fsubbas  23782  filconn  23798  fbasrn  23799  rnelfmlem  23867  flimss2  23887  flimss1  23888  hausflim  23896  flimclslem  23899  flimsncls  23901  cnpflfi  23914  flfcnp2  23922  fclsfnflim  23942  cnextfvval  23980  cnextfres1  23983  symgtgp  24021  opnsubg  24023  ghmcnp  24030  qustgpopn  24035  qustgplem  24036  qustgphaus  24038  tsmsfbas  24043  ustfilxp  24128  utoptop  24149  utopbas  24150  restutopopn  24153  iducn  24197  cstucnd  24198  ucncn  24199  fmucnd  24206  cfilufg  24207  trcfilu  24208  cfiluweak  24209  neipcfilu  24210  psmetres2  24229  isxmetd  24241  xmetpsmet  24263  imasf1oxmet  24290  xblss2ps  24316  xblss2  24317  xblcntrps  24325  xblcntr  24326  blcld  24420  metustfbas  24472  cfilucfil  24474  restmetu  24485  ngptgp  24551  tngngpd  24568  nrmtngnrm  24573  tngnrg  24589  nlmvscn  24602  nrginvrcn  24607  nmo0  24650  nmoeq0  24651  nmoid  24657  nghmcn  24660  0nmhm  24670  blcvx  24713  iccntr  24737  xrge0tsms  24750  xmetdcn2  24753  metdstri  24767  metdscn  24772  rescncf  24817  cncfco  24827  oprpiece1res2  24877  cnheibor  24881  cnllycmp  24882  bndth  24884  ishtpyd  24901  isphtpyd  24912  pcoval2  24943  nmhmcn  25047  ipcn  25173  lmnn  25190  cfilss  25197  iscfil3  25200  cfilfcls  25201  cmetcaulem  25215  iscmet3lem2  25219  cfilres  25223  lmcau  25240  flimcfil  25241  cncmet  25249  rlmbn  25288  minveclem3b  25355  pjthlem1  25364  pjth2  25367  ivthlem3  25381  ovolssnul  25415  ovolctb  25418  ovoliunnul  25435  ovolsca  25443  ovolicopnf  25452  voliunlem2  25479  volsup  25484  dyadmaxlem  25525  vitalilem5  25540  mbfres  25572  mbfss  25574  mbfmulc2re  25576  mbfadd  25589  mbfmulc2  25591  mbflim  25596  i1faddlem  25621  i1fmullem  25622  mbfmul  25654  itg2mulc  25675  itg2cnlem1  25689  ibl0  25715  iblposlem  25720  itgreval  25725  iblneg  25731  iblss  25733  iblss2  25734  itgle  25738  iblconst  25746  iblabs  25757  iblabsr  25758  iblmulc2  25759  bddmulibl  25767  limciun  25822  limcun  25823  dvres2lem  25838  dvidlem  25843  dvcnp2  25848  dvcnp2OLD  25849  dvcn  25850  cpnres  25866  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvcobr  25876  dvcobrOLD  25877  dvcjbr  25880  dvrec  25886  dvcnvlem  25907  dvferm  25919  dvlip2  25927  dveq0  25932  dv11cn  25933  dvivthlem1  25940  lhop1  25946  lhop2  25947  lhop  25948  dvcnvre  25951  dvfsumlem3  25962  dvfsumlem4  25963  dvfsumrlim  25965  dvfsum2  25968  ftc1a  25971  ftc1lem4  25973  ftc1lem6  25975  ftc1  25976  coe1mul3  26031  deg1addle2  26034  deg1sublt  26042  fta1blem  26103  drnguc1p  26106  ig1prsp  26113  plyco0  26124  plyeq0lem  26142  dgrub  26166  dgreq  26176  dgradd2  26201  dgrmul  26203  dgrcolem2  26207  dgrco  26208  plycpn  26224  plydivlem4  26231  plydiveu  26233  vieta1lem2  26246  vieta1  26247  aalioulem2  26268  aalioulem3  26269  aaliou3lem7  26284  tayl0  26296  ulmcn  26335  ulmdvlem3  26338  psercn  26363  abelth  26378  pilem3  26390  efif1olem1  26478  abslogimle  26509  argregt0  26546  argrege0  26547  logf1o2  26586  cxpsqrtlem  26638  cxpcn3  26685  abscxpbnd  26690  logreclem  26699  ang180lem2  26747  ang180lem3  26748  xrlimcnp  26905  harmonicbnd4  26948  fsumharmonic  26949  lgamgulmlem5  26970  lgambdd  26974  basellem4  27021  dvdsppwf1o  27123  dvdsflf1o  27124  fsumfldivdiaglem  27126  chpeq0  27146  chteq0  27147  chtub  27150  chpub  27158  dchrelbasd  27177  dchrmulcl  27187  dchrinv  27199  bposlem1  27222  bposlem2  27223  lgsdirprm  27269  lgsqrlem2  27285  lgsqrlem3  27286  lgsdchr  27293  lgseisenlem1  27313  lgseisenlem2  27314  lgseisenlem3  27315  lgsquadlem1  27318  2sqlem8  27364  2sqblem  27369  2sqmod  27374  chebbnd1lem1  27407  dchrisumlem1  27427  dchrisumlem2  27428  dchrisumlem3  27429  dchrisum0fno1  27449  pntrmax  27502  pntpbnd1a  27523  pntibndlem3  27530  pntlemn  27538  pntlemi  27542  pntlem3  27547  pntleml  27549  ostth1  27571  ostth2  27575  ostth3  27576  nosepon  27604  nolesgn2ores  27611  nogesgn1ores  27613  nosupres  27646  nosupbnd1lem2  27648  nosupbnd2lem1  27654  noinfres  27661  noinfbnd1lem2  27663  noinfbnd2lem1  27669  eqscut3  27765  cofcutrtime  27871  divmuldivsd  28170  divdivs1d  28171  nnsgt0  28267  ercgrg  28495  motco  28518  cnvmot  28519  legso  28577  mirmot  28653  colopp  28747  hphl  28749  lmicom  28766  lmimid  28772  lmimot  28776  hypcgrlem1  28777  hypcgrlem2  28778  trgcopyeulem  28783  inagswap  28819  inaghl  28823  cgrg3col4  28831  brbtwn2  28883  axlowdimlem3  28922  axlowdimlem16  28935  axcontlem8  28949  fusgrfis  29308  nbgr2vtx1edg  29328  0vtxrgr  29555  0vtxrusgr  29556  ewlkle  29584  wlk1ewlk  29618  uspgr2wlkeq2  29625  wlkp1lem8  29657  trlontrl  29687  pthonpth  29726  pthdlem2  29746  wlklnwwlkln1  29846  wlknewwlksn  29865  wwlksnred  29870  wwlksnredwwlkn0  29874  2trlond  29917  2pthond  29920  elwwlks2ons3im  29932  clwlkclwwlklem2a1  29972  clwlkclwwlkf1  29990  clwwlkel  30026  clwwlkwwlksb  30034  wwlksext2clwwlk  30037  1ewlk  30095  0trlon  30104  0pthon  30107  1pthond  30124  3trlond  30153  3pthond  30155  3spthond  30157  eupthres  30195  2clwwlk2clwwlk  30330  numclwwlk1lem2foa  30334  numclwwlk1lem2f1  30337  nvabs  30652  vacn  30674  nmcvcn  30675  nmblore  30766  0lno  30770  0blo  30772  nmlno0lem  30773  occl  31284  pjhthlem1  31371  pjpjpre  31399  nmopre  31850  nmlnop0iALT  31975  nmophmi  32011  leoprf2  32107  stlesi  32221  disjdifprg  32555  disjun0  32575  fsuppcurry1  32707  fsuppcurry2  32708  fpwrelmap  32716  fzspl  32772  dfmgc2lem  32976  pwrssmgc  32981  xrge0tsmsd  33042  psgnfzto1stlem  33069  fzto1st1  33071  evpmid  33117  pnfinf  33152  isarchiofld  33168  rmfsupp2  33205  fracfld  33274  dvdsruassoi  33349  nsgmgc  33377  drngidl  33398  qsdrngi  33460  deg1addlt  33560  ply1degltdimlem  33635  lbsdiflsp0  33639  fedgmul  33644  fldexttr  33671  fldextid  33672  irngnzply1lem  33703  finextalg  33711  minplyelirng  33728  irredminply  33729  algextdeglem8  33737  rtelextdg2lem  33739  constrsslem  33754  constrllcllem  33765  constrlccllem  33766  constrcccllem  33767  qtopt1  33848  reff  33852  locfinreflem  33853  metideq  33906  metider  33907  pstmxmet  33910  qqhval2lem  33994  qqhcn  34004  qqhucn  34005  pwsiga  34143  prsiga  34144  measle0  34221  mbfmcst  34272  1stmbfm  34273  2ndmbfm  34274  imambfm  34275  cnmbfm  34276  mbfmco  34277  mbfmco2  34278  0elcarsg  34320  carsgclctun  34334  sibfof  34353  oddpwdc  34367  eulerpartlemmf  34388  eulerpartlemgs2  34393  0rrv  34464  ballotlemfc0  34506  ballotlemfcc  34507  signstfveq0  34590  breprexplemc  34645  bnj1452  35064  usgrgt2cycl  35174  acycgr1v  35193  derangen  35216  subfacval3  35233  cvmseu  35320  cvmliftmolem2  35326  cvmliftlem7  35335  cvmliftlem15  35342  cvmlift2lem9a  35347  cvmlift2lem9  35355  cvmlift2lem10  35356  cvmlift2lem11  35357  cvmlift2lem12  35358  cvmlift3lem6  35368  cvmlift3lem8  35370  ex-sategoelel  35465  ex-sategoelelomsuc  35470  mclsppslem  35627  mclspps  35628  wsuclem  35867  fness  36393  fnetr  36395  fnessref  36401  refssfne  36402  neibastop1  36403  neibastop2  36405  tailfb  36421  filnetlem3  36424  weiunfrlem  36508  bj-finsumval0  37329  bj-rvecvec  37343  dfgcd3  37368  lindsadd  37652  poimirlem13  37672  poimirlem15  37674  poimirlem24  37683  poimirlem28  37687  mblfinlem2  37697  ovoliunnfl  37701  volsupnfl  37704  mbfresfi  37705  iblabsnc  37723  iblmulc2nc  37724  ftc1cnnclem  37730  ftc1cnnc  37731  ftc1anc  37740  sdclem2  37781  metf1o  37794  ismtyhmeolem  37843  ismtyres  37847  heibor1lem  37848  bfplem2  37862  bfp  37863  rrncmslem  37871  iccbnd  37879  icccmpALT  37880  rngogrphom  38010  rngoisoco  38021  keridl  38071  lsmcv2  39127  lsatcv0  39129  lcvexchlem4  39135  lcvexchlem5  39136  l1cvpat  39152  lfl0f  39167  lfladdcl  39169  lflnegcl  39173  lkrlss  39193  eqlkr  39197  lkrlsp  39200  lkrlsp2  39201  lshpkrcl  39214  lkrin  39262  1cvrjat  39573  llni  39606  llnle  39616  lplni  39630  lplnle  39638  llncvrlpln2  39655  2atmat  39659  lvoli  39673  lplncvrlvol2  39713  elpaddri  39900  paddclN  39940  pclclN  39989  pclfinN  39998  0psubclN  40041  1psubclN  40042  atpsubclN  40043  pmapsubclN  40044  osumclN  40065  pexmidN  40067  pexmidlem6N  40073  lhp2lt  40099  lautcnv  40188  idlaut  40194  lautco  40195  idldil  40212  ldilcnv  40213  ldilco  40214  ltrncnv  40244  idltrn  40248  cdleme16d  40379  cdleme50laut  40645  cdleme50ldil  40646  cdleme50ltrn  40655  ltrnco  40817  dian0  41137  dia0eldmN  41138  dia1eldmN  41139  dialss  41144  diaintclN  41156  docaclN  41222  doca2N  41224  djajN  41235  dibintclN  41265  diblss  41268  dicvaddcl  41288  dicvscacl  41289  dicn0  41290  cdlemn11a  41305  dihord2cN  41319  dihord11b  41320  dihord6apre  41354  dihmeetlem1N  41388  dihglblem5apreN  41389  dihpN  41434  dihjatcclem4  41519  dochkr1  41576  islpoldN  41582  lcfrlem31  41671  mapdpglem18  41787  mapdheq2  41827  mapdheq4  41830  mapdh6aN  41833  hdmap1l6a  41907  hdmap14lem4a  41969  lcmineqlem4  42124  frlmfzoccat  42597  drnginvmuld  42619  psrbagres  42638  evlselvlem  42678  evlselv  42679  fsuppind  42682  fsuppssind  42685  prjspvs  42702  irrapxlem4  42917  pell1234qrdich  42953  pell1qr1  42963  pell14qrgap  42967  pellqrexplicit  42969  rmspecfund  43001  fzmaxdif  43073  acongeq  43075  jm2.23  43088  jm3.1  43112  lmhmlnmsplit  43179  hbt  43222  dgrsub2  43227  proot1ex  43288  cantnfub  43413  cantnfresb  43416  cantnf2  43417  tfsconcatfv2  43432  tfsconcatrn  43434  tfsconcatb0  43436  naddcnff  43454  naddcnffo  43456  naddcnfid1  43459  naddcnfid2  43460  clublem  43702  dftrcl3  43812  mnugrud  44376  hashnzfz2  44413  dvconstbi  44426  ubelsupr  45116  restopn3  45247  wessf1ornlem  45281  lefldiveq  45392  iccintsng  45622  climsuse  45707  mullimc  45715  limcdm0  45717  limccog  45719  mullimcf  45722  constlimc  45723  idlimc  45725  limcperiod  45727  limsupre  45738  limcleqr  45741  neglimc  45744  addlimc  45745  0ellimcdiv  45746  xlimliminflimsup  45959  cncfshift  45971  cncfperiod  45976  cncfuni  45983  icccncfext  45984  cncfiooicclem1  45990  fperdvper  46016  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  mbfres2cn  46055  iblsplit  46063  stoweidlem7  46104  stoweidlem13  46110  stoweidlem26  46123  wallispilem3  46164  stirlinglem6  46176  stirlinglem10  46180  dirkercncf  46204  fourierdlem6  46210  fourierdlem11  46215  fourierdlem12  46216  fourierdlem15  46219  fourierdlem26  46230  fourierdlem42  46246  fourierdlem50  46253  fourierdlem51  46254  fourierdlem52  46255  fourierdlem54  46257  fourierdlem62  46265  fourierdlem79  46282  fourierdlem102  46305  fourierdlem114  46317  etransclem23  46354  chnsubseq  46977  3f1oss1  47174  zgeltp1eq  47408  setsnidel  47476  preimafvsnel  47478  iccpartres  47517  prpair  47600  fpprel2  47840  isubgrsubgr  47968  grimidvtxedg  47984  grimcnv  47987  isuspgrim  47995  upgrimpthslem2  48007  stgrnbgr0  48063  uhgrimgrlim  48086  clnbgr3stgrgrlim  48118  gpg5nbgrvtx03starlem2  48168  gpg5nbgrvtx13starlem2  48171  gpg5edgnedg  48229  isassintop  48309  rhmsubcALTV  48384  srhmsubcALTV  48424  fldhmsubcALTV  48432  rmfsupp  48472  scmfsupp  48474  mptcfsupp  48476  lcoel0  48528  lincsumcl  48531  lincscmcl  48532  lcoss  48536  lindsrng01  48568  lincreslvec3  48582  lindssnlvec  48586  zgtp1leeq  48621  lubsscl  49059  glbsscl  49060  idmon  49120  idepi  49121  iinfssc  49157  iinfsubc  49158  discsubc  49164  nelsubclem  49167  imassc  49253  imasubc3  49256  isnatd  49323  swapfiso  49385  fucoppc  49510  thinciso  49570  diagciso  49639  termolmd  49770