Theorem mpbir2and 721

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 518	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 259	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  elpreimad  7025  fveqressseq  7045  fmptsng  7137  fmptsnd  7138  fnprb  7177  fntpb  7178  fpr3g  8250  frrlem4  8254  1ellim  8451  isfsuppd  9298  fdmfifsupp  9307  fsuppmptif  9331  fsuppco2  9335  fsuppcor  9336  dffi3  9363  suppr  9404  infpr  9437  ordtypelem7  9458  cantnf0  9616  cantnfp1lem1  9619  cantnfp1lem2  9620  cantnfp1lem3  9621  cantnflem1a  9626  cantnflem1d  9629  cantnflem1  9630  cantnf  9634  rankpwi  9767  carduni  9925  fin23lem32  10287  fpwwe2lem5  10579  fpwwe2lem11  10585  fpwwe2lem12  10586  fpwwe2  10587  inttsk  10718  grutsk1  10765  add20  11685  supaddc  12145  supadd  12146  supmul  12150  suprzcl  12639  uzid  12840  uzwo3  12930  rpnnen1lem5  12968  xrletrid  13143  xrre  13158  xrre3  13160  xleadd1a  13242  xlemul1a  13277  elioc2  13399  elico2  13400  elicc2  13401  elfz1eq  13526  fzadd2  13550  fznatpl1  13569  elfz1uz  13585  nn0fz0  13616  fzctr  13631  fzo1fzo0n0  13707  fzoaddel  13709  elincfzoext  13715  flid  13804  flval3  13811  fladdz  13821  fldiv  13856  modid  13892  hashf1lem1  14454  pfxccatin12d  14744  repswpfx  14784  2cshw  14812  pfx2  14946  wwlktovf1  14956  sqeqd  15165  01sqrexlem7  15247  max0add  15309  abs2difabs  15334  rddif  15340  fzomaxdiflem  15342  rexico  15353  icodiamlt  15437  limsupgre  15480  rlim3  15497  icco1  15539  rlimclim  15545  rlimuni  15549  rlimresb  15564  isercolllem2  15665  isercolllem3  15666  isercoll  15667  caucvgrlem  15672  caurcvgr  15673  iseraltlem3  15683  fsum00  15798  o1fsum  15813  bitsfzolem  16440  bitsfzo  16441  bitsmod  16442  bitscmp  16444  gcd0id  16525  gcdneg  16528  bezoutlem4  16548  nn0seqcvgd  16576  lcmneg  16609  lcmfunsnlem2lem2  16645  qredeq  16663  prmind2  16691  eulerthlem2  16789  pcpremul  16851  pcidlem  16880  pcgcd1  16885  fldivp1  16905  pcfaclem  16906  4sqlem17  16969  vdwlem1  16989  vdwlem6  16994  vdwlem12  17000  vdwlem13  17001  0ram  17028  ram0  17030  ramub1lem1  17034  invco  17776  sectmon  17787  monsect  17788  invid  17792  ssctr  17830  ssceq  17831  0ssc  17842  0subcat  17843  catsubcat  17844  issubc3  17854  fullsubc  17855  funcinv  17878  fthmon  17934  fuccocl  17972  fucidcl  17973  invfuc  17982  2initoinv  18015  2termoinv  18022  elhomai  18038  setcmon  18092  setcepi  18093  catcisolem  18115  curf2cl  18235  yonedalem4c  18281  yonedalem3  18284  yoniso  18289  lublecl  18363  isacs3lem  18546  tsrdir  18608  chnccat  18630  rabsubmgmd  18710  submgmid  18712  subsubmgm  18716  mgmhmima  18721  mgmhmeql  18722  mndpfsupp  18773  mnd1  18785  sgrp2nmndlem4  18937  sgrp2nmndlem5  18938  0subg  19165  nmznsg  19181  ghmpreima  19250  ghmeql  19251  ghmnsgpreima  19253  kerf1ghm  19259  cntzsgrpcl  19346  cntzsubm  19350  cntzsubg  19351  cntzmhm  19353  symgextfo  19434  symgfixf1  19449  symgfixfolem1  19450  odlem2  19551  finodsubmsubg  19579  gexlem2  19594  gexcl2  19601  sylow1lem5  19614  subgslw  19628  slwhash  19636  fislw  19637  sylow3lem1  19639  lsmsubg  19666  efgredlemd  19756  efgredlem  19759  efgcpbllemb  19767  frgpuplem  19784  cyggeninv  19895  iscygd  19899  iscygodd  19900  gsumzadd  19934  gsumconst  19946  gsumpt  19974  gsum2dlem2  19983  gsum2d  19984  gsum2d2lem  19985  dprdfcntz  20029  eldprdi  20032  subgdmdprd  20048  subgdprd  20049  dprdpr  20064  ablfac1c  20085  ablfac1eu  20087  ablfaclem3  20101  ogrpaddlt  20150  ogrpsublt  20154  ring1  20328  subrngint  20578  rhmimasubrng  20584  cntzsubrng  20585  rhmeql  20621  rhmima  20622  cntzsubr  20624  rnghmsscmap2  20647  rnghmsscmap  20648  rnghmsubcsetc  20651  zrzeroorngc  20662  rhmsscmap2  20676  rhmsscmap  20677  rhmsubcsetc  20680  rhmsscrnghm  20683  rhmsubcrngc  20686  srhmsubc  20698  rhmsubc  20707  issubdrg  20798  fldhmsubc  20803  imadrhmcl  20815  isabvd  20830  abvdiv  20847  ornglmullt  20887  orngrmullt  20888  orngmullt  20889  ofldlt1  20893  lsslsp  21051  lmhmima  21083  lmhmpreima  21084  lmhmeql  21091  lsmcl  21119  lspfixed  21167  rnglidlrng  21286  rngqiprngim  21343  rng2idl1cntr  21344  qsssubdrg  21447  gzrngunit  21454  pzriprnglem8  21509  evpmodpmf1o  21617  ocvpj  21738  dsmm0cl  21761  dsmmacl  21762  dsmmsubg  21764  dsmmlss  21765  frlmsplit2  21794  uvcff  21812  lindfrn  21842  f1lindf  21843  lindsss  21845  issubassa  21888  issubassa2  21913  snifpsrbag  21941  psrbaglesupp  21943  psrbaglecl  21944  psrbagaddcl  21945  psrbagcon  21946  psrbagres  21951  mplsubglem  22019  mpllsslem  22020  mplassa  22042  subrgmpl  22053  mplcoe5  22062  mplbas2  22064  mplind  22092  mpfind  22137  ismhp2  22175  mhpmulcl  22183  mhplss  22189  ply1assa  22230  coe1tmmul2  22308  coe1tmmul  22309  cply1coe0bi  22334  dmatid  22524  dmatsubcl  22527  dmatscmcl  22532  scmatid  22543  scmataddcl  22545  scmatsubcl  22546  scmatmulcl  22547  smatvscl  22553  scmatrhmcl  22557  mat0scmat  22567  mat1scmat  22568  mdet0pr  22621  chmaidscmat  22877  distop  23024  indistopon  23030  ppttop  23036  epttop  23038  mretopd  23121  toponmre  23122  neiss  23138  opnneissb  23143  ssnei2  23145  innei  23154  neiptoptop  23160  ordtcld1  23226  ordtcld2  23227  lmconst  23290  cnpnei  23293  iscncl  23298  cnss1  23305  cnss2  23306  cncnpi  23307  cncnp  23309  cnconst2  23312  cnrest  23314  cnpresti  23317  cnpdis  23322  paste  23323  lmcnp  23333  cnhaus  23383  hauscmp  23436  2ndcomap  23487  1stcelcls  23490  1stccnp  23491  llyrest  23514  nllyrest  23515  llyidm  23517  nllyidm  23518  ssref  23541  reftr  23543  refun0  23544  dissnref  23557  kgentopon  23567  kgenidm  23576  kgencn3  23587  txcld  23632  neitx  23636  tx1cn  23638  tx2cn  23639  ptcld  23642  xkoccn  23648  txcnp  23649  ptcnp  23651  txcnmpt  23653  ptcn  23656  txdis1cn  23664  ptrescn  23668  txkgen  23681  xkoco1cn  23686  xkoco2cn  23687  xkococn  23689  xkoinjcn  23716  qtoptop2  23728  qtopuni  23731  qtopid  23734  qtopkgen  23739  basqtop  23740  tgqtop  23741  qtopss  23744  qtopeu  23745  qtoprest  23746  kqopn  23763  kqcld  23764  kqreglem2  23771  reghmph  23822  ordthmeolem  23830  qtopf1  23845  opnfbas  23871  isfil2  23885  fbasweak  23894  fsubbas  23896  filconn  23912  fbasrn  23913  rnelfmlem  23981  flimss2  24001  flimss1  24002  hausflim  24010  flimclslem  24013  flimsncls  24015  cnpflfi  24028  flfcnp2  24036  fclsfnflim  24056  cnextfvval  24094  cnextfres1  24097  symgtgp  24135  opnsubg  24137  ghmcnp  24144  qustgpopn  24149  qustgplem  24150  qustgphaus  24152  tsmsfbas  24157  ustfilxp  24242  utoptop  24263  utopbas  24264  restutopopn  24267  iducn  24311  cstucnd  24312  ucncn  24313  fmucnd  24320  cfilufg  24321  trcfilu  24322  cfiluweak  24323  neipcfilu  24324  psmetres2  24343  isxmetd  24355  xmetpsmet  24377  imasf1oxmet  24404  xblss2ps  24430  xblss2  24431  xblcntrps  24439  xblcntr  24440  blcld  24534  metustfbas  24586  cfilucfil  24588  restmetu  24599  ngptgp  24665  tngngpd  24682  nrmtngnrm  24687  tngnrg  24703  nlmvscn  24716  nrginvrcn  24721  nmo0  24764  nmoeq0  24765  nmoid  24771  nghmcn  24774  0nmhm  24784  blcvx  24827  iccntr  24851  xrge0tsms  24864  xmetdcn2  24867  metdstri  24881  metdscn  24886  rescncf  24928  cncfco  24938  oprpiece1res2  24983  cnheibor  24986  cnllycmp  24987  bndth  24989  ishtpyd  25006  isphtpyd  25017  pcoval2  25047  nmhmcn  25151  ipcn  25277  lmnn  25294  cfilss  25301  iscfil3  25304  cfilfcls  25305  cmetcaulem  25319  iscmet3lem2  25323  cfilres  25327  lmcau  25344  flimcfil  25345  cncmet  25353  rlmbn  25392  minveclem3b  25459  pjthlem1  25468  pjth2  25471  ivthlem3  25484  ovolssnul  25518  ovolctb  25521  ovoliunnul  25538  ovolsca  25546  ovolicopnf  25555  voliunlem2  25582  volsup  25587  dyadmaxlem  25628  vitalilem5  25643  mbfres  25675  mbfss  25677  mbfmulc2re  25679  mbfadd  25692  mbfmulc2  25694  mbflim  25699  i1faddlem  25724  i1fmullem  25725  mbfmul  25757  itg2mulc  25778  itg2cnlem1  25792  ibl0  25818  iblposlem  25823  itgreval  25828  iblneg  25834  iblss  25836  iblss2  25837  itgle  25841  iblconst  25849  iblabs  25860  iblabsr  25861  iblmulc2  25862  bddmulibl  25870  limciun  25925  limcun  25926  dvres2lem  25941  dvidlem  25946  dvcnp2  25951  dvcn  25952  cpnres  25968  dvaddbr  25969  dvmulbr  25970  dvcobr  25977  dvcjbr  25980  dvrec  25986  dvcnvlem  26007  dvferm  26019  dvlip2  26026  dveq0  26031  dv11cn  26032  dvivthlem1  26039  lhop1  26045  lhop2  26046  lhop  26047  dvcnvre  26050  dvfsumlem3  26059  dvfsumlem4  26060  dvfsumrlim  26062  dvfsum2  26065  ftc1a  26068  ftc1lem4  26070  ftc1lem6  26072  ftc1  26073  coe1mul3  26128  deg1addle2  26131  deg1sublt  26139  fta1blem  26200  drnguc1p  26203  ig1prsp  26210  plyco0  26221  plyeq0lem  26239  dgrub  26263  dgreq  26273  dgradd2  26297  dgrmul  26299  dgrcolem2  26303  dgrco  26304  plycpn  26319  plydivlem4  26326  plydiveu  26328  vieta1lem2  26341  vieta1  26342  aalioulem2  26363  aalioulem3  26364  aaliou3lem7  26379  tayl0  26391  ulmcn  26428  ulmdvlem3  26431  psercn  26455  abelth  26470  pilem3  26482  efif1olem1  26573  abslogimle  26604  argregt0  26641  argrege0  26642  logf1o2  26681  cxpsqrtlem  26733  cxpcn3  26779  abscxpbnd  26784  logreclem  26793  ang180lem2  26841  ang180lem3  26842  xrlimcnp  26999  harmonicbnd4  27041  fsumharmonic  27042  lgamgulmlem5  27063  lgambdd  27067  basellem4  27114  dvdsppwf1o  27216  dvdsflf1o  27217  fsumfldivdiaglem  27219  chpeq0  27238  chteq0  27239  chtub  27242  chpub  27250  dchrelbasd  27269  dchrmulcl  27279  dchrinv  27291  bposlem1  27314  bposlem2  27315  lgsdirprm  27361  lgsqrlem2  27377  lgsqrlem3  27378  lgsdchr  27385  lgseisenlem1  27405  lgseisenlem2  27406  lgseisenlem3  27407  lgsquadlem1  27410  2sqlem8  27456  2sqblem  27461  2sqmod  27466  chebbnd1lem1  27499  dchrisumlem1  27519  dchrisumlem2  27520  dchrisumlem3  27521  dchrisum0fno1  27541  pntrmax  27594  pntpbnd1a  27615  pntibndlem3  27622  pntlemn  27630  pntlemi  27634  pntlem3  27639  pntleml  27641  ostth1  27663  ostth2  27667  ostth3  27668  nosepon  27695  nolesgn2ores  27702  nogesgn1ores  27704  nosupres  27737  nosupbnd1lem2  27739  nosupbnd2lem1  27745  noinfres  27752  noinfbnd1lem2  27754  noinfbnd2lem1  27760  eqcuts3  27863  cofcutrtime  27986  divmuldivsd  28291  divdivs1d  28292  onsbnd  28340  nnsgt0  28398  bdayfinbndlem1  28526  ercgrg  28652  motco  28675  cnvmot  28676  legso  28734  mirmot  28810  colopp  28904  hphl  28906  lmicom  28923  lmimid  28929  lmimot  28933  hypcgrlem1  28934  hypcgrlem2  28935  trgcopyeulem  28940  inagswap  28976  inaghl  28980  cgrg3col4  28988  brbtwn2  29041  axlowdimlem3  29080  axlowdimlem16  29093  axcontlem8  29107  fusgrfis  29466  nbgr2vtx1edg  29486  0vtxrgr  29712  0vtxrusgr  29713  ewlkle  29741  wlk1ewlk  29775  uspgr2wlkeq2  29782  wlkp1lem8  29814  trlontrl  29844  pthonpth  29883  pthdlem2  29903  wlklnwwlkln1  30003  wlknewwlksn  30022  wwlksnred  30027  wwlksnredwwlkn0  30031  2trlond  30074  2pthond  30077  elwwlks2ons3im  30089  clwlkclwwlklem2a1  30129  clwlkclwwlkf1  30147  clwwlkel  30183  clwwlkwwlksb  30191  wwlksext2clwwlk  30194  1ewlk  30252  0trlon  30261  0pthon  30264  1pthond  30281  3trlond  30310  3pthond  30312  3spthond  30314  eupthres  30352  2clwwlk2clwwlk  30487  numclwwlk1lem2foa  30491  numclwwlk1lem2f1  30494  nvabs  30810  vacn  30832  nmcvcn  30833  nmblore  30924  0lno  30928  0blo  30930  nmlno0lem  30931  occl  31442  pjhthlem1  31529  pjpjpre  31557  nmopre  32008  nmlnop0iALT  32133  nmophmi  32169  leoprf2  32265  stlesi  32379  disjdifprg  32713  disjun0  32733  fsuppcurry1  32865  fsuppcurry2  32866  fpwrelmap  32874  fzspl  32930  dfmgc2lem  33123  pwrssmgc  33128  xrge0tsmsd  33203  psgnfzto1stlem  33230  fzto1st1  33232  evpmid  33278  pnfinf  33313  isarchiofld  33329  rmfsupp2  33368  fracfld  33441  dvdsruassoi  33516  nsgmgc  33544  drngidl  33565  qsdrngi  33627  deg1addlt  33740  ply1degltdimlem  33863  lbsdiflsp0  33867  fedgmul  33872  fldexttr  33899  fldextid  33900  irngnzply1lem  33931  finextalg  33939  minplyelirng  33956  irredminply  33957  algextdeglem8  33965  rtelextdg2lem  33967  constrsslem  33982  constrllcllem  33993  constrlccllem  33994  constrcccllem  33995  qtopt1  34076  reff  34080  locfinreflem  34081  metideq  34134  metider  34135  pstmxmet  34138  qqhval2lem  34222  qqhcn  34232  qqhucn  34233  pwsiga  34371  prsiga  34372  measle0  34449  mbfmcst  34500  1stmbfm  34501  2ndmbfm  34502  imambfm  34503  cnmbfm  34504  mbfmco  34505  mbfmco2  34506  0elcarsg  34548  carsgclctun  34562  sibfof  34581  oddpwdc  34595  eulerpartlemmf  34616  eulerpartlemgs2  34621  0rrv  34692  ballotlemfc0  34734  ballotlemfcc  34735  signstfveq0  34818  breprexplemc  34873  bnj1452  35294  usgrgt2cycl  35418  acycgr1v  35437  derangen  35460  subfacval3  35477  cvmseu  35564  cvmliftmolem2  35570  cvmliftlem7  35579  cvmliftlem15  35586  cvmlift2lem9a  35591  cvmlift2lem9  35599  cvmlift2lem10  35600  cvmlift2lem11  35601  cvmlift2lem12  35602  cvmlift3lem6  35612  cvmlift3lem8  35614  ex-sategoelel  35709  ex-sategoelelomsuc  35714  mclsppslem  35871  mclspps  35872  wsuclem  36111  fness  36647  fnetr  36649  fnessref  36655  refssfne  36656  neibastop1  36657  neibastop2  36659  tailfb  36675  filnetlem3  36678  weiunfrlem  36762  bj-finsumval0  37715  bj-rvecvec  37729  dfgcd3  37754  lindsadd  38050  poimirlem13  38070  poimirlem15  38072  poimirlem24  38081  poimirlem28  38085  mblfinlem2  38095  ovoliunnfl  38099  volsupnfl  38102  mbfresfi  38103  iblabsnc  38121  iblmulc2nc  38122  ftc1cnnclem  38128  ftc1cnnc  38129  ftc1anc  38138  sdclem2  38179  metf1o  38192  ismtyhmeolem  38241  ismtyres  38245  heibor1lem  38246  bfplem2  38260  bfp  38261  rrncmslem  38269  iccbnd  38277  icccmpALT  38278  rngogrphom  38408  rngoisoco  38419  keridl  38469  lsmcv2  39591  lsatcv0  39593  lcvexchlem4  39599  lcvexchlem5  39600  l1cvpat  39616  lfl0f  39631  lfladdcl  39633  lflnegcl  39637  lkrlss  39657  eqlkr  39661  lkrlsp  39664  lkrlsp2  39665  lshpkrcl  39678  lkrin  39726  1cvrjat  40037  llni  40070  llnle  40080  lplni  40094  lplnle  40102  llncvrlpln2  40119  2atmat  40123  lvoli  40137  lplncvrlvol2  40177  elpaddri  40364  paddclN  40404  pclclN  40453  pclfinN  40462  0psubclN  40505  1psubclN  40506  atpsubclN  40507  pmapsubclN  40508  osumclN  40529  pexmidN  40531  pexmidlem6N  40537  lhp2lt  40563  lautcnv  40652  idlaut  40658  lautco  40659  idldil  40676  ldilcnv  40677  ldilco  40678  ltrncnv  40708  idltrn  40712  cdleme16d  40843  cdleme50laut  41109  cdleme50ldil  41110  cdleme50ltrn  41119  ltrnco  41281  dian0  41601  dia0eldmN  41602  dia1eldmN  41603  dialss  41608  diaintclN  41620  docaclN  41686  doca2N  41688  djajN  41699  dibintclN  41729  diblss  41732  dicvaddcl  41752  dicvscacl  41753  dicn0  41754  cdlemn11a  41769  dihord2cN  41783  dihord11b  41784  dihord6apre  41818  dihmeetlem1N  41852  dihglblem5apreN  41853  dihpN  41898  dihjatcclem4  41983  dochkr1  42040  islpoldN  42046  lcfrlem31  42135  mapdpglem18  42251  mapdheq2  42291  mapdheq4  42294  mapdh6aN  42297  hdmap1l6a  42371  hdmap14lem4a  42433  lcmineqlem4  42587  frlmfzoccat  43065  drnginvmuld  43083  evlselvlem  43108  evlselv  43109  fsuppind  43110  fsuppssind  43113  prjspvs  43130  irrapxlem4  43340  pell1234qrdich  43376  pell1qr1  43386  pell14qrgap  43390  pellqrexplicit  43392  rmspecfund  43424  fzmaxdif  43496  acongeq  43498  jm2.23  43511  jm3.1  43535  lmhmlnmsplit  43602  hbt  43645  dgrsub2  43650  proot1ex  43711  cantnfub  43836  cantnfresb  43839  cantnf2  43840  tfsconcatfv2  43855  tfsconcatrn  43857  tfsconcatb0  43859  naddcnff  43877  naddcnffo  43879  naddcnfid1  43882  naddcnfid2  43883  clublem  44124  dftrcl3  44234  mnugrud  44798  hashnzfz2  44835  dvconstbi  44848  ubelsupr  45538  restopn3  45667  wessf1ornlem  45701  lefldiveq  45809  iccintsng  46037  climsuse  46122  mullimc  46130  limcdm0  46132  limccog  46134  mullimcf  46137  constlimc  46138  idlimc  46140  limcperiod  46142  limsupre  46153  limcleqr  46156  neglimc  46159  addlimc  46160  0ellimcdiv  46161  xlimliminflimsup  46374  cncfshift  46386  cncfperiod  46391  cncfuni  46398  icccncfext  46399  cncfiooicclem1  46405  fperdvper  46431  ioodvbdlimc1lem2  46444  ioodvbdlimc2lem  46446  mbfres2cn  46470  iblsplit  46478  stoweidlem7  46519  stoweidlem13  46525  stoweidlem26  46538  wallispilem3  46579  stirlinglem6  46591  stirlinglem10  46595  dirkercncf  46619  fourierdlem6  46625  fourierdlem11  46630  fourierdlem12  46631  fourierdlem15  46634  fourierdlem26  46645  fourierdlem42  46661  fourierdlem50  46668  fourierdlem51  46669  fourierdlem52  46670  fourierdlem54  46672  fourierdlem62  46680  fourierdlem79  46697  fourierdlem102  46720  fourierdlem114  46732  etransclem23  46769  chnsubseq  47394  3f1oss1  47607  zgeltp1eq  47841  nnmul2  47862  setsnidel  47921  preimafvsnel  47923  iccpartres  47962  prpair  48045  fpprel2  48301  isubgrsubgr  48429  grimidvtxedg  48445  grimcnv  48448  isuspgrim  48456  upgrimpthslem2  48468  stgrnbgr0  48524  uhgrimgrlim  48547  clnbgr3stgrgrlim  48579  gpg5nbgrvtx03starlem2  48629  gpg5nbgrvtx13starlem2  48632  gpg5edgnedg  48690  isassintop  48770  rhmsubcALTV  48845  srhmsubcALTV  48885  fldhmsubcALTV  48893  rmfsupp  48933  scmfsupp  48935  mptcfsupp  48937  lcoel0  48988  lincsumcl  48991  lincscmcl  48992  lcoss  48996  lindsrng01  49028  lincreslvec3  49042  lindssnlvec  49046  zgtp1leeq  49081  lubsscl  49519  glbsscl  49520  idmon  49579  idepi  49580  iinfssc  49616  iinfsubc  49617  discsubc  49623  nelsubclem  49626  imassc  49712  imasubc3  49715  isnatd  49782  swapfiso  49844  fucoppc  49969  thinciso  50029  diagciso  50098  termolmd  50229