Theorem mpbir2and 725

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  elpreimad  7054  fveqressseq  7074  fmptsng  7166  fmptsnd  7167  fnprb  7206  fntpb  7207  fpr3g  8280  frrlem4  8284  1ellim  8481  isfsuppd  9324  fdmfifsupp  9333  fsuppmptif  9357  fsuppco2  9361  fsuppcor  9362  dffi3  9389  suppr  9430  infpr  9463  ordtypelem7  9484  cantnf0  9642  cantnfp1lem1  9645  cantnfp1lem2  9646  cantnfp1lem3  9647  cantnflem1a  9652  cantnflem1d  9655  cantnflem1  9656  cantnf  9660  rankpwi  9793  carduni  9974  fin23lem32  10334  fpwwe2lem5  10626  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwe2  10634  inttsk  10765  grutsk1  10812  add20  11732  supaddc  12188  supadd  12189  supmul  12193  suprzcl  12682  uzid  12883  uzwo3  12973  rpnnen1lem5  13011  xrletrid  13186  xrre  13201  xrre3  13203  xleadd1a  13285  xlemul1a  13320  elioc2  13442  elico2  13443  elicc2  13444  elfz1eq  13569  fzadd2  13594  fznatpl1  13613  elfz1uz  13629  nn0fz0  13660  fzctr  13675  fzo1fzo0n0  13751  fzoaddel  13753  elincfzoext  13759  flid  13848  flval3  13855  fladdz  13865  fldiv  13900  modid  13936  hashf1lem1  14499  pfxccatin12d  14789  repswpfx  14829  2cshw  14857  pfx2  14991  wwlktovf1  15001  sqeqd  15224  01sqrexlem7  15306  max0add  15368  abs2difabs  15393  rddif  15399  fzomaxdiflem  15401  rexico  15412  icodiamlt  15496  limsupgre  15539  rlim3  15556  icco1  15598  rlimclim  15604  rlimuni  15608  rlimresb  15623  isercolllem2  15724  isercolllem3  15725  isercoll  15726  caucvgrlem  15731  caurcvgr  15732  iseraltlem3  15742  fsum00  15857  o1fsum  15872  bitsfzolem  16498  bitsfzo  16499  bitsmod  16500  bitscmp  16502  gcd0id  16583  gcdneg  16586  bezoutlem4  16606  nn0seqcvgd  16634  lcmneg  16667  lcmfunsnlem2lem2  16703  qredeq  16721  prmind2  16749  eulerthlem2  16847  pcpremul  16909  pcidlem  16938  pcgcd1  16943  fldivp1  16963  pcfaclem  16964  4sqlem17  17027  vdwlem1  17047  vdwlem6  17052  vdwlem12  17058  vdwlem13  17059  0ram  17086  ram0  17088  ramub1lem1  17092  invco  17834  sectmon  17845  monsect  17846  invid  17850  ssctr  17888  ssceq  17889  0ssc  17900  0subcat  17901  catsubcat  17902  issubc3  17912  fullsubc  17913  funcinv  17936  fthmon  17992  fuccocl  18030  fucidcl  18031  invfuc  18040  2initoinv  18073  2termoinv  18080  elhomai  18096  setcmon  18150  setcepi  18151  catcisolem  18173  curf2cl  18293  yonedalem4c  18339  yonedalem3  18342  yoniso  18347  lublecl  18421  isacs3lem  18604  tsrdir  18666  chnccat  18688  rabsubmgmd  18768  submgmid  18770  subsubmgm  18774  mgmhmima  18779  mgmhmeql  18780  mndpfsupp  18831  mnd1  18843  sgrp2nmndlem4  18996  sgrp2nmndlem5  18997  0subg  19224  nmznsg  19240  ghmpreima  19314  ghmeql  19315  ghmnsgpreima  19317  kerf1ghm  19323  cntzsgrpcl  19410  cntzsubm  19414  cntzsubg  19415  cntzmhm  19417  symgextfo  19498  symgfixf1  19513  symgfixfolem1  19514  odlem2  19615  finodsubmsubg  19643  gexlem2  19658  gexcl2  19665  sylow1lem5  19678  subgslw  19692  slwhash  19700  fislw  19701  sylow3lem1  19703  lsmsubg  19730  efgredlemd  19820  efgredlem  19823  efgcpbllemb  19831  frgpuplem  19848  cyggeninv  19959  iscygd  19963  iscygodd  19964  gsumzadd  19998  gsumconst  20010  gsumpt  20038  gsum2dlem2  20047  gsum2d  20048  gsum2d2lem  20049  dprdfcntz  20093  eldprdi  20096  subgdmdprd  20112  subgdprd  20113  dprdpr  20128  ablfac1c  20149  ablfac1eu  20151  ablfaclem3  20165  ogrpaddlt  20214  ogrpsublt  20218  ring1  20400  subrngint  20670  rhmimasubrng  20676  cntzsubrng  20677  rhmeql  20713  rhmima  20714  cntzsubr  20716  rnghmsscmap2  20739  rnghmsscmap  20740  rnghmsubcsetc  20743  zrzeroorngc  20754  rhmsscmap2  20768  rhmsscmap  20769  rhmsubcsetc  20772  rhmsscrnghm  20775  rhmsubcrngc  20778  srhmsubc  20790  rhmsubc  20799  issubdrg  20894  fldhmsubc  20899  imadrhmcl  20911  isabvd  20926  abvdiv  20943  ornglmullt  20983  orngrmullt  20984  orngmullt  20985  ofldlt1  20989  lsslsp  21147  lmhmima  21179  lmhmpreima  21180  lmhmeql  21187  lsmcl  21215  lspfixed  21263  rnglidlrng  21392  drngidl  21396  rngqiprngim  21455  rng2idl1cntr  21456  qsssubdrg  21587  gzrngunit  21594  pzriprnglem8  21649  evpmodpmf1o  21757  ocvpj  21878  dsmm0cl  21901  dsmmacl  21902  dsmmsubg  21904  dsmmlss  21905  frlmsplit2  21934  uvcff  21952  lindfrn  21982  f1lindf  21983  lindsss  21985  issubassa  22028  issubassa2  22053  snifpsrbag  22081  psrbaglesupp  22083  psrbaglecl  22084  psrbagaddcl  22085  psrbagcon  22086  psrbagres  22091  mplsubglem  22159  mpllsslem  22160  mplassa  22182  subrgmpl  22193  mplcoe5  22202  mplbas2  22204  mplind  22232  mpfind  22277  ismhp2  22315  mhpmulcl  22323  mhplss  22329  ply1assa  22370  coe1tmmul2  22448  coe1tmmul  22449  cply1coe0bi  22473  dmatid  22663  dmatsubcl  22666  dmatscmcl  22671  scmatid  22682  scmataddcl  22684  scmatsubcl  22685  scmatmulcl  22686  smatvscl  22692  scmatrhmcl  22696  mat0scmat  22706  mat1scmat  22707  mdet0pr  22760  chmaidscmat  23016  distop  23163  indistopon  23169  ppttop  23175  epttop  23177  mretopd  23260  toponmre  23261  neiss  23277  opnneissb  23282  ssnei2  23284  innei  23293  neiptoptop  23299  ordtcld1  23365  ordtcld2  23366  lmconst  23429  cnpnei  23432  iscncl  23437  cnss1  23444  cnss2  23445  cncnpi  23446  cncnp  23448  cnconst2  23451  cnrest  23453  cnpresti  23456  cnpdis  23461  paste  23462  lmcnp  23472  cnhaus  23522  hauscmp  23575  2ndcomap  23626  1stcelcls  23629  1stccnp  23630  llyrest  23653  nllyrest  23654  llyidm  23656  nllyidm  23657  ssref  23680  reftr  23682  refun0  23683  dissnref  23696  kgentopon  23706  kgenidm  23715  kgencn3  23726  txcld  23771  neitx  23775  tx1cn  23777  tx2cn  23778  ptcld  23781  xkoccn  23787  txcnp  23788  ptcnp  23790  txcnmpt  23792  ptcn  23795  txdis1cn  23803  ptrescn  23807  txkgen  23820  xkoco1cn  23825  xkoco2cn  23826  xkococn  23828  xkoinjcn  23855  qtoptop2  23867  qtopuni  23870  qtopid  23873  qtopkgen  23878  basqtop  23879  tgqtop  23880  qtopss  23883  qtopeu  23884  qtoprest  23885  kqopn  23902  kqcld  23903  kqreglem2  23910  reghmph  23961  ordthmeolem  23969  qtopf1  23984  opnfbas  24010  isfil2  24024  fbasweak  24033  fsubbas  24035  filconn  24051  fbasrn  24052  rnelfmlem  24120  flimss2  24140  flimss1  24141  hausflim  24149  flimclslem  24152  flimsncls  24154  cnpflfi  24167  flfcnp2  24175  fclsfnflim  24195  cnextfvval  24233  cnextfres1  24236  symgtgp  24274  opnsubg  24276  ghmcnp  24283  qustgpopn  24288  qustgplem  24289  qustgphaus  24291  tsmsfbas  24296  ustfilxp  24381  utoptop  24402  utopbas  24403  restutopopn  24406  iducn  24450  cstucnd  24451  ucncn  24452  fmucnd  24459  cfilufg  24460  trcfilu  24461  cfiluweak  24462  neipcfilu  24463  psmetres2  24482  isxmetd  24494  xmetpsmet  24516  imasf1oxmet  24543  xblss2ps  24569  xblss2  24570  xblcntrps  24578  xblcntr  24579  blcld  24673  metustfbas  24725  cfilucfil  24727  restmetu  24738  ngptgp  24804  tngngpd  24821  nrmtngnrm  24826  tngnrg  24842  nlmvscn  24855  nrginvrcn  24860  nmo0  24903  nmoeq0  24904  nmoid  24910  nghmcn  24913  0nmhm  24923  blcvx  24966  iccntr  24990  xrge0tsms  25003  xmetdcn2  25006  metdstri  25020  metdscn  25025  rescncf  25067  cncfco  25077  oprpiece1res2  25122  cnheibor  25125  cnllycmp  25126  bndth  25128  ishtpyd  25145  isphtpyd  25156  pcoval2  25186  nmhmcn  25290  ipcn  25416  lmnn  25433  cfilss  25440  iscfil3  25443  cfilfcls  25444  cmetcaulem  25458  iscmet3lem2  25462  cfilres  25466  lmcau  25483  flimcfil  25484  cncmet  25492  rlmbn  25531  minveclem3b  25598  pjthlem1  25607  pjth2  25610  ivthlem3  25623  ovolssnul  25657  ovolctb  25660  ovoliunnul  25677  ovolsca  25685  ovolicopnf  25694  voliunlem2  25721  volsup  25726  dyadmaxlem  25767  vitalilem5  25782  mbfres  25814  mbfss  25816  mbfmulc2re  25818  mbfadd  25831  mbfmulc2  25833  mbflim  25838  i1faddlem  25863  i1fmullem  25864  mbfmul  25896  itg2mulc  25917  itg2cnlem1  25931  ibl0  25957  iblposlem  25962  itgreval  25967  iblneg  25973  iblss  25975  iblss2  25976  itgle  25980  iblconst  25988  iblabs  25999  iblabsr  26000  iblmulc2  26001  bddmulibl  26009  limciun  26064  limcun  26065  dvres2lem  26080  dvidlem  26085  dvcnp2  26090  dvcn  26091  cpnres  26107  dvaddbr  26108  dvmulbr  26109  dvcobr  26116  dvcjbr  26119  dvrec  26125  dvcnvlem  26146  dvferm  26158  dvlip2  26165  dveq0  26170  dv11cn  26171  dvivthlem1  26178  lhop1  26184  lhop2  26185  lhop  26186  dvcnvre  26189  dvfsumlem3  26198  dvfsumlem4  26199  dvfsumrlim  26201  dvfsum2  26204  ftc1a  26207  ftc1lem4  26209  ftc1lem6  26211  ftc1  26212  coe1mul3  26267  deg1addle2  26270  deg1sublt  26278  fta1blem  26339  drnguc1p  26342  ig1prsp  26349  plyco0  26360  plyeq0lem  26378  dgrub  26402  dgreq  26412  dgradd2  26436  dgrmul  26438  dgrcolem2  26442  dgrco  26443  plycpn  26461  plydivlem4  26468  plydiveu  26470  vieta1lem2  26483  vieta1  26484  aalioulem2  26507  aalioulem3  26508  aaliou3lem7  26523  tayl0  26536  ulmcn  26573  ulmdvlem3  26576  psercn  26600  abelth  26615  pilem3  26627  efif1olem1  26718  abslogimle  26749  argregt0  26786  argrege0  26787  logf1o2  26826  cxpsqrtlem  26878  cxpcn3  26924  abscxpbnd  26929  logreclem  26938  ang180lem2  26986  ang180lem3  26987  xrlimcnp  27144  harmonicbnd4  27186  fsumharmonic  27187  lgamgulmlem5  27208  lgambdd  27212  basellem4  27259  dvdsppwf1o  27361  dvdsflf1o  27362  fsumfldivdiaglem  27364  chpeq0  27383  chteq0  27384  chtub  27387  chpub  27395  dchrelbasd  27414  dchrmulcl  27424  dchrinv  27436  bposlem1  27459  bposlem2  27460  lgsdirprm  27506  lgsqrlem2  27522  lgsqrlem3  27523  lgsdchr  27530  lgseisenlem1  27550  lgseisenlem2  27551  lgseisenlem3  27552  lgsquadlem1  27555  2sqlem8  27601  2sqblem  27606  2sqmod  27611  chebbnd1lem1  27644  dchrisumlem1  27664  dchrisumlem2  27665  dchrisumlem3  27666  dchrisum0fno1  27686  pntrmax  27739  pntpbnd1a  27760  pntibndlem3  27767  pntlemn  27775  pntlemi  27779  pntlem3  27784  pntleml  27786  ostth1  27808  ostth2  27812  ostth3  27813  nosepon  27840  nolesgn2ores  27847  nogesgn1ores  27849  nosupres  27882  nosupbnd1lem2  27884  nosupbnd2lem1  27890  noinfres  27897  noinfbnd1lem2  27899  noinfbnd2lem1  27905  eqcuts3  28008  cofcutrtime  28131  divmuldivsd  28436  divdivs1d  28437  onsbnd  28485  nnsgt0  28543  bdayfinbndlem1  28671  ercgrg  28797  motco  28820  cnvmot  28821  legso  28879  mirmot  28963  colopp  29062  hphl  29064  lmicom  29108  lmimid  29114  lmimot  29118  hypcgrlem1  29120  hypcgrlem2  29121  trgcopyeulem  29127  inagswap  29169  inaghl  29173  cgrg3col4  29181  prlngd  29200  prlngref  29201  dfprlng2  29208  brbtwn2  29266  axlowdimlem3  29305  axlowdimlem16  29318  axcontlem8  29332  fusgrfis  29691  nbgr2vtx1edg  29711  0vtxrgr  29937  0vtxrusgr  29938  ewlkle  29966  wlk1ewlk  30000  uspgr2wlkeq2  30007  wlkp1lem8  30039  trlontrl  30069  pthonpth  30108  pthdlem2  30128  wlklnwwlkln1  30228  wlknewwlksn  30247  wwlksnred  30252  wwlksnredwwlkn0  30256  2trlond  30299  2pthond  30302  elwwlks2ons3im  30314  clwlkclwwlklem2a1  30354  clwlkclwwlkf1  30372  clwwlkel  30408  clwwlkwwlksb  30416  wwlksext2clwwlk  30419  1ewlk  30477  0trlon  30486  0pthon  30489  1pthond  30506  3trlond  30535  3pthond  30537  3spthond  30539  eupthres  30577  2clwwlk2clwwlk  30712  numclwwlk1lem2foa  30716  numclwwlk1lem2f1  30719  nvabs  31035  vacn  31057  nmcvcn  31058  nmblore  31149  0lno  31153  0blo  31155  nmlno0lem  31156  occl  31667  pjhthlem1  31754  pjpjpre  31782  nmopre  32233  nmlnop0iALT  32358  nmophmi  32394  leoprf2  32490  stlesi  32604  disjdifprg  32931  disjun0  32951  fsuppcurry1  33080  fsuppcurry2  33081  fpwrelmap  33089  fzspl  33145  dfmgc2lem  33324  pwrssmgc  33329  xrge0tsmsd  33402  psgnfzto1stlem  33429  fzto1st1  33431  evpmid  33477  pnfinf  33512  isarchiofld  33528  rmfsupp2  33566  fracfld  33638  dvdsruassoi  33706  nsgmgc  33730  qsdrngi  33786  deg1addlt  33899  ply1degltdimlem  34021  lbsdiflsp0  34025  fedgmul  34030  fldexttr  34057  fldextid  34058  irngnzply1lem  34089  finextalg  34097  minplyelirng  34114  irredminply  34115  algextdeglem8  34123  rtelextdg2lem  34125  constrsslem  34140  constrllcllem  34151  constrlccllem  34152  constrcccllem  34153  qtopt1  34234  reff  34238  locfinreflem  34239  metideq  34292  metider  34293  pstmxmet  34296  qqhval2lem  34380  qqhcn  34390  qqhucn  34391  pwsiga  34529  prsiga  34530  measle0  34607  mbfmcst  34658  1stmbfm  34659  2ndmbfm  34660  imambfm  34661  cnmbfm  34662  mbfmco  34663  mbfmco2  34664  0elcarsg  34706  carsgclctun  34720  sibfof  34739  oddpwdc  34753  eulerpartlemmf  34774  eulerpartlemgs2  34779  0rrv  34850  ballotlemfc0  34892  ballotlemfcc  34893  signstfveq0  34973  breprexplemc  35028  bnj1452  35449  usgrgt2cycl  35630  acycgr1v  35649  derangen  35672  subfacval3  35689  cvmseu  35776  cvmliftmolem2  35782  cvmliftlem7  35791  cvmliftlem15  35798  cvmlift2lem9a  35803  cvmlift2lem9  35811  cvmlift2lem10  35812  cvmlift2lem11  35813  cvmlift2lem12  35814  cvmlift3lem6  35824  cvmlift3lem8  35826  ex-sategoelel  35921  ex-sategoelelomsuc  35926  mclsppslem  36083  mclspps  36084  wsuclem  36323  nadddilem2  36721  fness  36888  fnetr  36890  fnessref  36896  refssfne  36897  neibastop1  36898  neibastop2  36900  tailfb  36916  filnetlem3  36919  weiunfrlem  37003  bj-finsumval0  37957  bj-rvecvec  37971  dfgcd3  37996  lindsadd  38292  poimirlem13  38312  poimirlem15  38314  poimirlem24  38323  poimirlem28  38327  mblfinlem2  38337  ovoliunnfl  38341  volsupnfl  38344  mbfresfi  38345  iblabsnc  38363  iblmulc2nc  38364  ftc1cnnclem  38370  ftc1cnnc  38371  ftc1anc  38380  sdclem2  38421  metf1o  38434  ismtyhmeolem  38483  ismtyres  38487  heibor1lem  38488  bfplem2  38502  bfp  38503  rrncmslem  38511  iccbnd  38519  icccmpALT  38520  rngogrphom  38650  rngoisoco  38661  keridl  38711  lsmcv2  39831  lsatcv0  39833  lcvexchlem4  39839  lcvexchlem5  39840  l1cvpat  39856  lfl0f  39871  lfladdcl  39873  lflnegcl  39877  lkrlss  39897  eqlkr  39901  lkrlsp  39904  lkrlsp2  39905  lshpkrcl  39918  lkrin  39966  1cvrjat  40277  llni  40310  llnle  40320  lplni  40334  lplnle  40342  llncvrlpln2  40359  2atmat  40363  lvoli  40377  lplncvrlvol2  40417  elpaddri  40604  paddclN  40644  pclclN  40693  pclfinN  40702  0psubclN  40745  1psubclN  40746  atpsubclN  40747  pmapsubclN  40748  osumclN  40769  pexmidN  40771  pexmidlem6N  40777  lhp2lt  40803  lautcnv  40892  idlaut  40898  lautco  40899  idldil  40916  ldilcnv  40917  ldilco  40918  ltrncnv  40948  idltrn  40952  cdleme16d  41083  cdleme50laut  41349  cdleme50ldil  41350  cdleme50ltrn  41359  ltrnco  41521  dian0  41841  dia0eldmN  41842  dia1eldmN  41843  dialss  41848  diaintclN  41860  docaclN  41926  doca2N  41928  djajN  41939  dibintclN  41969  diblss  41972  dicvaddcl  41992  dicvscacl  41993  dicn0  41994  cdlemn11a  42009  dihord2cN  42023  dihord11b  42024  dihord6apre  42058  dihmeetlem1N  42092  dihglblem5apreN  42093  dihpN  42138  dihjatcclem4  42223  dochkr1  42280  islpoldN  42286  lcfrlem31  42375  mapdpglem18  42491  mapdheq2  42531  mapdheq4  42534  mapdh6aN  42537  hdmap1l6a  42611  hdmap14lem4a  42673  lcmineqlem4  42827  frlmfzoccat  43307  drnginvmuld  43323  evlselvlem  43348  evlselv  43349  fsuppind  43350  fsuppssind  43353  prjspvs  43370  irrapxlem4  43580  pell1234qrdich  43616  pell1qr1  43626  pell14qrgap  43630  pellqrexplicit  43632  rmspecfund  43664  fzmaxdif  43736  acongeq  43738  jm2.23  43751  jm3.1  43775  lmhmlnmsplit  43842  hbt  43885  dgrsub2  43890  proot1ex  43951  cantnfub  44076  cantnfresb  44079  cantnf2  44080  tfsconcatfv2  44095  tfsconcatrn  44097  tfsconcatb0  44099  naddcnff  44117  naddcnffo  44119  naddcnfid1  44122  naddcnfid2  44123  clublem  44364  dftrcl3  44474  mnugrud  45022  hashnzfz2  45059  dvconstbi  45072  ubelsupr  45768  restopn3  45897  wessf1ornlem  45931  lefldiveq  46039  iccintsng  46267  climsuse  46352  mullimc  46360  limcdm0  46362  limccog  46364  mullimcf  46367  constlimc  46368  idlimc  46370  limcperiod  46372  limsupre  46383  limcleqr  46386  neglimc  46389  addlimc  46390  0ellimcdiv  46391  xlimliminflimsup  46604  cncfshift  46616  cncfperiod  46621  cncfuni  46628  icccncfext  46629  cncfiooicclem1  46635  fperdvper  46661  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  mbfres2cn  46700  iblsplit  46708  stoweidlem7  46749  stoweidlem13  46755  stoweidlem26  46768  wallispilem3  46809  stirlinglem6  46821  stirlinglem10  46825  dirkercncf  46849  fourierdlem6  46855  fourierdlem11  46860  fourierdlem12  46861  fourierdlem15  46864  fourierdlem26  46875  fourierdlem42  46891  fourierdlem50  46898  fourierdlem51  46899  fourierdlem52  46900  fourierdlem54  46902  fourierdlem62  46910  fourierdlem79  46927  fourierdlem102  46950  fourierdlem114  46962  etransclem23  46999  chnsubseq  47624  3f1oss1  47840  zgeltp1eq  48074  nnmul2  48095  setsnidel  48154  preimafvsnel  48156  iccpartres  48195  prpair  48278  fpprel2  48534  isubgrsubgr  48662  grimidvtxedg  48678  grimcnv  48681  isuspgrim  48689  upgrimpthslem2  48701  stgrnbgr0  48757  uhgrimgrlim  48780  clnbgr3stgrgrlim  48812  gpg5nbgrvtx03starlem2  48862  gpg5nbgrvtx13starlem2  48865  gpg5edgnedg  48923  isassintop  49003  rhmsubcALTV  49078  srhmsubcALTV  49118  fldhmsubcALTV  49126  rmfsupp  49181  scmfsupp  49183  mptcfsupp  49185  lcoel0  49236  lincsumcl  49239  lincscmcl  49240  lcoss  49244  lindsrng01  49276  lincreslvec3  49290  lindssnlvec  49294  zgtp1leeq  49329  lubsscl  49766  glbsscl  49767  idmon  49826  idepi  49827  iinfssc  49863  iinfsubc  49864  discsubc  49870  nelsubclem  49873  imassc  49959  imasubc3  49962  isnatd  50029  swapfiso  50091  fucoppc  50216  thinciso  50276  diagciso  50345  termolmd  50476