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  7006  fveqressseq  7026  fmptsng  7116  fmptsnd  7117  fnprb  7156  fntpb  7157  fpr3g  8229  frrlem4  8233  1ellim  8427  isfsuppd  9273  fdmfifsupp  9282  fczfsuppd  9293  fsuppmptif  9306  fsuppco2  9310  fsuppcor  9311  dffi3  9338  suppr  9379  infpr  9412  ordtypelem7  9433  cantnf0  9588  cantnfp1lem1  9591  cantnfp1lem2  9592  cantnfp1lem3  9593  cantnflem1a  9598  cantnflem1d  9601  cantnflem1  9602  cantnf  9606  rankpwi  9739  carduni  9897  fin23lem32  10258  fpwwe2lem5  10550  fpwwe2lem11  10556  fpwwe2lem12  10557  fpwwe2  10558  inttsk  10689  grutsk1  10736  add20  11653  supaddc  12113  supadd  12114  supmul  12118  suprzcl  12576  uzid  12770  uzwo3  12860  rpnnen1lem5  12898  xrletrid  13073  xrre  13088  xrre3  13090  xleadd1a  13172  xlemul1a  13207  elioc2  13329  elico2  13330  elicc2  13331  elfz1eq  13455  fzadd2  13479  fznatpl1  13498  elfz1uz  13514  nn0fz0  13545  fzctr  13560  fzo1fzo0n0  13635  fzoaddel  13637  elincfzoext  13643  flid  13732  flval3  13739  fladdz  13749  fldiv  13784  modid  13820  hashf1lem1  14382  pfxccatin12d  14672  repswpfx  14712  2cshw  14740  pfx2  14874  wwlktovf1  14884  sqeqd  15093  01sqrexlem7  15175  max0add  15237  abs2difabs  15262  rddif  15268  fzomaxdiflem  15270  rexico  15281  icodiamlt  15365  limsupgre  15408  rlim3  15425  icco1  15467  rlimclim  15473  rlimuni  15477  rlimresb  15492  isercolllem2  15593  isercolllem3  15594  isercoll  15595  caucvgrlem  15600  caurcvgr  15601  iseraltlem3  15611  fsum00  15725  o1fsum  15740  bitsfzolem  16365  bitsfzo  16366  bitsmod  16367  bitscmp  16369  gcd0id  16450  gcdneg  16453  bezoutlem4  16473  nn0seqcvgd  16501  lcmneg  16534  lcmfunsnlem2lem2  16570  qredeq  16588  prmind2  16616  eulerthlem2  16713  pcpremul  16775  pcidlem  16804  pcgcd1  16809  fldivp1  16829  pcfaclem  16830  4sqlem17  16893  vdwlem1  16913  vdwlem6  16918  vdwlem12  16924  vdwlem13  16925  0ram  16952  ram0  16954  ramub1lem1  16958  invco  17699  sectmon  17710  monsect  17711  invid  17715  ssctr  17753  ssceq  17754  0ssc  17765  0subcat  17766  catsubcat  17767  issubc3  17777  fullsubc  17778  funcinv  17801  fthmon  17857  fuccocl  17895  fucidcl  17896  invfuc  17905  2initoinv  17938  2termoinv  17945  elhomai  17961  setcmon  18015  setcepi  18016  catcisolem  18038  curf2cl  18158  yonedalem4c  18204  yonedalem3  18207  yoniso  18212  lublecl  18286  isacs3lem  18469  tsrdir  18531  chnccat  18553  rabsubmgmd  18633  submgmid  18635  subsubmgm  18639  mgmhmima  18644  mgmhmeql  18645  mndpfsupp  18696  mnd1  18708  sgrp2nmndlem4  18857  sgrp2nmndlem5  18858  0subg  19085  nmznsg  19101  ghmpreima  19171  ghmeql  19172  ghmnsgpreima  19174  kerf1ghm  19180  cntzsgrpcl  19267  cntzsubm  19271  cntzsubg  19272  cntzmhm  19274  symgextfo  19355  symgfixf1  19370  symgfixfolem1  19371  odlem2  19472  finodsubmsubg  19500  gexlem2  19515  gexcl2  19522  sylow1lem5  19535  subgslw  19549  slwhash  19557  fislw  19558  sylow3lem1  19560  lsmsubg  19587  efgredlemd  19677  efgredlem  19680  efgcpbllemb  19688  frgpuplem  19705  cyggeninv  19816  iscygd  19820  iscygodd  19821  gsumzadd  19855  gsumconst  19867  gsumpt  19895  gsum2dlem2  19904  gsum2d  19905  gsum2d2lem  19906  dprdfcntz  19950  eldprdi  19953  subgdmdprd  19969  subgdprd  19970  dprdpr  19985  ablfac1c  20006  ablfac1eu  20008  ablfaclem3  20022  ogrpaddlt  20071  ogrpsublt  20075  ring1  20249  subrngint  20497  rhmimasubrng  20503  cntzsubrng  20504  rhmeql  20540  rhmima  20541  cntzsubr  20543  rnghmsscmap2  20566  rnghmsscmap  20567  rnghmsubcsetc  20570  zrzeroorngc  20581  rhmsscmap2  20595  rhmsscmap  20596  rhmsubcsetc  20599  rhmsscrnghm  20602  rhmsubcrngc  20605  srhmsubc  20617  rhmsubc  20626  issubdrg  20717  fldhmsubc  20722  imadrhmcl  20734  isabvd  20749  abvdiv  20766  ornglmullt  20806  orngrmullt  20807  orngmullt  20808  ofldlt1  20812  lsslsp  20970  lsslspOLD  20971  lmhmima  21003  lmhmpreima  21004  lmhmeql  21011  lsmcl  21039  lspfixed  21087  rnglidlrng  21206  rngqiprngim  21263  rng2idl1cntr  21264  qsssubdrg  21385  gzrngunit  21392  pzriprnglem8  21447  evpmodpmf1o  21555  ocvpj  21676  dsmm0cl  21699  dsmmacl  21700  dsmmsubg  21702  dsmmlss  21703  frlmsplit2  21732  uvcff  21750  lindfrn  21780  f1lindf  21781  lindsss  21783  issubassa  21826  issubassa2  21852  snifpsrbag  21880  psrbaglesupp  21882  psrbaglecl  21883  psrbagaddcl  21884  psrbagcon  21885  mplsubglem  21958  mpllsslem  21959  mplassa  21981  subrgmpl  21991  mplcoe5  21999  mplbas2  22001  mplind  22029  mpfind  22074  ismhp2  22088  mhpmulcl  22096  mhplss  22102  ply1assa  22144  coe1tmmul2  22222  coe1tmmul  22223  cply1coe0bi  22250  dmatid  22443  dmatsubcl  22446  dmatscmcl  22451  scmatid  22462  scmataddcl  22464  scmatsubcl  22465  scmatmulcl  22466  smatvscl  22472  scmatrhmcl  22476  mat0scmat  22486  mat1scmat  22487  mdet0pr  22540  chmaidscmat  22796  distop  22943  indistopon  22949  ppttop  22955  epttop  22957  mretopd  23040  toponmre  23041  neiss  23057  opnneissb  23062  ssnei2  23064  innei  23073  neiptoptop  23079  ordtcld1  23145  ordtcld2  23146  lmconst  23209  cnpnei  23212  iscncl  23217  cnss1  23224  cnss2  23225  cncnpi  23226  cncnp  23228  cnconst2  23231  cnrest  23233  cnpresti  23236  cnpdis  23241  paste  23242  lmcnp  23252  cnhaus  23302  hauscmp  23355  2ndcomap  23406  1stcelcls  23409  1stccnp  23410  llyrest  23433  nllyrest  23434  llyidm  23436  nllyidm  23437  ssref  23460  reftr  23462  refun0  23463  dissnref  23476  kgentopon  23486  kgenidm  23495  kgencn3  23506  txcld  23551  neitx  23555  tx1cn  23557  tx2cn  23558  ptcld  23561  xkoccn  23567  txcnp  23568  ptcnp  23570  txcnmpt  23572  ptcn  23575  txdis1cn  23583  ptrescn  23587  txkgen  23600  xkoco1cn  23605  xkoco2cn  23606  xkococn  23608  xkoinjcn  23635  qtoptop2  23647  qtopuni  23650  qtopid  23653  qtopkgen  23658  basqtop  23659  tgqtop  23660  qtopss  23663  qtopeu  23664  qtoprest  23665  kqopn  23682  kqcld  23683  kqreglem2  23690  reghmph  23741  ordthmeolem  23749  qtopf1  23764  opnfbas  23790  isfil2  23804  fbasweak  23813  fsubbas  23815  filconn  23831  fbasrn  23832  rnelfmlem  23900  flimss2  23920  flimss1  23921  hausflim  23929  flimclslem  23932  flimsncls  23934  cnpflfi  23947  flfcnp2  23955  fclsfnflim  23975  cnextfvval  24013  cnextfres1  24016  symgtgp  24054  opnsubg  24056  ghmcnp  24063  qustgpopn  24068  qustgplem  24069  qustgphaus  24071  tsmsfbas  24076  ustfilxp  24161  utoptop  24182  utopbas  24183  restutopopn  24186  iducn  24230  cstucnd  24231  ucncn  24232  fmucnd  24239  cfilufg  24240  trcfilu  24241  cfiluweak  24242  neipcfilu  24243  psmetres2  24262  isxmetd  24274  xmetpsmet  24296  imasf1oxmet  24323  xblss2ps  24349  xblss2  24350  xblcntrps  24358  xblcntr  24359  blcld  24453  metustfbas  24505  cfilucfil  24507  restmetu  24518  ngptgp  24584  tngngpd  24601  nrmtngnrm  24606  tngnrg  24622  nlmvscn  24635  nrginvrcn  24640  nmo0  24683  nmoeq0  24684  nmoid  24690  nghmcn  24693  0nmhm  24703  blcvx  24746  iccntr  24770  xrge0tsms  24783  xmetdcn2  24786  metdstri  24800  metdscn  24805  rescncf  24850  cncfco  24860  oprpiece1res2  24910  cnheibor  24914  cnllycmp  24915  bndth  24917  ishtpyd  24934  isphtpyd  24945  pcoval2  24976  nmhmcn  25080  ipcn  25206  lmnn  25223  cfilss  25230  iscfil3  25233  cfilfcls  25234  cmetcaulem  25248  iscmet3lem2  25252  cfilres  25256  lmcau  25273  flimcfil  25274  cncmet  25282  rlmbn  25321  minveclem3b  25388  pjthlem1  25397  pjth2  25400  ivthlem3  25414  ovolssnul  25448  ovolctb  25451  ovoliunnul  25468  ovolsca  25476  ovolicopnf  25485  voliunlem2  25512  volsup  25517  dyadmaxlem  25558  vitalilem5  25573  mbfres  25605  mbfss  25607  mbfmulc2re  25609  mbfadd  25622  mbfmulc2  25624  mbflim  25629  i1faddlem  25654  i1fmullem  25655  mbfmul  25687  itg2mulc  25708  itg2cnlem1  25722  ibl0  25748  iblposlem  25753  itgreval  25758  iblneg  25764  iblss  25766  iblss2  25767  itgle  25771  iblconst  25779  iblabs  25790  iblabsr  25791  iblmulc2  25792  bddmulibl  25800  limciun  25855  limcun  25856  dvres2lem  25871  dvidlem  25876  dvcnp2  25881  dvcnp2OLD  25882  dvcn  25883  cpnres  25899  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvcobr  25909  dvcobrOLD  25910  dvcjbr  25913  dvrec  25919  dvcnvlem  25940  dvferm  25952  dvlip2  25960  dveq0  25965  dv11cn  25966  dvivthlem1  25973  lhop1  25979  lhop2  25980  lhop  25981  dvcnvre  25984  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  26234  dgrmul  26236  dgrcolem2  26240  dgrco  26241  plycpn  26257  plydivlem4  26264  plydiveu  26266  vieta1lem2  26279  vieta1  26280  aalioulem2  26301  aalioulem3  26302  aaliou3lem7  26317  tayl0  26329  ulmcn  26368  ulmdvlem3  26371  psercn  26396  abelth  26411  pilem3  26423  efif1olem1  26511  abslogimle  26542  argregt0  26579  argrege0  26580  logf1o2  26619  cxpsqrtlem  26671  cxpcn3  26718  abscxpbnd  26723  logreclem  26732  ang180lem2  26780  ang180lem3  26781  xrlimcnp  26938  harmonicbnd4  26981  fsumharmonic  26982  lgamgulmlem5  27003  lgambdd  27007  basellem4  27054  dvdsppwf1o  27156  dvdsflf1o  27157  fsumfldivdiaglem  27159  chpeq0  27179  chteq0  27180  chtub  27183  chpub  27191  dchrelbasd  27210  dchrmulcl  27220  dchrinv  27232  bposlem1  27255  bposlem2  27256  lgsdirprm  27302  lgsqrlem2  27318  lgsqrlem3  27319  lgsdchr  27326  lgseisenlem1  27346  lgseisenlem2  27347  lgseisenlem3  27348  lgsquadlem1  27351  2sqlem8  27397  2sqblem  27402  2sqmod  27407  chebbnd1lem1  27440  dchrisumlem1  27460  dchrisumlem2  27461  dchrisumlem3  27462  dchrisum0fno1  27482  pntrmax  27535  pntpbnd1a  27556  pntibndlem3  27563  pntlemn  27571  pntlemi  27575  pntlem3  27580  pntleml  27582  ostth1  27604  ostth2  27608  ostth3  27609  nosepon  27637  nolesgn2ores  27644  nogesgn1ores  27646  nosupres  27679  nosupbnd1lem2  27681  nosupbnd2lem1  27687  noinfres  27694  noinfbnd1lem2  27696  noinfbnd2lem1  27702  eqscut3  27802  cofcutrtime  27909  divmuldivsd  28213  divdivs1d  28214  onsbnd  28262  nnsgt0  28319  bdayfinbndlem1  28446  ercgrg  28572  motco  28595  cnvmot  28596  legso  28654  mirmot  28730  colopp  28824  hphl  28826  lmicom  28843  lmimid  28849  lmimot  28853  hypcgrlem1  28854  hypcgrlem2  28855  trgcopyeulem  28860  inagswap  28896  inaghl  28900  cgrg3col4  28908  brbtwn2  28961  axlowdimlem3  29000  axlowdimlem16  29013  axcontlem8  29027  fusgrfis  29386  nbgr2vtx1edg  29406  0vtxrgr  29633  0vtxrusgr  29634  ewlkle  29662  wlk1ewlk  29696  uspgr2wlkeq2  29703  wlkp1lem8  29735  trlontrl  29765  pthonpth  29804  pthdlem2  29824  wlklnwwlkln1  29924  wlknewwlksn  29943  wwlksnred  29948  wwlksnredwwlkn0  29952  2trlond  29995  2pthond  29998  elwwlks2ons3im  30010  clwlkclwwlklem2a1  30050  clwlkclwwlkf1  30068  clwwlkel  30104  clwwlkwwlksb  30112  wwlksext2clwwlk  30115  1ewlk  30173  0trlon  30182  0pthon  30185  1pthond  30202  3trlond  30231  3pthond  30233  3spthond  30235  eupthres  30273  2clwwlk2clwwlk  30408  numclwwlk1lem2foa  30412  numclwwlk1lem2f1  30415  nvabs  30730  vacn  30752  nmcvcn  30753  nmblore  30844  0lno  30848  0blo  30850  nmlno0lem  30851  occl  31362  pjhthlem1  31449  pjpjpre  31477  nmopre  31928  nmlnop0iALT  32053  nmophmi  32089  leoprf2  32185  stlesi  32299  disjdifprg  32632  disjun0  32652  fsuppcurry1  32784  fsuppcurry2  32785  fpwrelmap  32793  fzspl  32850  dfmgc2lem  33058  pwrssmgc  33063  xrge0tsmsd  33136  psgnfzto1stlem  33163  fzto1st1  33165  evpmid  33211  pnfinf  33246  isarchiofld  33262  rmfsupp2  33301  fracfld  33371  dvdsruassoi  33446  nsgmgc  33474  drngidl  33495  qsdrngi  33557  deg1addlt  33662  ply1degltdimlem  33760  lbsdiflsp0  33764  fedgmul  33769  fldexttr  33796  fldextid  33797  irngnzply1lem  33828  finextalg  33836  minplyelirng  33853  irredminply  33854  algextdeglem8  33862  rtelextdg2lem  33864  constrsslem  33879  constrllcllem  33890  constrlccllem  33891  constrcccllem  33892  qtopt1  33973  reff  33977  locfinreflem  33978  metideq  34031  metider  34032  pstmxmet  34035  qqhval2lem  34119  qqhcn  34129  qqhucn  34130  pwsiga  34268  prsiga  34269  measle0  34346  mbfmcst  34397  1stmbfm  34398  2ndmbfm  34399  imambfm  34400  cnmbfm  34401  mbfmco  34402  mbfmco2  34403  0elcarsg  34445  carsgclctun  34459  sibfof  34478  oddpwdc  34492  eulerpartlemmf  34513  eulerpartlemgs2  34518  0rrv  34589  ballotlemfc0  34631  ballotlemfcc  34632  signstfveq0  34715  breprexplemc  34770  bnj1452  35189  usgrgt2cycl  35305  acycgr1v  35324  derangen  35347  subfacval3  35364  cvmseu  35451  cvmliftmolem2  35457  cvmliftlem7  35466  cvmliftlem15  35473  cvmlift2lem9a  35478  cvmlift2lem9  35486  cvmlift2lem10  35487  cvmlift2lem11  35488  cvmlift2lem12  35489  cvmlift3lem6  35499  cvmlift3lem8  35501  ex-sategoelel  35596  ex-sategoelelomsuc  35601  mclsppslem  35758  mclspps  35759  wsuclem  35998  fness  36524  fnetr  36526  fnessref  36532  refssfne  36533  neibastop1  36534  neibastop2  36536  tailfb  36552  filnetlem3  36555  weiunfrlem  36639  bj-finsumval0  37461  bj-rvecvec  37475  dfgcd3  37500  lindsadd  37785  poimirlem13  37805  poimirlem15  37807  poimirlem24  37816  poimirlem28  37820  mblfinlem2  37830  ovoliunnfl  37834  volsupnfl  37837  mbfresfi  37838  iblabsnc  37856  iblmulc2nc  37857  ftc1cnnclem  37863  ftc1cnnc  37864  ftc1anc  37873  sdclem2  37914  metf1o  37927  ismtyhmeolem  37976  ismtyres  37980  heibor1lem  37981  bfplem2  37995  bfp  37996  rrncmslem  38004  iccbnd  38012  icccmpALT  38013  rngogrphom  38143  rngoisoco  38154  keridl  38204  lsmcv2  39326  lsatcv0  39328  lcvexchlem4  39334  lcvexchlem5  39335  l1cvpat  39351  lfl0f  39366  lfladdcl  39368  lflnegcl  39372  lkrlss  39392  eqlkr  39396  lkrlsp  39399  lkrlsp2  39400  lshpkrcl  39413  lkrin  39461  1cvrjat  39772  llni  39805  llnle  39815  lplni  39829  lplnle  39837  llncvrlpln2  39854  2atmat  39858  lvoli  39872  lplncvrlvol2  39912  elpaddri  40099  paddclN  40139  pclclN  40188  pclfinN  40197  0psubclN  40240  1psubclN  40241  atpsubclN  40242  pmapsubclN  40243  osumclN  40264  pexmidN  40266  pexmidlem6N  40272  lhp2lt  40298  lautcnv  40387  idlaut  40393  lautco  40394  idldil  40411  ldilcnv  40412  ldilco  40413  ltrncnv  40443  idltrn  40447  cdleme16d  40578  cdleme50laut  40844  cdleme50ldil  40845  cdleme50ltrn  40854  ltrnco  41016  dian0  41336  dia0eldmN  41337  dia1eldmN  41338  dialss  41343  diaintclN  41355  docaclN  41421  doca2N  41423  djajN  41434  dibintclN  41464  diblss  41467  dicvaddcl  41487  dicvscacl  41488  dicn0  41489  cdlemn11a  41504  dihord2cN  41518  dihord11b  41519  dihord6apre  41553  dihmeetlem1N  41587  dihglblem5apreN  41588  dihpN  41633  dihjatcclem4  41718  dochkr1  41775  islpoldN  41781  lcfrlem31  41870  mapdpglem18  41986  mapdheq2  42026  mapdheq4  42029  mapdh6aN  42032  hdmap1l6a  42106  hdmap14lem4a  42168  lcmineqlem4  42323  frlmfzoccat  42796  drnginvmuld  42818  psrbagres  42835  evlselvlem  42865  evlselv  42866  fsuppind  42869  fsuppssind  42872  prjspvs  42889  irrapxlem4  43103  pell1234qrdich  43139  pell1qr1  43149  pell14qrgap  43153  pellqrexplicit  43155  rmspecfund  43187  fzmaxdif  43259  acongeq  43261  jm2.23  43274  jm3.1  43298  lmhmlnmsplit  43365  hbt  43408  dgrsub2  43413  proot1ex  43474  cantnfub  43599  cantnfresb  43602  cantnf2  43603  tfsconcatfv2  43618  tfsconcatrn  43620  tfsconcatb0  43622  naddcnff  43640  naddcnffo  43642  naddcnfid1  43645  naddcnfid2  43646  clublem  43887  dftrcl3  43997  mnugrud  44561  hashnzfz2  44598  dvconstbi  44611  ubelsupr  45301  restopn3  45431  wessf1ornlem  45465  lefldiveq  45576  iccintsng  45805  climsuse  45890  mullimc  45898  limcdm0  45900  limccog  45902  mullimcf  45905  constlimc  45906  idlimc  45908  limcperiod  45910  limsupre  45921  limcleqr  45924  neglimc  45927  addlimc  45928  0ellimcdiv  45929  xlimliminflimsup  46142  cncfshift  46154  cncfperiod  46159  cncfuni  46166  icccncfext  46167  cncfiooicclem1  46173  fperdvper  46199  ioodvbdlimc1lem2  46212  ioodvbdlimc2lem  46214  mbfres2cn  46238  iblsplit  46246  stoweidlem7  46287  stoweidlem13  46293  stoweidlem26  46306  wallispilem3  46347  stirlinglem6  46359  stirlinglem10  46363  dirkercncf  46387  fourierdlem6  46393  fourierdlem11  46398  fourierdlem12  46399  fourierdlem15  46402  fourierdlem26  46413  fourierdlem42  46429  fourierdlem50  46436  fourierdlem51  46437  fourierdlem52  46438  fourierdlem54  46440  fourierdlem62  46448  fourierdlem79  46465  fourierdlem102  46488  fourierdlem114  46500  etransclem23  46537  chnsubseq  47160  3f1oss1  47357  zgeltp1eq  47591  setsnidel  47659  preimafvsnel  47661  iccpartres  47700  prpair  47783  fpprel2  48023  isubgrsubgr  48151  grimidvtxedg  48167  grimcnv  48170  isuspgrim  48178  upgrimpthslem2  48190  stgrnbgr0  48246  uhgrimgrlim  48269  clnbgr3stgrgrlim  48301  gpg5nbgrvtx03starlem2  48351  gpg5nbgrvtx13starlem2  48354  gpg5edgnedg  48412  isassintop  48492  rhmsubcALTV  48567  srhmsubcALTV  48607  fldhmsubcALTV  48615  rmfsupp  48655  scmfsupp  48657  mptcfsupp  48659  lcoel0  48710  lincsumcl  48713  lincscmcl  48714  lcoss  48718  lindsrng01  48750  lincreslvec3  48764  lindssnlvec  48768  zgtp1leeq  48803  lubsscl  49241  glbsscl  49242  idmon  49301  idepi  49302  iinfssc  49338  iinfsubc  49339  discsubc  49345  nelsubclem  49348  imassc  49434  imasubc3  49437  isnatd  49504  swapfiso  49566  fucoppc  49691  thinciso  49751  diagciso  49820  termolmd  49951