Theorem mpbir2and 726

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

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

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 402

This theorem is used by:  elpreimad  7046  fveqressseq  7067  fmptsng  7161  fmptsnd  7162  fnprb  7202  fntpb  7203  fpr3g  8281  frrlem4  8285  1ellim  8484  isfsuppd  9336  fdmfifsupp  9345  fsuppmptif  9369  fsuppco2  9373  fsuppcor  9374  dffi3  9401  suppr  9442  infpr  9475  ordtypelem7  9496  cantnf0  9654  cantnfp1lem1  9657  cantnfp1lem2  9658  cantnfp1lem3  9659  cantnflem1a  9664  cantnflem1d  9667  cantnflem1  9668  cantnf  9672  rankpwi  9805  carduni  10033  fin23lem32  10393  fpwwe2lem5  10691  fpwwe2lem11  10697  fpwwe2lem12  10698  fpwwe2  10699  inttsk  10830  grutsk1  10877  add20  11797  supaddc  12253  supadd  12254  supmul  12258  suprzcl  12748  uzid  12949  uzwo3  13039  rpnnen1lem5  13078  xrletrid  13253  xrre  13268  xrre3  13270  xleadd1a  13352  xlemul1a  13387  elioc2  13509  elico2  13510  elicc2  13511  elfz1eq  13636  fzadd2  13661  fznatpl1  13680  elfz1uz  13696  nn0fz0  13727  fzctr  13742  fzo1fzo0n0  13818  fzoaddel  13820  elincfzoext  13826  f1resfz0f1d  13895  flid  13916  flval3  13923  fladdz  13933  fldiv  13968  modid  14004  hashf1lem1  14567  pfxccatin12d  14861  repswpfx  14903  2cshw  14931  pfx2  15065  wwlktovf1  15077  sqeqd  15300  01sqrexlem7  15382  max0add  15444  abs2difabs  15469  rddif  15475  fzomaxdiflem  15477  rexico  15488  icodiamlt  15572  limsupgre  15615  rlim3  15632  icco1  15674  rlimclim  15680  rlimuni  15684  rlimresb  15699  isercolllem2  15800  isercolllem3  15801  isercoll  15802  caucvgrlem  15807  caurcvgr  15808  iseraltlem3  15818  fsum00  15932  o1fsum  15947  bitsfzolem  16571  bitsfzo  16572  bitsmod  16573  bitscmp  16575  gcd0id  16656  gcdneg  16659  bezoutlem4  16679  nn0seqcvgd  16707  lcmneg  16740  lcmfunsnlem2lem2  16776  qredeq  16794  prmind2  16822  eulerthlem2  16920  pcpremul  16982  pcidlem  17011  pcgcd1  17016  fldivp1  17036  pcfaclem  17037  4sqlem17  17100  vdwlem1  17120  vdwlem6  17125  vdwlem12  17131  vdwlem13  17132  0ram  17159  ram0  17161  ramub1lem1  17165  invco  17907  sectmon  17918  monsect  17919  invid  17923  ssctr  17961  ssceq  17962  0ssc  17973  0subcat  17974  catsubcat  17975  issubc3  17985  fullsubc  17986  funcinv  18009  fthmon  18065  fuccocl  18103  fucidcl  18104  invfuc  18113  2initoinv  18146  2termoinv  18153  elhomai  18169  setcmon  18223  setcepi  18224  catcisolem  18246  curf2cl  18366  yonedalem4c  18412  yonedalem3  18415  yoniso  18420  lublecl  18494  isacs3lem  18677  tsrdir  18739  chnccat  18761  rabsubmgmd  18854  submgmid  18856  subsubmgm  18860  mgmhmima  18865  mgmhmeql  18866  mndpfsupp  18922  mnd1  18934  sgrp2nmndlem4  19088  sgrp2nmndlem5  19089  0subg  19323  nmznsg  19339  ghmpreima  19413  ghmeql  19414  ghmnsgpreima  19416  kerf1ghm  19422  cntzsgrpcl  19509  cntzsubm  19513  cntzsubg  19514  cntzmhm  19516  symgextfo  19597  symgfixf1  19612  symgfixfolem1  19613  odlem2  19714  finodsubmsubg  19742  gexlem2  19757  gexcl2  19764  sylow1lem5  19777  subgslw  19791  slwhash  19799  fislw  19800  sylow3lem1  19802  lsmsubg  19829  efgredlemd  19919  efgredlem  19922  efgcpbllemb  19930  frgpuplem  19947  cyggeninv  20058  iscygd  20062  iscygodd  20063  gsumzadd  20097  gsumconst  20109  gsumpt  20137  gsum2dlem2  20146  gsum2d  20147  gsum2d2lem  20148  dprdfcntz  20192  eldprdi  20195  subgdmdprd  20211  subgdprd  20212  dprdpr  20227  ablfac1c  20248  ablfac1eu  20250  ablfaclem3  20264  ogrpaddlt  20313  ogrpsublt  20317  ring1  20502  subrngint  20773  rhmimasubrng  20779  cntzsubrng  20780  rhmeql  20816  rhmima  20817  cntzsubr  20819  rnghmsscmap2  20842  rnghmsscmap  20843  rnghmsubcsetc  20846  zrzeroorngc  20857  rhmsscmap2  20871  rhmsscmap  20872  rhmsubcsetc  20875  rhmsscrnghm  20878  rhmsubcrngc  20881  srhmsubc  20893  rhmsubc  20902  issubdrg  20998  fldhmsubc  21003  imadrhmcl  21015  isabvd  21030  abvdiv  21047  ornglmullt  21087  orngrmullt  21088  orngmullt  21089  ofldlt1  21093  lsslsp  21251  lmhmima  21283  lmhmpreima  21284  lmhmeql  21291  lsmcl  21319  lspfixed  21367  rnglidlrng  21496  drngidl  21500  rngqiprngim  21561  rng2idl1cntr  21562  qsssubdrg  21693  gzrngunit  21700  pzriprnglem8  21755  evpmodpmf1o  21863  ocvpj  21984  dsmm0cl  22007  dsmmacl  22008  dsmmsubg  22010  dsmmlss  22011  frlmsplit2  22040  uvcff  22058  lindfrn  22088  f1lindf  22089  lindsss  22091  issubassa  22136  issubassa2  22161  snifpsrbag  22189  psrbaglesupp  22191  psrbaglecl  22192  psrbagaddcl  22193  psrbagcon  22194  psrbagres  22199  mplsubglem  22267  mpllsslem  22268  mplassa  22290  subrgmpl  22301  mplcoe5  22310  mplbas2  22312  mplind  22340  mpfind  22385  ismhp2  22423  mhpmulcl  22431  mhplss  22437  ply1assa  22478  coe1tmmul2  22556  coe1tmmul  22557  cply1coe0bi  22581  dmatid  22771  dmatsubcl  22774  dmatscmcl  22779  scmatid  22790  scmataddcl  22792  scmatsubcl  22793  scmatmulcl  22794  smatvscl  22800  scmatrhmcl  22804  mat0scmat  22814  mat1scmat  22815  mdet0pr  22868  chmaidscmat  23127  distop  23274  indistopon  23280  ppttop  23286  epttop  23288  mretopd  23371  toponmre  23372  neiss  23388  opnneissb  23393  ssnei2  23395  innei  23404  neiptoptop  23410  ordtcld1  23476  ordtcld2  23477  lmconst  23540  cnpnei  23543  iscncl  23548  cnss1  23555  cnss2  23556  cncnpi  23557  cncnp  23559  cnconst2  23562  cnrest  23564  cnpresti  23567  cnpdis  23572  paste  23573  lmcnp  23583  cnhaus  23633  hauscmp  23686  2ndcomap  23738  1stcelcls  23741  1stccnp  23742  llyrest  23765  nllyrest  23766  llyidm  23768  nllyidm  23769  ssref  23792  reftr  23794  refun0  23795  dissnref  23808  kgentopon  23818  kgenidm  23827  kgencn3  23838  txcld  23883  neitx  23887  tx1cn  23889  tx2cn  23890  ptcld  23893  xkoccn  23899  txcnp  23900  ptcnp  23902  txcnmpt  23904  ptcn  23907  txdis1cn  23915  ptrescn  23919  txkgen  23932  xkoco1cn  23937  xkoco2cn  23938  xkococn  23940  xkoinjcn  23967  qtoptop2  23979  qtopuni  23982  qtopid  23985  qtopkgen  23990  basqtop  23991  tgqtop  23992  qtopss  23995  qtopeu  23996  qtoprest  23997  kqopn  24014  kqcld  24015  kqreglem2  24022  reghmph  24073  ordthmeolem  24081  qtopf1  24096  opnfbas  24122  isfil2  24136  fbasweak  24145  fsubbas  24147  filconn  24163  fbasrn  24164  rnelfmlem  24232  flimss2  24252  flimss1  24253  hausflim  24261  flimclslem  24264  flimsncls  24266  cnpflfi  24279  flfcnp2  24287  fclsfnflim  24307  cnextfvval  24345  cnextfres1  24348  symgtgp  24386  opnsubg  24388  ghmcnp  24395  qustgpopn  24400  qustgplem  24401  qustgphaus  24403  tsmsfbas  24408  ustfilxp  24493  utoptop  24514  utopbas  24515  restutopopn  24518  iducn  24562  cstucnd  24563  ucncn  24564  fmucnd  24571  cfilufg  24572  trcfilu  24573  cfiluweak  24574  neipcfilu  24575  psmetres2  24594  isxmetd  24606  xmetpsmet  24628  imasf1oxmet  24655  xblss2ps  24681  xblss2  24682  xblcntrps  24690  xblcntr  24691  blcld  24785  metustfbas  24837  cfilucfil  24839  restmetu  24850  ngptgp  24916  tngngpd  24933  nrmtngnrm  24938  tngnrg  24954  nlmvscn  24967  nrginvrcn  24972  nmo0  25015  nmoeq0  25016  nmoid  25022  nghmcn  25025  0nmhm  25035  blcvx  25078  iccntr  25102  xrge0tsms  25115  xmetdcn2  25118  metdstri  25132  metdscn  25137  rescncf  25179  cncfco  25189  oprpiece1res2  25234  cnheibor  25237  cnllycmp  25238  bndth  25240  ishtpyd  25257  isphtpyd  25268  pcoval2  25298  nmhmcn  25402  ipcn  25528  lmnn  25545  cfilss  25552  iscfil3  25555  cfilfcls  25556  cmetcaulem  25570  iscmet3lem2  25574  cfilres  25578  lmcau  25595  flimcfil  25596  cncmet  25604  rlmbn  25643  minveclem3b  25710  pjthlem1  25719  pjth2  25722  ivthlem3  25735  ovolssnul  25769  ovolctb  25772  ovoliunnul  25789  ovolsca  25797  ovolicopnf  25806  voliunlem2  25833  volsup  25838  dyadmaxlem  25879  vitalilem5  25894  mbfres  25926  mbfss  25928  mbfmulc2re  25930  mbfadd  25943  mbfmulc2  25945  mbflim  25950  i1faddlem  25975  i1fmullem  25976  mbfmul  26008  itg2mulc  26029  itg2cnlem1  26043  ibl0  26068  iblposlem  26073  itgreval  26078  iblneg  26084  iblss  26086  iblss2  26087  itgle  26091  iblconst  26099  iblabs  26110  iblabsr  26111  iblmulc2  26112  bddmulibl  26120  limciun  26175  limcun  26176  dvres2lem  26191  dvidlem  26196  dvcnp2  26201  dvcn  26202  cpnres  26218  dvaddbr  26219  dvmulbr  26220  dvcobr  26227  dvcjbr  26230  dvrec  26236  dvcnvlem  26257  dvferm  26269  dvlip2  26276  dveq0  26281  dv11cn  26282  dvivthlem1  26289  lhop1  26295  lhop2  26296  lhop  26297  dvcnvre  26300  dvfsumlem3  26309  dvfsumlem4  26310  dvfsumrlim  26312  dvfsum2  26315  ftc1a  26318  ftc1lem4  26320  ftc1lem6  26322  ftc1  26323  coe1mul3  26378  deg1addle2  26381  deg1sublt  26389  fta1blem  26450  drnguc1p  26453  ig1prsp  26460  plyco0  26471  plyeq0lem  26490  dgrub  26514  dgreq  26524  dgradd2  26548  dgrmul  26550  dgrcolem2  26554  dgrco  26555  plycpn  26573  plydivlem4  26580  plydiveu  26582  vieta1lem2  26597  vieta1  26598  aalioulem2  26623  aalioulem3  26624  aaliou3lem7  26639  tayl0  26652  ulmcn  26689  ulmdvlem3  26692  psercn  26716  abelth  26731  pilem3  26743  efif1olem1  26833  abslogimle  26864  argregt0  26901  argrege0  26902  logf1o2  26941  cxpsqrtlem  26993  cxpcn3  27039  abscxpbnd  27044  logreclem  27053  ang180lem2  27101  ang180lem3  27102  xrlimcnp  27259  harmonicbnd4  27301  fsumharmonic  27302  lgamgulmlem5  27323  lgambdd  27327  basellem4  27374  dvdsppwf1o  27476  dvdsflf1o  27477  fsumfldivdiaglem  27479  chpeq0  27498  chteq0  27499  chtub  27502  chpub  27510  dchrelbasd  27529  dchrmulcl  27539  dchrinv  27551  bposlem1  27574  bposlem2  27575  lgsdirprm  27621  lgsqrlem2  27637  lgsqrlem3  27638  lgsdchr  27645  lgseisenlem1  27665  lgseisenlem2  27666  lgseisenlem3  27667  lgsquadlem1  27670  2sqlem8  27716  2sqblem  27721  2sqmod  27726  chebbnd1lem1  27759  dchrisumlem1  27779  dchrisumlem2  27780  dchrisumlem3  27781  dchrisum0fno1  27801  pntrmax  27854  pntpbnd1a  27875  pntibndlem3  27882  pntlemn  27890  pntlemi  27894  pntlem3  27899  pntleml  27901  ostth1  27923  ostth2  27927  ostth3  27928  nosepon  27955  nolesgn2ores  27962  nogesgn1ores  27964  nosupres  27997  nosupbnd1lem2  27999  nosupbnd2lem1  28005  noinfres  28012  noinfbnd1lem2  28014  noinfbnd2lem1  28020  eqcuts3  28123  cofcutrtime  28246  divmuldivsd  28551  divdivs1d  28552  onsbnd  28600  nnsgt0  28658  bdayfinbndlem1  28786  ercgrg  28913  motco  28936  cnvmot  28937  legso  28995  mirmot  29080  colopp  29180  hphl  29182  lmicom  29226  lmimid  29232  lmimot  29236  hypcgrlem1  29238  hypcgrlem2  29239  trgcopyeulem  29245  inagswap  29293  inaghl  29297  cgrg3col4  29305  prlngd  29350  prlngref  29351  dfprlng2  29358  brbtwn2  29416  axlowdimlem3  29455  axlowdimlem16  29468  axcontlem8  29482  fusgrfis  29844  nbgr2vtx1edg  29864  0vtxrgr  30090  0vtxrusgr  30091  ewlkle  30119  wlk1ewlk  30153  uspgr2wlkeq2  30160  wlkp1lem8  30192  trlontrl  30226  pthonpth  30267  pthdlem2  30287  wlklnwwlkln1  30390  wlknewwlksn  30409  wwlksnred  30414  wwlksnredwwlkn0  30418  2trlond  30461  2pthond  30464  elwwlks2ons3im  30476  clwlkclwwlklem2a1  30516  clwlkclwwlkf1  30534  clwwlkel  30570  clwwlkwwlksb  30578  wwlksext2clwwlk  30581  1ewlk  30639  0trlon  30648  0pthon  30651  1pthond  30668  3trlond  30707  3pthond  30709  3spthond  30711  eupthres  30749  2clwwlk2clwwlk  30884  numclwwlk1lem2foa  30888  numclwwlk1lem2f1  30891  nvabs  31207  vacn  31229  nmcvcn  31230  nmblore  31321  0lno  31325  0blo  31327  nmlno0lem  31328  occl  31839  pjhthlem1  31926  pjpjpre  31954  nmopre  32405  nmlnop0iALT  32530  nmophmi  32566  leoprf2  32662  stlesi  32776  disjdifprg  33102  disjun0  33122  fsuppcurry1  33249  fsuppcurry2  33250  fpwrelmap  33258  fzspl  33314  dfmgc2lem  33489  pwrssmgc  33494  xrge0tsmsd  33567  psgnfzto1stlem  33594  fzto1st1  33596  evpmid  33642  pnfinf  33677  isarchiofld  33693  rmfsupp2  33731  fracfld  33803  dvdsruassoi  33872  nsgmgc  33896  qsdrngi  33952  deg1addlt  34065  ply1degltdimlem  34187  lbsdiflsp0  34191  fedgmul  34196  fldexttr  34223  fldextid  34224  irngnzply1lem  34255  finextalg  34263  minplyelirng  34280  irredminply  34281  algextdeglem8  34289  rtelextdg2lem  34291  constrsslem  34306  constrllcllem  34317  constrlccllem  34318  constrcccllem  34319  qtopt1  34400  reff  34404  locfinreflem  34405  metideq  34458  metider  34459  pstmxmet  34462  qqhval2lem  34546  qqhcn  34556  qqhucn  34557  pwsiga  34695  prsiga  34696  measle0  34774  mbfmcst  34825  1stmbfm  34826  2ndmbfm  34827  imambfm  34828  cnmbfm  34829  mbfmco  34830  mbfmco2  34831  0elcarsg  34873  carsgclctun  34887  sibfof  34906  oddpwdc  34920  eulerpartlemmf  34941  eulerpartlemgs2  34946  0rrv  35017  ballotlemfc0  35059  ballotlemfcc  35060  signstfveq0  35140  breprexplemc  35195  bnj1452  35616  usgrgt2cycl  35830  acycgr1v  35835  derangen  35858  subfacval3  35875  cvmseu  35962  cvmliftmolem2  35968  cvmliftlem7  35977  cvmliftlem15  35984  cvmlift2lem9a  35989  cvmlift2lem9  35997  cvmlift2lem10  35998  cvmlift2lem11  35999  cvmlift2lem12  36000  cvmlift3lem6  36010  cvmlift3lem8  36012  ex-sategoelel  36107  ex-sategoelelomsuc  36112  mclsppslem  36269  mclspps  36270  wsuclem  36509  nadddilem2  36892  fness  37059  fnetr  37061  fnessref  37067  refssfne  37068  neibastop1  37069  neibastop2  37071  tailfb  37087  filnetlem3  37090  weiunfrlem  37174  bj-finsumval0  38126  bj-rvecvec  38140  dfgcd3  38165  lindsadd  38456  poimirlem13  38471  poimirlem15  38473  poimirlem24  38482  poimirlem28  38486  mblfinlem2  38496  ovoliunnfl  38500  volsupnfl  38503  mbfresfi  38504  iblabsnc  38522  iblmulc2nc  38523  ftc1cnnclem  38529  ftc1cnnc  38530  ftc1anc  38539  sdclem2  38596  metf1o  38609  ismtyhmeolem  38658  ismtyres  38662  heibor1lem  38663  bfplem2  38677  bfp  38678  rrncmslem  38686  iccbnd  38694  icccmpALT  38695  rngogrphom  38825  rngoisoco  38836  keridl  38886  lsmcv2  40006  lsatcv0  40008  lcvexchlem4  40014  lcvexchlem5  40015  l1cvpat  40031  lfl0f  40046  lfladdcl  40048  lflnegcl  40052  lkrlss  40072  eqlkr  40076  lkrlsp  40079  lkrlsp2  40080  lshpkrcl  40093  lkrin  40141  1cvrjat  40452  llni  40485  llnle  40495  lplni  40509  lplnle  40517  llncvrlpln2  40534  2atmat  40538  lvoli  40552  lplncvrlvol2  40592  elpaddri  40779  paddclN  40819  pclclN  40868  pclfinN  40877  0psubclN  40920  1psubclN  40921  atpsubclN  40922  pmapsubclN  40923  osumclN  40944  pexmidN  40946  pexmidlem6N  40952  lhp2lt  40978  lautcnv  41067  idlaut  41073  lautco  41074  idldil  41091  ldilcnv  41092  ldilco  41093  ltrncnv  41123  idltrn  41127  cdleme16d  41258  cdleme50laut  41524  cdleme50ldil  41525  cdleme50ltrn  41534  ltrnco  41696  dian0  42016  dia0eldmN  42017  dia1eldmN  42018  dialss  42023  diaintclN  42035  docaclN  42101  doca2N  42103  djajN  42114  dibintclN  42144  diblss  42147  dicvaddcl  42167  dicvscacl  42168  dicn0  42169  cdlemn11a  42184  dihord2cN  42198  dihord11b  42199  dihord6apre  42233  dihmeetlem1N  42267  dihglblem5apreN  42268  dihpN  42313  dihjatcclem4  42398  dochkr1  42455  islpoldN  42461  lcfrlem31  42550  mapdpglem18  42666  mapdheq2  42706  mapdheq4  42709  mapdh6aN  42712  hdmap1l6a  42786  hdmap14lem4a  42848  lcmineqlem4  43002  frlmfzoccat  43497  drnginvmuld  43513  evlselvlem  43538  evlselv  43539  fsuppind  43540  fsuppssind  43543  prjspvs  43560  irrapxlem4  43770  pell1234qrdich  43806  pell1qr1  43816  pell14qrgap  43820  pellqrexplicit  43822  rmspecfund  43854  fzmaxdif  43926  acongeq  43928  jm2.23  43941  jm3.1  43965  lmhmlnmsplit  44032  hbt  44075  dgrsub2  44080  proot1ex  44141  cantnfub  44266  cantnfresb  44269  cantnf2  44270  tfsconcatfv2  44285  tfsconcatrn  44287  tfsconcatb0  44289  naddcnff  44307  naddcnffo  44309  naddcnfid1  44312  naddcnfid2  44313  clublem  44554  dftrcl3  44664  mnugrud  45212  hashnzfz2  45249  dvconstbi  45262  ubelsupr  45958  restopn3  46087  wessf1ornlem  46121  lefldiveq  46229  iccintsng  46457  climsuse  46542  mullimc  46550  limcdm0  46552  limccog  46554  mullimcf  46557  constlimc  46558  idlimc  46560  limcperiod  46562  limsupre  46573  limcleqr  46576  neglimc  46579  addlimc  46580  0ellimcdiv  46581  xlimliminflimsup  46794  cncfshift  46806  cncfperiod  46811  cncfuni  46818  icccncfext  46819  cncfiooicclem1  46825  fperdvper  46851  ioodvbdlimc1lem2  46864  ioodvbdlimc2lem  46866  mbfres2cn  46890  iblsplit  46898  stoweidlem7  46939  stoweidlem13  46945  stoweidlem26  46958  wallispilem3  46999  stirlinglem6  47011  stirlinglem10  47015  dirkercncf  47039  fourierdlem6  47045  fourierdlem11  47050  fourierdlem12  47051  fourierdlem15  47054  fourierdlem26  47065  fourierdlem42  47081  fourierdlem50  47088  fourierdlem51  47089  fourierdlem52  47090  fourierdlem54  47092  fourierdlem62  47100  fourierdlem79  47117  fourierdlem102  47140  fourierdlem114  47152  etransclem23  47189  chnsubseq  47812  3f1oss1  48067  zgeltp1eq  48301  nnmul2  48322  setsnidel  48381  preimafvsnel  48383  iccpartres  48422  prpair  48505  fpprel2  48761  isubgrsubgr  48889  grimidvtxedg  48905  grimcnv  48908  isuspgrim  48916  upgrimpthslem2  48928  stgrnbgr0  48984  uhgrimgrlim  49007  clnbgr3stgrgrlim  49039  gpg5nbgrvtx03starlem2  49089  gpg5nbgrvtx13starlem2  49092  gpg5edgnedg  49150  isassintop  49229  rhmsubcALTV  49304  srhmsubcALTV  49344  fldhmsubcALTV  49352  rmfsupp  49407  scmfsupp  49409  mptcfsupp  49411  lcoel0  49462  lincsumcl  49465  lincscmcl  49466  lcoss  49470  lindsrng01  49502  lincreslvec3  49516  lindssnlvec  49520  zgtp1leeq  49555  lubsscl  49990  glbsscl  49991  idmon  50050  idepi  50051  iinfssc  50087  iinfsubc  50088  discsubc  50094  nelsubclem  50097  imassc  50183  imasubc3  50186  isnatd  50253  swapfiso  50315  fucoppc  50440  thinciso  50500  diagciso  50569  termolmd  50700  wrdf1d  50862