Theorem mpbir2and 714

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  7012  fveqressseq  7032  fmptsng  7123  fmptsnd  7124  fnprb  7163  fntpb  7164  fpr3g  8235  frrlem4  8239  1ellim  8433  isfsuppd  9279  fdmfifsupp  9288  fczfsuppd  9299  fsuppmptif  9312  fsuppco2  9316  fsuppcor  9317  dffi3  9344  suppr  9385  infpr  9418  ordtypelem7  9439  cantnf0  9596  cantnfp1lem1  9599  cantnfp1lem2  9600  cantnfp1lem3  9601  cantnflem1a  9606  cantnflem1d  9609  cantnflem1  9610  cantnf  9614  rankpwi  9747  carduni  9905  fin23lem32  10266  fpwwe2lem5  10558  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  inttsk  10697  grutsk1  10744  add20  11662  supaddc  12123  supadd  12124  supmul  12128  suprzcl  12609  uzid  12803  uzwo3  12893  rpnnen1lem5  12931  xrletrid  13106  xrre  13121  xrre3  13123  xleadd1a  13205  xlemul1a  13240  elioc2  13362  elico2  13363  elicc2  13364  elfz1eq  13489  fzadd2  13513  fznatpl1  13532  elfz1uz  13548  nn0fz0  13579  fzctr  13594  fzo1fzo0n0  13670  fzoaddel  13672  elincfzoext  13678  flid  13767  flval3  13774  fladdz  13784  fldiv  13819  modid  13855  hashf1lem1  14417  pfxccatin12d  14707  repswpfx  14747  2cshw  14775  pfx2  14909  wwlktovf1  14919  sqeqd  15128  01sqrexlem7  15210  max0add  15272  abs2difabs  15297  rddif  15303  fzomaxdiflem  15305  rexico  15316  icodiamlt  15400  limsupgre  15443  rlim3  15460  icco1  15502  rlimclim  15508  rlimuni  15512  rlimresb  15527  isercolllem2  15628  isercolllem3  15629  isercoll  15630  caucvgrlem  15635  caurcvgr  15636  iseraltlem3  15646  fsum00  15761  o1fsum  15776  bitsfzolem  16403  bitsfzo  16404  bitsmod  16405  bitscmp  16407  gcd0id  16488  gcdneg  16491  bezoutlem4  16511  nn0seqcvgd  16539  lcmneg  16572  lcmfunsnlem2lem2  16608  qredeq  16626  prmind2  16654  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  17738  sectmon  17749  monsect  17750  invid  17754  ssctr  17792  ssceq  17793  0ssc  17804  0subcat  17805  catsubcat  17806  issubc3  17816  fullsubc  17817  funcinv  17840  fthmon  17896  fuccocl  17934  fucidcl  17935  invfuc  17944  2initoinv  17977  2termoinv  17984  elhomai  18000  setcmon  18054  setcepi  18055  catcisolem  18077  curf2cl  18197  yonedalem4c  18243  yonedalem3  18246  yoniso  18251  lublecl  18325  isacs3lem  18508  tsrdir  18570  chnccat  18592  rabsubmgmd  18672  submgmid  18674  subsubmgm  18678  mgmhmima  18683  mgmhmeql  18684  mndpfsupp  18735  mnd1  18747  sgrp2nmndlem4  18899  sgrp2nmndlem5  18900  0subg  19127  nmznsg  19143  ghmpreima  19213  ghmeql  19214  ghmnsgpreima  19216  kerf1ghm  19222  cntzsgrpcl  19309  cntzsubm  19313  cntzsubg  19314  cntzmhm  19316  symgextfo  19397  symgfixf1  19412  symgfixfolem1  19413  odlem2  19514  finodsubmsubg  19542  gexlem2  19557  gexcl2  19564  sylow1lem5  19577  subgslw  19591  slwhash  19599  fislw  19600  sylow3lem1  19602  lsmsubg  19629  efgredlemd  19719  efgredlem  19722  efgcpbllemb  19730  frgpuplem  19747  cyggeninv  19858  iscygd  19862  iscygodd  19863  gsumzadd  19897  gsumconst  19909  gsumpt  19937  gsum2dlem2  19946  gsum2d  19947  gsum2d2lem  19948  dprdfcntz  19992  eldprdi  19995  subgdmdprd  20011  subgdprd  20012  dprdpr  20027  ablfac1c  20048  ablfac1eu  20050  ablfaclem3  20064  ogrpaddlt  20113  ogrpsublt  20117  ring1  20291  subrngint  20537  rhmimasubrng  20543  cntzsubrng  20544  rhmeql  20580  rhmima  20581  cntzsubr  20583  rnghmsscmap2  20606  rnghmsscmap  20607  rnghmsubcsetc  20610  zrzeroorngc  20621  rhmsscmap2  20635  rhmsscmap  20636  rhmsubcsetc  20639  rhmsscrnghm  20642  rhmsubcrngc  20645  srhmsubc  20657  rhmsubc  20666  issubdrg  20757  fldhmsubc  20762  imadrhmcl  20774  isabvd  20789  abvdiv  20806  ornglmullt  20846  orngrmullt  20847  orngmullt  20848  ofldlt1  20852  lsslsp  21010  lmhmima  21042  lmhmpreima  21043  lmhmeql  21050  lsmcl  21078  lspfixed  21126  rnglidlrng  21245  rngqiprngim  21302  rng2idl1cntr  21303  qsssubdrg  21406  gzrngunit  21413  pzriprnglem8  21468  evpmodpmf1o  21576  ocvpj  21697  dsmm0cl  21720  dsmmacl  21721  dsmmsubg  21723  dsmmlss  21724  frlmsplit2  21753  uvcff  21771  lindfrn  21801  f1lindf  21802  lindsss  21804  issubassa  21847  issubassa2  21872  snifpsrbag  21900  psrbaglesupp  21902  psrbaglecl  21903  psrbagaddcl  21904  psrbagcon  21905  mplsubglem  21977  mpllsslem  21978  mplassa  22000  subrgmpl  22010  mplcoe5  22018  mplbas2  22020  mplind  22048  mpfind  22093  ismhp2  22107  mhpmulcl  22115  mhplss  22121  ply1assa  22163  coe1tmmul2  22241  coe1tmmul  22242  cply1coe0bi  22267  dmatid  22460  dmatsubcl  22463  dmatscmcl  22468  scmatid  22479  scmataddcl  22481  scmatsubcl  22482  scmatmulcl  22483  smatvscl  22489  scmatrhmcl  22493  mat0scmat  22503  mat1scmat  22504  mdet0pr  22557  chmaidscmat  22813  distop  22960  indistopon  22966  ppttop  22972  epttop  22974  mretopd  23057  toponmre  23058  neiss  23074  opnneissb  23079  ssnei2  23081  innei  23090  neiptoptop  23096  ordtcld1  23162  ordtcld2  23163  lmconst  23226  cnpnei  23229  iscncl  23234  cnss1  23241  cnss2  23242  cncnpi  23243  cncnp  23245  cnconst2  23248  cnrest  23250  cnpresti  23253  cnpdis  23258  paste  23259  lmcnp  23269  cnhaus  23319  hauscmp  23372  2ndcomap  23423  1stcelcls  23426  1stccnp  23427  llyrest  23450  nllyrest  23451  llyidm  23453  nllyidm  23454  ssref  23477  reftr  23479  refun0  23480  dissnref  23493  kgentopon  23503  kgenidm  23512  kgencn3  23523  txcld  23568  neitx  23572  tx1cn  23574  tx2cn  23575  ptcld  23578  xkoccn  23584  txcnp  23585  ptcnp  23587  txcnmpt  23589  ptcn  23592  txdis1cn  23600  ptrescn  23604  txkgen  23617  xkoco1cn  23622  xkoco2cn  23623  xkococn  23625  xkoinjcn  23652  qtoptop2  23664  qtopuni  23667  qtopid  23670  qtopkgen  23675  basqtop  23676  tgqtop  23677  qtopss  23680  qtopeu  23681  qtoprest  23682  kqopn  23699  kqcld  23700  kqreglem2  23707  reghmph  23758  ordthmeolem  23766  qtopf1  23781  opnfbas  23807  isfil2  23821  fbasweak  23830  fsubbas  23832  filconn  23848  fbasrn  23849  rnelfmlem  23917  flimss2  23937  flimss1  23938  hausflim  23946  flimclslem  23949  flimsncls  23951  cnpflfi  23964  flfcnp2  23972  fclsfnflim  23992  cnextfvval  24030  cnextfres1  24033  symgtgp  24071  opnsubg  24073  ghmcnp  24080  qustgpopn  24085  qustgplem  24086  qustgphaus  24088  tsmsfbas  24093  ustfilxp  24178  utoptop  24199  utopbas  24200  restutopopn  24203  iducn  24247  cstucnd  24248  ucncn  24249  fmucnd  24256  cfilufg  24257  trcfilu  24258  cfiluweak  24259  neipcfilu  24260  psmetres2  24279  isxmetd  24291  xmetpsmet  24313  imasf1oxmet  24340  xblss2ps  24366  xblss2  24367  xblcntrps  24375  xblcntr  24376  blcld  24470  metustfbas  24522  cfilucfil  24524  restmetu  24535  ngptgp  24601  tngngpd  24618  nrmtngnrm  24623  tngnrg  24639  nlmvscn  24652  nrginvrcn  24657  nmo0  24700  nmoeq0  24701  nmoid  24707  nghmcn  24710  0nmhm  24720  blcvx  24763  iccntr  24787  xrge0tsms  24800  xmetdcn2  24803  metdstri  24817  metdscn  24822  rescncf  24864  cncfco  24874  oprpiece1res2  24919  cnheibor  24922  cnllycmp  24923  bndth  24925  ishtpyd  24942  isphtpyd  24953  pcoval2  24983  nmhmcn  25087  ipcn  25213  lmnn  25230  cfilss  25237  iscfil3  25240  cfilfcls  25241  cmetcaulem  25255  iscmet3lem2  25259  cfilres  25263  lmcau  25280  flimcfil  25281  cncmet  25289  rlmbn  25328  minveclem3b  25395  pjthlem1  25404  pjth2  25407  ivthlem3  25420  ovolssnul  25454  ovolctb  25457  ovoliunnul  25474  ovolsca  25482  ovolicopnf  25491  voliunlem2  25518  volsup  25523  dyadmaxlem  25564  vitalilem5  25579  mbfres  25611  mbfss  25613  mbfmulc2re  25615  mbfadd  25628  mbfmulc2  25630  mbflim  25635  i1faddlem  25660  i1fmullem  25661  mbfmul  25693  itg2mulc  25714  itg2cnlem1  25728  ibl0  25754  iblposlem  25759  itgreval  25764  iblneg  25770  iblss  25772  iblss2  25773  itgle  25777  iblconst  25785  iblabs  25796  iblabsr  25797  iblmulc2  25798  bddmulibl  25806  limciun  25861  limcun  25862  dvres2lem  25877  dvidlem  25882  dvcnp2  25887  dvcn  25888  cpnres  25904  dvaddbr  25905  dvmulbr  25906  dvcobr  25913  dvcjbr  25916  dvrec  25922  dvcnvlem  25943  dvferm  25955  dvlip2  25962  dveq0  25967  dv11cn  25968  dvivthlem1  25975  lhop1  25981  lhop2  25982  lhop  25983  dvcnvre  25986  dvfsumlem3  25995  dvfsumlem4  25996  dvfsumrlim  25998  dvfsum2  26001  ftc1a  26004  ftc1lem4  26006  ftc1lem6  26008  ftc1  26009  coe1mul3  26064  deg1addle2  26067  deg1sublt  26075  fta1blem  26136  drnguc1p  26139  ig1prsp  26146  plyco0  26157  plyeq0lem  26175  dgrub  26199  dgreq  26209  dgradd2  26233  dgrmul  26235  dgrcolem2  26239  dgrco  26240  plycpn  26255  plydivlem4  26262  plydiveu  26264  vieta1lem2  26277  vieta1  26278  aalioulem2  26299  aalioulem3  26300  aaliou3lem7  26315  tayl0  26327  ulmcn  26364  ulmdvlem3  26367  psercn  26391  abelth  26406  pilem3  26418  efif1olem1  26506  abslogimle  26537  argregt0  26574  argrege0  26575  logf1o2  26614  cxpsqrtlem  26666  cxpcn3  26712  abscxpbnd  26717  logreclem  26726  ang180lem2  26774  ang180lem3  26775  xrlimcnp  26932  harmonicbnd4  26974  fsumharmonic  26975  lgamgulmlem5  26996  lgambdd  27000  basellem4  27047  dvdsppwf1o  27149  dvdsflf1o  27150  fsumfldivdiaglem  27152  chpeq0  27171  chteq0  27172  chtub  27175  chpub  27183  dchrelbasd  27202  dchrmulcl  27212  dchrinv  27224  bposlem1  27247  bposlem2  27248  lgsdirprm  27294  lgsqrlem2  27310  lgsqrlem3  27311  lgsdchr  27318  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgsquadlem1  27343  2sqlem8  27389  2sqblem  27394  2sqmod  27399  chebbnd1lem1  27432  dchrisumlem1  27452  dchrisumlem2  27453  dchrisumlem3  27454  dchrisum0fno1  27474  pntrmax  27527  pntpbnd1a  27548  pntibndlem3  27555  pntlemn  27563  pntlemi  27567  pntlem3  27572  pntleml  27574  ostth1  27596  ostth2  27600  ostth3  27601  nosepon  27629  nolesgn2ores  27636  nogesgn1ores  27638  nosupres  27671  nosupbnd1lem2  27673  nosupbnd2lem1  27679  noinfres  27686  noinfbnd1lem2  27688  noinfbnd2lem1  27694  eqcuts3  27796  cofcutrtime  27919  divmuldivsd  28224  divdivs1d  28225  onsbnd  28273  nnsgt0  28331  bdayfinbndlem1  28459  ercgrg  28585  motco  28608  cnvmot  28609  legso  28667  mirmot  28743  colopp  28837  hphl  28839  lmicom  28856  lmimid  28862  lmimot  28866  hypcgrlem1  28867  hypcgrlem2  28868  trgcopyeulem  28873  inagswap  28909  inaghl  28913  cgrg3col4  28921  brbtwn2  28974  axlowdimlem3  29013  axlowdimlem16  29026  axcontlem8  29040  fusgrfis  29399  nbgr2vtx1edg  29419  0vtxrgr  29645  0vtxrusgr  29646  ewlkle  29674  wlk1ewlk  29708  uspgr2wlkeq2  29715  wlkp1lem8  29747  trlontrl  29777  pthonpth  29816  pthdlem2  29836  wlklnwwlkln1  29936  wlknewwlksn  29955  wwlksnred  29960  wwlksnredwwlkn0  29964  2trlond  30007  2pthond  30010  elwwlks2ons3im  30022  clwlkclwwlklem2a1  30062  clwlkclwwlkf1  30080  clwwlkel  30116  clwwlkwwlksb  30124  wwlksext2clwwlk  30127  1ewlk  30185  0trlon  30194  0pthon  30197  1pthond  30214  3trlond  30243  3pthond  30245  3spthond  30247  eupthres  30285  2clwwlk2clwwlk  30420  numclwwlk1lem2foa  30424  numclwwlk1lem2f1  30427  nvabs  30743  vacn  30765  nmcvcn  30766  nmblore  30857  0lno  30861  0blo  30863  nmlno0lem  30864  occl  31375  pjhthlem1  31462  pjpjpre  31490  nmopre  31941  nmlnop0iALT  32066  nmophmi  32102  leoprf2  32198  stlesi  32312  disjdifprg  32645  disjun0  32665  fsuppcurry1  32797  fsuppcurry2  32798  fpwrelmap  32806  fzspl  32862  dfmgc2lem  33055  pwrssmgc  33060  xrge0tsmsd  33134  psgnfzto1stlem  33161  fzto1st1  33163  evpmid  33209  pnfinf  33244  isarchiofld  33260  rmfsupp2  33299  fracfld  33369  dvdsruassoi  33444  nsgmgc  33472  drngidl  33493  qsdrngi  33555  deg1addlt  33660  ply1degltdimlem  33766  lbsdiflsp0  33770  fedgmul  33775  fldexttr  33802  fldextid  33803  irngnzply1lem  33834  finextalg  33842  minplyelirng  33859  irredminply  33860  algextdeglem8  33868  rtelextdg2lem  33870  constrsslem  33885  constrllcllem  33896  constrlccllem  33897  constrcccllem  33898  qtopt1  33979  reff  33983  locfinreflem  33984  metideq  34037  metider  34038  pstmxmet  34041  qqhval2lem  34125  qqhcn  34135  qqhucn  34136  pwsiga  34274  prsiga  34275  measle0  34352  mbfmcst  34403  1stmbfm  34404  2ndmbfm  34405  imambfm  34406  cnmbfm  34407  mbfmco  34408  mbfmco2  34409  0elcarsg  34451  carsgclctun  34465  sibfof  34484  oddpwdc  34498  eulerpartlemmf  34519  eulerpartlemgs2  34524  0rrv  34595  ballotlemfc0  34637  ballotlemfcc  34638  signstfveq0  34721  breprexplemc  34776  bnj1452  35194  usgrgt2cycl  35312  acycgr1v  35331  derangen  35354  subfacval3  35371  cvmseu  35458  cvmliftmolem2  35464  cvmliftlem7  35473  cvmliftlem15  35480  cvmlift2lem9a  35485  cvmlift2lem9  35493  cvmlift2lem10  35494  cvmlift2lem11  35495  cvmlift2lem12  35496  cvmlift3lem6  35506  cvmlift3lem8  35508  ex-sategoelel  35603  ex-sategoelelomsuc  35608  mclsppslem  35765  mclspps  35766  wsuclem  36005  fness  36531  fnetr  36533  fnessref  36539  refssfne  36540  neibastop1  36541  neibastop2  36543  tailfb  36559  filnetlem3  36562  weiunfrlem  36646  bj-finsumval0  37599  bj-rvecvec  37613  dfgcd3  37638  lindsadd  37934  poimirlem13  37954  poimirlem15  37956  poimirlem24  37965  poimirlem28  37969  mblfinlem2  37979  ovoliunnfl  37983  volsupnfl  37986  mbfresfi  37987  iblabsnc  38005  iblmulc2nc  38006  ftc1cnnclem  38012  ftc1cnnc  38013  ftc1anc  38022  sdclem2  38063  metf1o  38076  ismtyhmeolem  38125  ismtyres  38129  heibor1lem  38130  bfplem2  38144  bfp  38145  rrncmslem  38153  iccbnd  38161  icccmpALT  38162  rngogrphom  38292  rngoisoco  38303  keridl  38353  lsmcv2  39475  lsatcv0  39477  lcvexchlem4  39483  lcvexchlem5  39484  l1cvpat  39500  lfl0f  39515  lfladdcl  39517  lflnegcl  39521  lkrlss  39541  eqlkr  39545  lkrlsp  39548  lkrlsp2  39549  lshpkrcl  39562  lkrin  39610  1cvrjat  39921  llni  39954  llnle  39964  lplni  39978  lplnle  39986  llncvrlpln2  40003  2atmat  40007  lvoli  40021  lplncvrlvol2  40061  elpaddri  40248  paddclN  40288  pclclN  40337  pclfinN  40346  0psubclN  40389  1psubclN  40390  atpsubclN  40391  pmapsubclN  40392  osumclN  40413  pexmidN  40415  pexmidlem6N  40421  lhp2lt  40447  lautcnv  40536  idlaut  40542  lautco  40543  idldil  40560  ldilcnv  40561  ldilco  40562  ltrncnv  40592  idltrn  40596  cdleme16d  40727  cdleme50laut  40993  cdleme50ldil  40994  cdleme50ltrn  41003  ltrnco  41165  dian0  41485  dia0eldmN  41486  dia1eldmN  41487  dialss  41492  diaintclN  41504  docaclN  41570  doca2N  41572  djajN  41583  dibintclN  41613  diblss  41616  dicvaddcl  41636  dicvscacl  41637  dicn0  41638  cdlemn11a  41653  dihord2cN  41667  dihord11b  41668  dihord6apre  41702  dihmeetlem1N  41736  dihglblem5apreN  41737  dihpN  41782  dihjatcclem4  41867  dochkr1  41924  islpoldN  41930  lcfrlem31  42019  mapdpglem18  42135  mapdheq2  42175  mapdheq4  42178  mapdh6aN  42181  hdmap1l6a  42255  hdmap14lem4a  42317  lcmineqlem4  42471  frlmfzoccat  42950  drnginvmuld  42972  psrbagres  42989  evlselvlem  43019  evlselv  43020  fsuppind  43023  fsuppssind  43026  prjspvs  43043  irrapxlem4  43253  pell1234qrdich  43289  pell1qr1  43299  pell14qrgap  43303  pellqrexplicit  43305  rmspecfund  43337  fzmaxdif  43409  acongeq  43411  jm2.23  43424  jm3.1  43448  lmhmlnmsplit  43515  hbt  43558  dgrsub2  43563  proot1ex  43624  cantnfub  43749  cantnfresb  43752  cantnf2  43753  tfsconcatfv2  43768  tfsconcatrn  43770  tfsconcatb0  43772  naddcnff  43790  naddcnffo  43792  naddcnfid1  43795  naddcnfid2  43796  clublem  44037  dftrcl3  44147  mnugrud  44711  hashnzfz2  44748  dvconstbi  44761  ubelsupr  45451  restopn3  45581  wessf1ornlem  45615  lefldiveq  45725  iccintsng  45953  climsuse  46038  mullimc  46046  limcdm0  46048  limccog  46050  mullimcf  46053  constlimc  46054  idlimc  46056  limcperiod  46058  limsupre  46069  limcleqr  46072  neglimc  46075  addlimc  46076  0ellimcdiv  46077  xlimliminflimsup  46290  cncfshift  46302  cncfperiod  46307  cncfuni  46314  icccncfext  46315  cncfiooicclem1  46321  fperdvper  46347  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  mbfres2cn  46386  iblsplit  46394  stoweidlem7  46435  stoweidlem13  46441  stoweidlem26  46454  wallispilem3  46495  stirlinglem6  46507  stirlinglem10  46511  dirkercncf  46535  fourierdlem6  46541  fourierdlem11  46546  fourierdlem12  46547  fourierdlem15  46550  fourierdlem26  46561  fourierdlem42  46577  fourierdlem50  46584  fourierdlem51  46585  fourierdlem52  46586  fourierdlem54  46588  fourierdlem62  46596  fourierdlem79  46613  fourierdlem102  46636  fourierdlem114  46648  etransclem23  46685  chnsubseq  47308  3f1oss1  47517  zgeltp1eq  47751  nnmul2  47772  setsnidel  47831  preimafvsnel  47833  iccpartres  47872  prpair  47955  fpprel2  48211  isubgrsubgr  48339  grimidvtxedg  48355  grimcnv  48358  isuspgrim  48366  upgrimpthslem2  48378  stgrnbgr0  48434  uhgrimgrlim  48457  clnbgr3stgrgrlim  48489  gpg5nbgrvtx03starlem2  48539  gpg5nbgrvtx13starlem2  48542  gpg5edgnedg  48600  isassintop  48680  rhmsubcALTV  48755  srhmsubcALTV  48795  fldhmsubcALTV  48803  rmfsupp  48843  scmfsupp  48845  mptcfsupp  48847  lcoel0  48898  lincsumcl  48901  lincscmcl  48902  lcoss  48906  lindsrng01  48938  lincreslvec3  48952  lindssnlvec  48956  zgtp1leeq  48991  lubsscl  49429  glbsscl  49430  idmon  49489  idepi  49490  iinfssc  49526  iinfsubc  49527  discsubc  49533  nelsubclem  49536  imassc  49622  imasubc3  49625  isnatd  49692  swapfiso  49754  fucoppc  49879  thinciso  49939  diagciso  50008  termolmd  50139