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  6998  fveqressseq  7018  fmptsng  7108  fmptsnd  7109  fnprb  7148  fntpb  7149  fpr3g  8221  frrlem4  8225  1ellim  8419  isfsuppd  9256  fdmfifsupp  9265  fczfsuppd  9276  fsuppmptif  9289  fsuppco2  9293  fsuppcor  9294  dffi3  9321  suppr  9362  infpr  9395  ordtypelem7  9416  cantnf0  9571  cantnfp1lem1  9574  cantnfp1lem2  9575  cantnfp1lem3  9576  cantnflem1a  9581  cantnflem1d  9584  cantnflem1  9585  cantnf  9589  rankpwi  9722  carduni  9880  fin23lem32  10241  fpwwe2lem5  10532  fpwwe2lem11  10538  fpwwe2lem12  10539  fpwwe2  10540  inttsk  10671  grutsk1  10718  add20  11635  supaddc  12095  supadd  12096  supmul  12100  suprzcl  12559  uzid  12753  uzwo3  12847  rpnnen1lem5  12885  xrletrid  13060  xrre  13074  xrre3  13076  xleadd1a  13158  xlemul1a  13193  elioc2  13315  elico2  13316  elicc2  13317  elfz1eq  13441  fzadd2  13465  fznatpl1  13484  elfz1uz  13500  nn0fz0  13531  fzctr  13546  fzo1fzo0n0  13621  fzoaddel  13623  elincfzoext  13629  flid  13718  flval3  13725  fladdz  13735  fldiv  13770  modid  13806  hashf1lem1  14368  pfxccatin12d  14658  repswpfx  14698  2cshw  14726  pfx2  14860  wwlktovf1  14870  sqeqd  15079  01sqrexlem7  15161  max0add  15223  abs2difabs  15248  rddif  15254  fzomaxdiflem  15256  rexico  15267  icodiamlt  15351  limsupgre  15394  rlim3  15411  icco1  15453  rlimclim  15459  rlimuni  15463  rlimresb  15478  isercolllem2  15579  isercolllem3  15580  isercoll  15581  caucvgrlem  15586  caurcvgr  15587  iseraltlem3  15597  fsum00  15711  o1fsum  15726  bitsfzolem  16351  bitsfzo  16352  bitsmod  16353  bitscmp  16355  gcd0id  16436  gcdneg  16439  bezoutlem4  16459  nn0seqcvgd  16487  lcmneg  16520  lcmfunsnlem2lem2  16556  qredeq  16574  prmind2  16602  eulerthlem2  16699  pcpremul  16761  pcidlem  16790  pcgcd1  16795  fldivp1  16815  pcfaclem  16816  4sqlem17  16879  vdwlem1  16899  vdwlem6  16904  vdwlem12  16910  vdwlem13  16911  0ram  16938  ram0  16940  ramub1lem1  16944  invco  17684  sectmon  17695  monsect  17696  invid  17700  ssctr  17738  ssceq  17739  0ssc  17750  0subcat  17751  catsubcat  17752  issubc3  17762  fullsubc  17763  funcinv  17786  fthmon  17842  fuccocl  17880  fucidcl  17881  invfuc  17890  2initoinv  17923  2termoinv  17930  elhomai  17946  setcmon  18000  setcepi  18001  catcisolem  18023  curf2cl  18143  yonedalem4c  18189  yonedalem3  18192  yoniso  18197  lublecl  18271  isacs3lem  18454  tsrdir  18516  chnccat  18538  rabsubmgmd  18618  submgmid  18620  subsubmgm  18624  mgmhmima  18629  mgmhmeql  18630  mndpfsupp  18681  mnd1  18693  sgrp2nmndlem4  18842  sgrp2nmndlem5  18843  0subg  19070  nmznsg  19086  ghmpreima  19156  ghmeql  19157  ghmnsgpreima  19159  kerf1ghm  19165  cntzsgrpcl  19252  cntzsubm  19256  cntzsubg  19257  cntzmhm  19259  symgextfo  19340  symgfixf1  19355  symgfixfolem1  19356  odlem2  19457  finodsubmsubg  19485  gexlem2  19500  gexcl2  19507  sylow1lem5  19520  subgslw  19534  slwhash  19542  fislw  19543  sylow3lem1  19545  lsmsubg  19572  efgredlemd  19662  efgredlem  19665  efgcpbllemb  19673  frgpuplem  19690  cyggeninv  19801  iscygd  19805  iscygodd  19806  gsumzadd  19840  gsumconst  19852  gsumpt  19880  gsum2dlem2  19889  gsum2d  19890  gsum2d2lem  19891  dprdfcntz  19935  eldprdi  19938  subgdmdprd  19954  subgdprd  19955  dprdpr  19970  ablfac1c  19991  ablfac1eu  19993  ablfaclem3  20007  ogrpaddlt  20056  ogrpsublt  20060  ring1  20234  subrngint  20481  rhmimasubrng  20487  cntzsubrng  20488  rhmeql  20524  rhmima  20525  cntzsubr  20527  rnghmsscmap2  20550  rnghmsscmap  20551  rnghmsubcsetc  20554  zrzeroorngc  20565  rhmsscmap2  20579  rhmsscmap  20580  rhmsubcsetc  20583  rhmsscrnghm  20586  rhmsubcrngc  20589  srhmsubc  20601  rhmsubc  20610  issubdrg  20701  fldhmsubc  20706  imadrhmcl  20718  isabvd  20733  abvdiv  20750  ornglmullt  20790  orngrmullt  20791  orngmullt  20792  ofldlt1  20796  lsslsp  20954  lsslspOLD  20955  lmhmima  20987  lmhmpreima  20988  lmhmeql  20995  lsmcl  21023  lspfixed  21071  rnglidlrng  21190  rngqiprngim  21247  rng2idl1cntr  21248  qsssubdrg  21369  gzrngunit  21376  pzriprnglem8  21431  evpmodpmf1o  21539  ocvpj  21660  dsmm0cl  21683  dsmmacl  21684  dsmmsubg  21686  dsmmlss  21687  frlmsplit2  21716  uvcff  21734  lindfrn  21764  f1lindf  21765  lindsss  21767  issubassa  21810  issubassa2  21835  snifpsrbag  21863  psrbaglesupp  21865  psrbaglecl  21866  psrbagaddcl  21867  psrbagcon  21868  mplsubglem  21942  mpllsslem  21943  mplassa  21965  subrgmpl  21973  mplcoe5  21981  mplbas2  21983  mplind  22011  mpfind  22048  ismhp2  22062  mhpmulcl  22070  mhplss  22076  ply1assa  22118  coe1tmmul2  22196  coe1tmmul  22197  cply1coe0bi  22223  dmatid  22416  dmatsubcl  22419  dmatscmcl  22424  scmatid  22435  scmataddcl  22437  scmatsubcl  22438  scmatmulcl  22439  smatvscl  22445  scmatrhmcl  22449  mat0scmat  22459  mat1scmat  22460  mdet0pr  22513  chmaidscmat  22769  distop  22916  indistopon  22922  ppttop  22928  epttop  22930  mretopd  23013  toponmre  23014  neiss  23030  opnneissb  23035  ssnei2  23037  innei  23046  neiptoptop  23052  ordtcld1  23118  ordtcld2  23119  lmconst  23182  cnpnei  23185  iscncl  23190  cnss1  23197  cnss2  23198  cncnpi  23199  cncnp  23201  cnconst2  23204  cnrest  23206  cnpresti  23209  cnpdis  23214  paste  23215  lmcnp  23225  cnhaus  23275  hauscmp  23328  2ndcomap  23379  1stcelcls  23382  1stccnp  23383  llyrest  23406  nllyrest  23407  llyidm  23409  nllyidm  23410  ssref  23433  reftr  23435  refun0  23436  dissnref  23449  kgentopon  23459  kgenidm  23468  kgencn3  23479  txcld  23524  neitx  23528  tx1cn  23530  tx2cn  23531  ptcld  23534  xkoccn  23540  txcnp  23541  ptcnp  23543  txcnmpt  23545  ptcn  23548  txdis1cn  23556  ptrescn  23560  txkgen  23573  xkoco1cn  23578  xkoco2cn  23579  xkococn  23581  xkoinjcn  23608  qtoptop2  23620  qtopuni  23623  qtopid  23626  qtopkgen  23631  basqtop  23632  tgqtop  23633  qtopss  23636  qtopeu  23637  qtoprest  23638  kqopn  23655  kqcld  23656  kqreglem2  23663  reghmph  23714  ordthmeolem  23722  qtopf1  23737  opnfbas  23763  isfil2  23777  fbasweak  23786  fsubbas  23788  filconn  23804  fbasrn  23805  rnelfmlem  23873  flimss2  23893  flimss1  23894  hausflim  23902  flimclslem  23905  flimsncls  23907  cnpflfi  23920  flfcnp2  23928  fclsfnflim  23948  cnextfvval  23986  cnextfres1  23989  symgtgp  24027  opnsubg  24029  ghmcnp  24036  qustgpopn  24041  qustgplem  24042  qustgphaus  24044  tsmsfbas  24049  ustfilxp  24134  utoptop  24155  utopbas  24156  restutopopn  24159  iducn  24203  cstucnd  24204  ucncn  24205  fmucnd  24212  cfilufg  24213  trcfilu  24214  cfiluweak  24215  neipcfilu  24216  psmetres2  24235  isxmetd  24247  xmetpsmet  24269  imasf1oxmet  24296  xblss2ps  24322  xblss2  24323  xblcntrps  24331  xblcntr  24332  blcld  24426  metustfbas  24478  cfilucfil  24480  restmetu  24491  ngptgp  24557  tngngpd  24574  nrmtngnrm  24579  tngnrg  24595  nlmvscn  24608  nrginvrcn  24613  nmo0  24656  nmoeq0  24657  nmoid  24663  nghmcn  24666  0nmhm  24676  blcvx  24719  iccntr  24743  xrge0tsms  24756  xmetdcn2  24759  metdstri  24773  metdscn  24778  rescncf  24823  cncfco  24833  oprpiece1res2  24883  cnheibor  24887  cnllycmp  24888  bndth  24890  ishtpyd  24907  isphtpyd  24918  pcoval2  24949  nmhmcn  25053  ipcn  25179  lmnn  25196  cfilss  25203  iscfil3  25206  cfilfcls  25207  cmetcaulem  25221  iscmet3lem2  25225  cfilres  25229  lmcau  25246  flimcfil  25247  cncmet  25255  rlmbn  25294  minveclem3b  25361  pjthlem1  25370  pjth2  25373  ivthlem3  25387  ovolssnul  25421  ovolctb  25424  ovoliunnul  25441  ovolsca  25449  ovolicopnf  25458  voliunlem2  25485  volsup  25490  dyadmaxlem  25531  vitalilem5  25546  mbfres  25578  mbfss  25580  mbfmulc2re  25582  mbfadd  25595  mbfmulc2  25597  mbflim  25602  i1faddlem  25627  i1fmullem  25628  mbfmul  25660  itg2mulc  25681  itg2cnlem1  25695  ibl0  25721  iblposlem  25726  itgreval  25731  iblneg  25737  iblss  25739  iblss2  25740  itgle  25744  iblconst  25752  iblabs  25763  iblabsr  25764  iblmulc2  25765  bddmulibl  25773  limciun  25828  limcun  25829  dvres2lem  25844  dvidlem  25849  dvcnp2  25854  dvcnp2OLD  25855  dvcn  25856  cpnres  25872  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvcobr  25882  dvcobrOLD  25883  dvcjbr  25886  dvrec  25892  dvcnvlem  25913  dvferm  25925  dvlip2  25933  dveq0  25938  dv11cn  25939  dvivthlem1  25946  lhop1  25952  lhop2  25953  lhop  25954  dvcnvre  25957  dvfsumlem3  25968  dvfsumlem4  25969  dvfsumrlim  25971  dvfsum2  25974  ftc1a  25977  ftc1lem4  25979  ftc1lem6  25981  ftc1  25982  coe1mul3  26037  deg1addle2  26040  deg1sublt  26048  fta1blem  26109  drnguc1p  26112  ig1prsp  26119  plyco0  26130  plyeq0lem  26148  dgrub  26172  dgreq  26182  dgradd2  26207  dgrmul  26209  dgrcolem2  26213  dgrco  26214  plycpn  26230  plydivlem4  26237  plydiveu  26239  vieta1lem2  26252  vieta1  26253  aalioulem2  26274  aalioulem3  26275  aaliou3lem7  26290  tayl0  26302  ulmcn  26341  ulmdvlem3  26344  psercn  26369  abelth  26384  pilem3  26396  efif1olem1  26484  abslogimle  26515  argregt0  26552  argrege0  26553  logf1o2  26592  cxpsqrtlem  26644  cxpcn3  26691  abscxpbnd  26696  logreclem  26705  ang180lem2  26753  ang180lem3  26754  xrlimcnp  26911  harmonicbnd4  26954  fsumharmonic  26955  lgamgulmlem5  26976  lgambdd  26980  basellem4  27027  dvdsppwf1o  27129  dvdsflf1o  27130  fsumfldivdiaglem  27132  chpeq0  27152  chteq0  27153  chtub  27156  chpub  27164  dchrelbasd  27183  dchrmulcl  27193  dchrinv  27205  bposlem1  27228  bposlem2  27229  lgsdirprm  27275  lgsqrlem2  27291  lgsqrlem3  27292  lgsdchr  27299  lgseisenlem1  27319  lgseisenlem2  27320  lgseisenlem3  27321  lgsquadlem1  27324  2sqlem8  27370  2sqblem  27375  2sqmod  27380  chebbnd1lem1  27413  dchrisumlem1  27433  dchrisumlem2  27434  dchrisumlem3  27435  dchrisum0fno1  27455  pntrmax  27508  pntpbnd1a  27529  pntibndlem3  27536  pntlemn  27544  pntlemi  27548  pntlem3  27553  pntleml  27555  ostth1  27577  ostth2  27581  ostth3  27582  nosepon  27610  nolesgn2ores  27617  nogesgn1ores  27619  nosupres  27652  nosupbnd1lem2  27654  nosupbnd2lem1  27660  noinfres  27667  noinfbnd1lem2  27669  noinfbnd2lem1  27675  eqscut3  27771  cofcutrtime  27877  divmuldivsd  28176  divdivs1d  28177  nnsgt0  28273  ercgrg  28501  motco  28524  cnvmot  28525  legso  28583  mirmot  28659  colopp  28753  hphl  28755  lmicom  28772  lmimid  28778  lmimot  28782  hypcgrlem1  28783  hypcgrlem2  28784  trgcopyeulem  28789  inagswap  28825  inaghl  28829  cgrg3col4  28837  brbtwn2  28890  axlowdimlem3  28929  axlowdimlem16  28942  axcontlem8  28956  fusgrfis  29315  nbgr2vtx1edg  29335  0vtxrgr  29562  0vtxrusgr  29563  ewlkle  29591  wlk1ewlk  29625  uspgr2wlkeq2  29632  wlkp1lem8  29664  trlontrl  29694  pthonpth  29733  pthdlem2  29753  wlklnwwlkln1  29853  wlknewwlksn  29872  wwlksnred  29877  wwlksnredwwlkn0  29881  2trlond  29924  2pthond  29927  elwwlks2ons3im  29939  clwlkclwwlklem2a1  29979  clwlkclwwlkf1  29997  clwwlkel  30033  clwwlkwwlksb  30041  wwlksext2clwwlk  30044  1ewlk  30102  0trlon  30111  0pthon  30114  1pthond  30131  3trlond  30160  3pthond  30162  3spthond  30164  eupthres  30202  2clwwlk2clwwlk  30337  numclwwlk1lem2foa  30341  numclwwlk1lem2f1  30344  nvabs  30659  vacn  30681  nmcvcn  30682  nmblore  30773  0lno  30777  0blo  30779  nmlno0lem  30780  occl  31291  pjhthlem1  31378  pjpjpre  31406  nmopre  31857  nmlnop0iALT  31982  nmophmi  32018  leoprf2  32114  stlesi  32228  disjdifprg  32562  disjun0  32582  fsuppcurry1  32714  fsuppcurry2  32715  fpwrelmap  32723  fzspl  32779  dfmgc2lem  32983  pwrssmgc  32988  xrge0tsmsd  33049  psgnfzto1stlem  33076  fzto1st1  33078  evpmid  33124  pnfinf  33159  isarchiofld  33175  rmfsupp2  33212  fracfld  33281  dvdsruassoi  33356  nsgmgc  33384  drngidl  33405  qsdrngi  33467  deg1addlt  33567  ply1degltdimlem  33642  lbsdiflsp0  33646  fedgmul  33651  fldexttr  33678  fldextid  33679  irngnzply1lem  33710  finextalg  33718  minplyelirng  33735  irredminply  33736  algextdeglem8  33744  rtelextdg2lem  33746  constrsslem  33761  constrllcllem  33772  constrlccllem  33773  constrcccllem  33774  qtopt1  33855  reff  33859  locfinreflem  33860  metideq  33913  metider  33914  pstmxmet  33917  qqhval2lem  34001  qqhcn  34011  qqhucn  34012  pwsiga  34150  prsiga  34151  measle0  34228  mbfmcst  34279  1stmbfm  34280  2ndmbfm  34281  imambfm  34282  cnmbfm  34283  mbfmco  34284  mbfmco2  34285  0elcarsg  34327  carsgclctun  34341  sibfof  34360  oddpwdc  34374  eulerpartlemmf  34395  eulerpartlemgs2  34400  0rrv  34471  ballotlemfc0  34513  ballotlemfcc  34514  signstfveq0  34597  breprexplemc  34652  bnj1452  35071  usgrgt2cycl  35181  acycgr1v  35200  derangen  35223  subfacval3  35240  cvmseu  35327  cvmliftmolem2  35333  cvmliftlem7  35342  cvmliftlem15  35349  cvmlift2lem9a  35354  cvmlift2lem9  35362  cvmlift2lem10  35363  cvmlift2lem11  35364  cvmlift2lem12  35365  cvmlift3lem6  35375  cvmlift3lem8  35377  ex-sategoelel  35472  ex-sategoelelomsuc  35477  mclsppslem  35634  mclspps  35635  wsuclem  35874  fness  36400  fnetr  36402  fnessref  36408  refssfne  36409  neibastop1  36410  neibastop2  36412  tailfb  36428  filnetlem3  36431  weiunfrlem  36515  bj-finsumval0  37336  bj-rvecvec  37350  dfgcd3  37375  lindsadd  37659  poimirlem13  37679  poimirlem15  37681  poimirlem24  37690  poimirlem28  37694  mblfinlem2  37704  ovoliunnfl  37708  volsupnfl  37711  mbfresfi  37712  iblabsnc  37730  iblmulc2nc  37731  ftc1cnnclem  37737  ftc1cnnc  37738  ftc1anc  37747  sdclem2  37788  metf1o  37801  ismtyhmeolem  37850  ismtyres  37854  heibor1lem  37855  bfplem2  37869  bfp  37870  rrncmslem  37878  iccbnd  37886  icccmpALT  37887  rngogrphom  38017  rngoisoco  38028  keridl  38078  lsmcv2  39134  lsatcv0  39136  lcvexchlem4  39142  lcvexchlem5  39143  l1cvpat  39159  lfl0f  39174  lfladdcl  39176  lflnegcl  39180  lkrlss  39200  eqlkr  39204  lkrlsp  39207  lkrlsp2  39208  lshpkrcl  39221  lkrin  39269  1cvrjat  39580  llni  39613  llnle  39623  lplni  39637  lplnle  39645  llncvrlpln2  39662  2atmat  39666  lvoli  39680  lplncvrlvol2  39720  elpaddri  39907  paddclN  39947  pclclN  39996  pclfinN  40005  0psubclN  40048  1psubclN  40049  atpsubclN  40050  pmapsubclN  40051  osumclN  40072  pexmidN  40074  pexmidlem6N  40080  lhp2lt  40106  lautcnv  40195  idlaut  40201  lautco  40202  idldil  40219  ldilcnv  40220  ldilco  40221  ltrncnv  40251  idltrn  40255  cdleme16d  40386  cdleme50laut  40652  cdleme50ldil  40653  cdleme50ltrn  40662  ltrnco  40824  dian0  41144  dia0eldmN  41145  dia1eldmN  41146  dialss  41151  diaintclN  41163  docaclN  41229  doca2N  41231  djajN  41242  dibintclN  41272  diblss  41275  dicvaddcl  41295  dicvscacl  41296  dicn0  41297  cdlemn11a  41312  dihord2cN  41326  dihord11b  41327  dihord6apre  41361  dihmeetlem1N  41395  dihglblem5apreN  41396  dihpN  41441  dihjatcclem4  41526  dochkr1  41583  islpoldN  41589  lcfrlem31  41678  mapdpglem18  41794  mapdheq2  41834  mapdheq4  41837  mapdh6aN  41840  hdmap1l6a  41914  hdmap14lem4a  41976  lcmineqlem4  42131  frlmfzoccat  42604  drnginvmuld  42626  psrbagres  42645  evlselvlem  42685  evlselv  42686  fsuppind  42689  fsuppssind  42692  prjspvs  42709  irrapxlem4  42923  pell1234qrdich  42959  pell1qr1  42969  pell14qrgap  42973  pellqrexplicit  42975  rmspecfund  43007  fzmaxdif  43079  acongeq  43081  jm2.23  43094  jm3.1  43118  lmhmlnmsplit  43185  hbt  43228  dgrsub2  43233  proot1ex  43294  cantnfub  43419  cantnfresb  43422  cantnf2  43423  tfsconcatfv2  43438  tfsconcatrn  43440  tfsconcatb0  43442  naddcnff  43460  naddcnffo  43462  naddcnfid1  43465  naddcnfid2  43466  clublem  43708  dftrcl3  43818  mnugrud  44382  hashnzfz2  44419  dvconstbi  44432  ubelsupr  45122  restopn3  45253  wessf1ornlem  45287  lefldiveq  45398  iccintsng  45628  climsuse  45713  mullimc  45721  limcdm0  45723  limccog  45725  mullimcf  45728  constlimc  45729  idlimc  45731  limcperiod  45733  limsupre  45744  limcleqr  45747  neglimc  45750  addlimc  45751  0ellimcdiv  45752  xlimliminflimsup  45965  cncfshift  45977  cncfperiod  45982  cncfuni  45989  icccncfext  45990  cncfiooicclem1  45996  fperdvper  46022  ioodvbdlimc1lem2  46035  ioodvbdlimc2lem  46037  mbfres2cn  46061  iblsplit  46069  stoweidlem7  46110  stoweidlem13  46116  stoweidlem26  46129  wallispilem3  46170  stirlinglem6  46182  stirlinglem10  46186  dirkercncf  46210  fourierdlem6  46216  fourierdlem11  46221  fourierdlem12  46222  fourierdlem15  46225  fourierdlem26  46236  fourierdlem42  46252  fourierdlem50  46259  fourierdlem51  46260  fourierdlem52  46261  fourierdlem54  46263  fourierdlem62  46271  fourierdlem79  46288  fourierdlem102  46311  fourierdlem114  46323  etransclem23  46360  chnsubseq  46983  3f1oss1  47180  zgeltp1eq  47414  setsnidel  47482  preimafvsnel  47484  iccpartres  47523  prpair  47606  fpprel2  47846  isubgrsubgr  47974  grimidvtxedg  47990  grimcnv  47993  isuspgrim  48001  upgrimpthslem2  48013  stgrnbgr0  48069  uhgrimgrlim  48092  clnbgr3stgrgrlim  48124  gpg5nbgrvtx03starlem2  48174  gpg5nbgrvtx13starlem2  48177  gpg5edgnedg  48235  isassintop  48315  rhmsubcALTV  48390  srhmsubcALTV  48430  fldhmsubcALTV  48438  rmfsupp  48478  scmfsupp  48480  mptcfsupp  48482  lcoel0  48534  lincsumcl  48537  lincscmcl  48538  lcoss  48542  lindsrng01  48574  lincreslvec3  48588  lindssnlvec  48592  zgtp1leeq  48627  lubsscl  49065  glbsscl  49066  idmon  49126  idepi  49127  iinfssc  49163  iinfsubc  49164  discsubc  49170  nelsubclem  49173  imassc  49259  imasubc3  49262  isnatd  49329  swapfiso  49391  fucoppc  49516  thinciso  49576  diagciso  49645  termolmd  49776