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  7055  fveqressseq  7075  fmptsng  7169  fmptsnd  7170  fnprb  7210  fntpb  7211  fpr3g  8287  frrlem4  8291  1ellim  8488  isfsuppd  9339  fdmfifsupp  9348  fsuppmptif  9372  fsuppco2  9376  fsuppcor  9377  dffi3  9404  suppr  9445  infpr  9478  ordtypelem7  9499  cantnf0  9657  cantnfp1lem1  9660  cantnfp1lem2  9661  cantnfp1lem3  9662  cantnflem1a  9667  cantnflem1d  9670  cantnflem1  9671  cantnf  9675  rankpwi  9808  carduni  9989  fin23lem32  10349  fpwwe2lem5  10647  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  inttsk  10786  grutsk1  10833  add20  11753  supaddc  12209  supadd  12210  supmul  12214  suprzcl  12704  uzid  12905  uzwo3  12995  rpnnen1lem5  13033  xrletrid  13208  xrre  13223  xrre3  13225  xleadd1a  13307  xlemul1a  13342  elioc2  13464  elico2  13465  elicc2  13466  elfz1eq  13591  fzadd2  13616  fznatpl1  13635  elfz1uz  13651  nn0fz0  13682  fzctr  13697  fzo1fzo0n0  13773  fzoaddel  13775  elincfzoext  13781  f1resfz0f1d  13850  flid  13871  flval3  13878  fladdz  13888  fldiv  13923  modid  13959  hashf1lem1  14522  pfxccatin12d  14816  repswpfx  14858  2cshw  14886  pfx2  15020  wwlktovf1  15032  sqeqd  15255  01sqrexlem7  15337  max0add  15399  abs2difabs  15424  rddif  15430  fzomaxdiflem  15432  rexico  15443  icodiamlt  15527  limsupgre  15570  rlim3  15587  icco1  15629  rlimclim  15635  rlimuni  15639  rlimresb  15654  isercolllem2  15755  isercolllem3  15756  isercoll  15757  caucvgrlem  15762  caurcvgr  15763  iseraltlem3  15773  fsum00  15887  o1fsum  15902  bitsfzolem  16528  bitsfzo  16529  bitsmod  16530  bitscmp  16532  gcd0id  16613  gcdneg  16616  bezoutlem4  16636  nn0seqcvgd  16664  lcmneg  16697  lcmfunsnlem2lem2  16733  qredeq  16751  prmind2  16779  eulerthlem2  16877  pcpremul  16939  pcidlem  16968  pcgcd1  16973  fldivp1  16993  pcfaclem  16994  4sqlem17  17057  vdwlem1  17077  vdwlem6  17082  vdwlem12  17088  vdwlem13  17089  0ram  17116  ram0  17118  ramub1lem1  17122  invco  17864  sectmon  17875  monsect  17876  invid  17880  ssctr  17918  ssceq  17919  0ssc  17930  0subcat  17931  catsubcat  17932  issubc3  17942  fullsubc  17943  funcinv  17966  fthmon  18022  fuccocl  18060  fucidcl  18061  invfuc  18070  2initoinv  18103  2termoinv  18110  elhomai  18126  setcmon  18180  setcepi  18181  catcisolem  18203  curf2cl  18323  yonedalem4c  18369  yonedalem3  18372  yoniso  18377  lublecl  18451  isacs3lem  18634  tsrdir  18696  chnccat  18718  rabsubmgmd  18808  submgmid  18810  subsubmgm  18814  mgmhmima  18819  mgmhmeql  18820  mndpfsupp  18876  mnd1  18888  sgrp2nmndlem4  19041  sgrp2nmndlem5  19042  0subg  19276  nmznsg  19292  ghmpreima  19366  ghmeql  19367  ghmnsgpreima  19369  kerf1ghm  19375  cntzsgrpcl  19462  cntzsubm  19466  cntzsubg  19467  cntzmhm  19469  symgextfo  19550  symgfixf1  19565  symgfixfolem1  19566  odlem2  19667  finodsubmsubg  19695  gexlem2  19710  gexcl2  19717  sylow1lem5  19730  subgslw  19744  slwhash  19752  fislw  19753  sylow3lem1  19755  lsmsubg  19782  efgredlemd  19872  efgredlem  19875  efgcpbllemb  19883  frgpuplem  19900  cyggeninv  20011  iscygd  20015  iscygodd  20016  gsumzadd  20050  gsumconst  20062  gsumpt  20090  gsum2dlem2  20099  gsum2d  20100  gsum2d2lem  20101  dprdfcntz  20145  eldprdi  20148  subgdmdprd  20164  subgdprd  20165  dprdpr  20180  ablfac1c  20201  ablfac1eu  20203  ablfaclem3  20217  ogrpaddlt  20266  ogrpsublt  20270  ring1  20453  subrngint  20723  rhmimasubrng  20729  cntzsubrng  20730  rhmeql  20766  rhmima  20767  cntzsubr  20769  rnghmsscmap2  20792  rnghmsscmap  20793  rnghmsubcsetc  20796  zrzeroorngc  20807  rhmsscmap2  20821  rhmsscmap  20822  rhmsubcsetc  20825  rhmsscrnghm  20828  rhmsubcrngc  20831  srhmsubc  20843  rhmsubc  20852  issubdrg  20947  fldhmsubc  20952  imadrhmcl  20964  isabvd  20979  abvdiv  20996  ornglmullt  21036  orngrmullt  21037  orngmullt  21038  ofldlt1  21042  lsslsp  21200  lmhmima  21232  lmhmpreima  21233  lmhmeql  21240  lsmcl  21268  lspfixed  21316  rnglidlrng  21445  drngidl  21449  rngqiprngim  21508  rng2idl1cntr  21509  qsssubdrg  21640  gzrngunit  21647  pzriprnglem8  21702  evpmodpmf1o  21810  ocvpj  21931  dsmm0cl  21954  dsmmacl  21955  dsmmsubg  21957  dsmmlss  21958  frlmsplit2  21987  uvcff  22005  lindfrn  22035  f1lindf  22036  lindsss  22038  issubassa  22083  issubassa2  22108  snifpsrbag  22136  psrbaglesupp  22138  psrbaglecl  22139  psrbagaddcl  22140  psrbagcon  22141  psrbagres  22146  mplsubglem  22214  mpllsslem  22215  mplassa  22237  subrgmpl  22248  mplcoe5  22257  mplbas2  22259  mplind  22287  mpfind  22332  ismhp2  22370  mhpmulcl  22378  mhplss  22384  ply1assa  22425  coe1tmmul2  22503  coe1tmmul  22504  cply1coe0bi  22528  dmatid  22718  dmatsubcl  22721  dmatscmcl  22726  scmatid  22737  scmataddcl  22739  scmatsubcl  22740  scmatmulcl  22741  smatvscl  22747  scmatrhmcl  22751  mat0scmat  22761  mat1scmat  22762  mdet0pr  22815  chmaidscmat  23074  distop  23221  indistopon  23227  ppttop  23233  epttop  23235  mretopd  23318  toponmre  23319  neiss  23335  opnneissb  23340  ssnei2  23342  innei  23351  neiptoptop  23357  ordtcld1  23423  ordtcld2  23424  lmconst  23487  cnpnei  23490  iscncl  23495  cnss1  23502  cnss2  23503  cncnpi  23504  cncnp  23506  cnconst2  23509  cnrest  23511  cnpresti  23514  cnpdis  23519  paste  23520  lmcnp  23530  cnhaus  23580  hauscmp  23633  2ndcomap  23685  1stcelcls  23688  1stccnp  23689  llyrest  23712  nllyrest  23713  llyidm  23715  nllyidm  23716  ssref  23739  reftr  23741  refun0  23742  dissnref  23755  kgentopon  23765  kgenidm  23774  kgencn3  23785  txcld  23830  neitx  23834  tx1cn  23836  tx2cn  23837  ptcld  23840  xkoccn  23846  txcnp  23847  ptcnp  23849  txcnmpt  23851  ptcn  23854  txdis1cn  23862  ptrescn  23866  txkgen  23879  xkoco1cn  23884  xkoco2cn  23885  xkococn  23887  xkoinjcn  23914  qtoptop2  23926  qtopuni  23929  qtopid  23932  qtopkgen  23937  basqtop  23938  tgqtop  23939  qtopss  23942  qtopeu  23943  qtoprest  23944  kqopn  23961  kqcld  23962  kqreglem2  23969  reghmph  24020  ordthmeolem  24028  qtopf1  24043  opnfbas  24069  isfil2  24083  fbasweak  24092  fsubbas  24094  filconn  24110  fbasrn  24111  rnelfmlem  24179  flimss2  24199  flimss1  24200  hausflim  24208  flimclslem  24211  flimsncls  24213  cnpflfi  24226  flfcnp2  24234  fclsfnflim  24254  cnextfvval  24292  cnextfres1  24295  symgtgp  24333  opnsubg  24335  ghmcnp  24342  qustgpopn  24347  qustgplem  24348  qustgphaus  24350  tsmsfbas  24355  ustfilxp  24440  utoptop  24461  utopbas  24462  restutopopn  24465  iducn  24509  cstucnd  24510  ucncn  24511  fmucnd  24518  cfilufg  24519  trcfilu  24520  cfiluweak  24521  neipcfilu  24522  psmetres2  24541  isxmetd  24553  xmetpsmet  24575  imasf1oxmet  24602  xblss2ps  24628  xblss2  24629  xblcntrps  24637  xblcntr  24638  blcld  24732  metustfbas  24784  cfilucfil  24786  restmetu  24797  ngptgp  24863  tngngpd  24880  nrmtngnrm  24885  tngnrg  24901  nlmvscn  24914  nrginvrcn  24919  nmo0  24962  nmoeq0  24963  nmoid  24969  nghmcn  24972  0nmhm  24982  blcvx  25025  iccntr  25049  xrge0tsms  25062  xmetdcn2  25065  metdstri  25079  metdscn  25084  rescncf  25126  cncfco  25136  oprpiece1res2  25181  cnheibor  25184  cnllycmp  25185  bndth  25187  ishtpyd  25204  isphtpyd  25215  pcoval2  25245  nmhmcn  25349  ipcn  25475  lmnn  25492  cfilss  25499  iscfil3  25502  cfilfcls  25503  cmetcaulem  25517  iscmet3lem2  25521  cfilres  25525  lmcau  25542  flimcfil  25543  cncmet  25551  rlmbn  25590  minveclem3b  25657  pjthlem1  25666  pjth2  25669  ivthlem3  25682  ovolssnul  25716  ovolctb  25719  ovoliunnul  25736  ovolsca  25744  ovolicopnf  25753  voliunlem2  25780  volsup  25785  dyadmaxlem  25826  vitalilem5  25841  mbfres  25873  mbfss  25875  mbfmulc2re  25877  mbfadd  25890  mbfmulc2  25892  mbflim  25897  i1faddlem  25922  i1fmullem  25923  mbfmul  25955  itg2mulc  25976  itg2cnlem1  25990  ibl0  26016  iblposlem  26021  itgreval  26026  iblneg  26032  iblss  26034  iblss2  26035  itgle  26039  iblconst  26047  iblabs  26058  iblabsr  26059  iblmulc2  26060  bddmulibl  26068  limciun  26123  limcun  26124  dvres2lem  26139  dvidlem  26144  dvcnp2  26149  dvcn  26150  cpnres  26166  dvaddbr  26167  dvmulbr  26168  dvcobr  26175  dvcjbr  26178  dvrec  26184  dvcnvlem  26205  dvferm  26217  dvlip2  26224  dveq0  26229  dv11cn  26230  dvivthlem1  26237  lhop1  26243  lhop2  26244  lhop  26245  dvcnvre  26248  dvfsumlem3  26257  dvfsumlem4  26258  dvfsumrlim  26260  dvfsum2  26263  ftc1a  26266  ftc1lem4  26268  ftc1lem6  26270  ftc1  26271  coe1mul3  26326  deg1addle2  26329  deg1sublt  26337  fta1blem  26398  drnguc1p  26401  ig1prsp  26408  plyco0  26419  plyeq0lem  26437  dgrub  26461  dgreq  26471  dgradd2  26495  dgrmul  26497  dgrcolem2  26501  dgrco  26502  plycpn  26520  plydivlem4  26527  plydiveu  26529  vieta1lem2  26542  vieta1  26543  aalioulem2  26566  aalioulem3  26567  aaliou3lem7  26582  tayl0  26595  ulmcn  26632  ulmdvlem3  26635  psercn  26659  abelth  26674  pilem3  26686  efif1olem1  26777  abslogimle  26808  argregt0  26845  argrege0  26846  logf1o2  26885  cxpsqrtlem  26937  cxpcn3  26983  abscxpbnd  26988  logreclem  26997  ang180lem2  27045  ang180lem3  27046  xrlimcnp  27203  harmonicbnd4  27245  fsumharmonic  27246  lgamgulmlem5  27267  lgambdd  27271  basellem4  27318  dvdsppwf1o  27420  dvdsflf1o  27421  fsumfldivdiaglem  27423  chpeq0  27442  chteq0  27443  chtub  27446  chpub  27454  dchrelbasd  27473  dchrmulcl  27483  dchrinv  27495  bposlem1  27518  bposlem2  27519  lgsdirprm  27565  lgsqrlem2  27581  lgsqrlem3  27582  lgsdchr  27589  lgseisenlem1  27609  lgseisenlem2  27610  lgseisenlem3  27611  lgsquadlem1  27614  2sqlem8  27660  2sqblem  27665  2sqmod  27670  chebbnd1lem1  27703  dchrisumlem1  27723  dchrisumlem2  27724  dchrisumlem3  27725  dchrisum0fno1  27745  pntrmax  27798  pntpbnd1a  27819  pntibndlem3  27826  pntlemn  27834  pntlemi  27838  pntlem3  27843  pntleml  27845  ostth1  27867  ostth2  27871  ostth3  27872  nosepon  27899  nolesgn2ores  27906  nogesgn1ores  27908  nosupres  27941  nosupbnd1lem2  27943  nosupbnd2lem1  27949  noinfres  27956  noinfbnd1lem2  27958  noinfbnd2lem1  27964  eqcuts3  28067  cofcutrtime  28190  divmuldivsd  28495  divdivs1d  28496  onsbnd  28544  nnsgt0  28602  bdayfinbndlem1  28730  ercgrg  28857  motco  28880  cnvmot  28881  legso  28939  mirmot  29024  colopp  29124  hphl  29126  lmicom  29170  lmimid  29176  lmimot  29180  hypcgrlem1  29182  hypcgrlem2  29183  trgcopyeulem  29189  inagswap  29237  inaghl  29241  cgrg3col4  29249  prlngd  29282  prlngref  29283  dfprlng2  29290  brbtwn2  29348  axlowdimlem3  29387  axlowdimlem16  29400  axcontlem8  29414  fusgrfis  29776  nbgr2vtx1edg  29796  0vtxrgr  30022  0vtxrusgr  30023  ewlkle  30051  wlk1ewlk  30085  uspgr2wlkeq2  30092  wlkp1lem8  30124  trlontrl  30158  pthonpth  30199  pthdlem2  30219  wlklnwwlkln1  30322  wlknewwlksn  30341  wwlksnred  30346  wwlksnredwwlkn0  30350  2trlond  30393  2pthond  30396  elwwlks2ons3im  30408  clwlkclwwlklem2a1  30448  clwlkclwwlkf1  30466  clwwlkel  30502  clwwlkwwlksb  30510  wwlksext2clwwlk  30513  1ewlk  30571  0trlon  30580  0pthon  30583  1pthond  30600  3trlond  30639  3pthond  30641  3spthond  30643  eupthres  30681  2clwwlk2clwwlk  30816  numclwwlk1lem2foa  30820  numclwwlk1lem2f1  30823  nvabs  31139  vacn  31161  nmcvcn  31162  nmblore  31253  0lno  31257  0blo  31259  nmlno0lem  31260  occl  31771  pjhthlem1  31858  pjpjpre  31886  nmopre  32337  nmlnop0iALT  32462  nmophmi  32498  leoprf2  32594  stlesi  32708  disjdifprg  33035  disjun0  33055  fsuppcurry1  33182  fsuppcurry2  33183  fpwrelmap  33191  fzspl  33247  dfmgc2lem  33422  pwrssmgc  33427  xrge0tsmsd  33500  psgnfzto1stlem  33527  fzto1st1  33529  evpmid  33575  pnfinf  33610  isarchiofld  33626  rmfsupp2  33664  fracfld  33736  dvdsruassoi  33804  nsgmgc  33828  qsdrngi  33884  deg1addlt  33997  ply1degltdimlem  34119  lbsdiflsp0  34123  fedgmul  34128  fldexttr  34155  fldextid  34156  irngnzply1lem  34187  finextalg  34195  minplyelirng  34212  irredminply  34213  algextdeglem8  34221  rtelextdg2lem  34223  constrsslem  34238  constrllcllem  34249  constrlccllem  34250  constrcccllem  34251  qtopt1  34332  reff  34336  locfinreflem  34337  metideq  34390  metider  34391  pstmxmet  34394  qqhval2lem  34478  qqhcn  34488  qqhucn  34489  pwsiga  34627  prsiga  34628  measle0  34706  mbfmcst  34757  1stmbfm  34758  2ndmbfm  34759  imambfm  34760  cnmbfm  34761  mbfmco  34762  mbfmco2  34763  0elcarsg  34805  carsgclctun  34819  sibfof  34838  oddpwdc  34852  eulerpartlemmf  34873  eulerpartlemgs2  34878  0rrv  34949  ballotlemfc0  34991  ballotlemfcc  34992  signstfveq0  35072  breprexplemc  35127  bnj1452  35548  usgrgt2cycl  35710  acycgr1v  35715  derangen  35738  subfacval3  35755  cvmseu  35842  cvmliftmolem2  35848  cvmliftlem7  35857  cvmliftlem15  35864  cvmlift2lem9a  35869  cvmlift2lem9  35877  cvmlift2lem10  35878  cvmlift2lem11  35879  cvmlift2lem12  35880  cvmlift3lem6  35890  cvmlift3lem8  35892  ex-sategoelel  35987  ex-sategoelelomsuc  35992  mclsppslem  36149  mclspps  36150  wsuclem  36389  nadddilem2  36788  fness  36955  fnetr  36957  fnessref  36963  refssfne  36964  neibastop1  36965  neibastop2  36967  tailfb  36983  filnetlem3  36986  weiunfrlem  37070  bj-finsumval0  38024  bj-rvecvec  38038  dfgcd3  38063  lindsadd  38354  poimirlem13  38369  poimirlem15  38371  poimirlem24  38380  poimirlem28  38384  mblfinlem2  38394  ovoliunnfl  38398  volsupnfl  38401  mbfresfi  38402  iblabsnc  38420  iblmulc2nc  38421  ftc1cnnclem  38427  ftc1cnnc  38428  ftc1anc  38437  sdclem2  38479  metf1o  38492  ismtyhmeolem  38541  ismtyres  38545  heibor1lem  38546  bfplem2  38560  bfp  38561  rrncmslem  38569  iccbnd  38577  icccmpALT  38578  rngogrphom  38708  rngoisoco  38719  keridl  38769  lsmcv2  39889  lsatcv0  39891  lcvexchlem4  39897  lcvexchlem5  39898  l1cvpat  39914  lfl0f  39929  lfladdcl  39931  lflnegcl  39935  lkrlss  39955  eqlkr  39959  lkrlsp  39962  lkrlsp2  39963  lshpkrcl  39976  lkrin  40024  1cvrjat  40335  llni  40368  llnle  40378  lplni  40392  lplnle  40400  llncvrlpln2  40417  2atmat  40421  lvoli  40435  lplncvrlvol2  40475  elpaddri  40662  paddclN  40702  pclclN  40751  pclfinN  40760  0psubclN  40803  1psubclN  40804  atpsubclN  40805  pmapsubclN  40806  osumclN  40827  pexmidN  40829  pexmidlem6N  40835  lhp2lt  40861  lautcnv  40950  idlaut  40956  lautco  40957  idldil  40974  ldilcnv  40975  ldilco  40976  ltrncnv  41006  idltrn  41010  cdleme16d  41141  cdleme50laut  41407  cdleme50ldil  41408  cdleme50ltrn  41417  ltrnco  41579  dian0  41899  dia0eldmN  41900  dia1eldmN  41901  dialss  41906  diaintclN  41918  docaclN  41984  doca2N  41986  djajN  41997  dibintclN  42027  diblss  42030  dicvaddcl  42050  dicvscacl  42051  dicn0  42052  cdlemn11a  42067  dihord2cN  42081  dihord11b  42082  dihord6apre  42116  dihmeetlem1N  42150  dihglblem5apreN  42151  dihpN  42196  dihjatcclem4  42281  dochkr1  42338  islpoldN  42344  lcfrlem31  42433  mapdpglem18  42549  mapdheq2  42589  mapdheq4  42592  mapdh6aN  42595  hdmap1l6a  42669  hdmap14lem4a  42731  lcmineqlem4  42885  frlmfzoccat  43380  drnginvmuld  43396  evlselvlem  43421  evlselv  43422  fsuppind  43423  fsuppssind  43426  prjspvs  43443  irrapxlem4  43653  pell1234qrdich  43689  pell1qr1  43699  pell14qrgap  43703  pellqrexplicit  43705  rmspecfund  43737  fzmaxdif  43809  acongeq  43811  jm2.23  43824  jm3.1  43848  lmhmlnmsplit  43915  hbt  43958  dgrsub2  43963  proot1ex  44024  cantnfub  44149  cantnfresb  44152  cantnf2  44153  tfsconcatfv2  44168  tfsconcatrn  44170  tfsconcatb0  44172  naddcnff  44190  naddcnffo  44192  naddcnfid1  44195  naddcnfid2  44196  clublem  44437  dftrcl3  44547  mnugrud  45095  hashnzfz2  45132  dvconstbi  45145  ubelsupr  45841  restopn3  45970  wessf1ornlem  46004  lefldiveq  46112  iccintsng  46340  climsuse  46425  mullimc  46433  limcdm0  46435  limccog  46437  mullimcf  46440  constlimc  46441  idlimc  46443  limcperiod  46445  limsupre  46456  limcleqr  46459  neglimc  46462  addlimc  46463  0ellimcdiv  46464  xlimliminflimsup  46677  cncfshift  46689  cncfperiod  46694  cncfuni  46701  icccncfext  46702  cncfiooicclem1  46708  fperdvper  46734  ioodvbdlimc1lem2  46747  ioodvbdlimc2lem  46749  mbfres2cn  46773  iblsplit  46781  stoweidlem7  46822  stoweidlem13  46828  stoweidlem26  46841  wallispilem3  46882  stirlinglem6  46894  stirlinglem10  46898  dirkercncf  46922  fourierdlem6  46928  fourierdlem11  46933  fourierdlem12  46934  fourierdlem15  46937  fourierdlem26  46948  fourierdlem42  46964  fourierdlem50  46971  fourierdlem51  46972  fourierdlem52  46973  fourierdlem54  46975  fourierdlem62  46983  fourierdlem79  47000  fourierdlem102  47023  fourierdlem114  47035  etransclem23  47072  chnsubseq  47695  3f1oss1  47950  zgeltp1eq  48184  nnmul2  48205  setsnidel  48264  preimafvsnel  48266  iccpartres  48305  prpair  48388  fpprel2  48644  isubgrsubgr  48772  grimidvtxedg  48788  grimcnv  48791  isuspgrim  48799  upgrimpthslem2  48811  stgrnbgr0  48867  uhgrimgrlim  48890  clnbgr3stgrgrlim  48922  gpg5nbgrvtx03starlem2  48972  gpg5nbgrvtx13starlem2  48975  gpg5edgnedg  49033  isassintop  49112  rhmsubcALTV  49187  srhmsubcALTV  49227  fldhmsubcALTV  49235  rmfsupp  49290  scmfsupp  49292  mptcfsupp  49294  lcoel0  49345  lincsumcl  49348  lincscmcl  49349  lcoss  49353  lindsrng01  49385  lincreslvec3  49399  lindssnlvec  49403  zgtp1leeq  49438  lubsscl  49873  glbsscl  49874  idmon  49933  idepi  49934  iinfssc  49970  iinfsubc  49971  discsubc  49977  nelsubclem  49980  imassc  50066  imasubc3  50069  isnatd  50136  swapfiso  50198  fucoppc  50323  thinciso  50383  diagciso  50452  termolmd  50583  wrdf1d  50760