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  18810  submgmid  18812  subsubmgm  18816  mgmhmima  18821  mgmhmeql  18822  mndpfsupp  18878  mnd1  18890  sgrp2nmndlem4  19044  sgrp2nmndlem5  19045  0subg  19279  nmznsg  19295  ghmpreima  19369  ghmeql  19370  ghmnsgpreima  19372  kerf1ghm  19378  cntzsgrpcl  19465  cntzsubm  19469  cntzsubg  19470  cntzmhm  19472  symgextfo  19553  symgfixf1  19568  symgfixfolem1  19569  odlem2  19670  finodsubmsubg  19698  gexlem2  19713  gexcl2  19720  sylow1lem5  19733  subgslw  19747  slwhash  19755  fislw  19756  sylow3lem1  19758  lsmsubg  19785  efgredlemd  19875  efgredlem  19878  efgcpbllemb  19886  frgpuplem  19903  cyggeninv  20014  iscygd  20018  iscygodd  20019  gsumzadd  20053  gsumconst  20065  gsumpt  20093  gsum2dlem2  20102  gsum2d  20103  gsum2d2lem  20104  dprdfcntz  20148  eldprdi  20151  subgdmdprd  20167  subgdprd  20168  dprdpr  20183  ablfac1c  20204  ablfac1eu  20206  ablfaclem3  20220  ogrpaddlt  20269  ogrpsublt  20273  ring1  20456  subrngint  20726  rhmimasubrng  20732  cntzsubrng  20733  rhmeql  20769  rhmima  20770  cntzsubr  20772  rnghmsscmap2  20795  rnghmsscmap  20796  rnghmsubcsetc  20799  zrzeroorngc  20810  rhmsscmap2  20824  rhmsscmap  20825  rhmsubcsetc  20828  rhmsscrnghm  20831  rhmsubcrngc  20834  srhmsubc  20846  rhmsubc  20855  issubdrg  20950  fldhmsubc  20955  imadrhmcl  20967  isabvd  20982  abvdiv  20999  ornglmullt  21039  orngrmullt  21040  orngmullt  21041  ofldlt1  21045  lsslsp  21203  lmhmima  21235  lmhmpreima  21236  lmhmeql  21243  lsmcl  21271  lspfixed  21319  rnglidlrng  21448  drngidl  21452  rngqiprngim  21511  rng2idl1cntr  21512  qsssubdrg  21643  gzrngunit  21650  pzriprnglem8  21705  evpmodpmf1o  21813  ocvpj  21934  dsmm0cl  21957  dsmmacl  21958  dsmmsubg  21960  dsmmlss  21961  frlmsplit2  21990  uvcff  22008  lindfrn  22038  f1lindf  22039  lindsss  22041  issubassa  22086  issubassa2  22111  snifpsrbag  22139  psrbaglesupp  22141  psrbaglecl  22142  psrbagaddcl  22143  psrbagcon  22144  psrbagres  22149  mplsubglem  22217  mpllsslem  22218  mplassa  22240  subrgmpl  22251  mplcoe5  22260  mplbas2  22262  mplind  22290  mpfind  22335  ismhp2  22373  mhpmulcl  22381  mhplss  22387  ply1assa  22428  coe1tmmul2  22506  coe1tmmul  22507  cply1coe0bi  22531  dmatid  22721  dmatsubcl  22724  dmatscmcl  22729  scmatid  22740  scmataddcl  22742  scmatsubcl  22743  scmatmulcl  22744  smatvscl  22750  scmatrhmcl  22754  mat0scmat  22764  mat1scmat  22765  mdet0pr  22818  chmaidscmat  23077  distop  23224  indistopon  23230  ppttop  23236  epttop  23238  mretopd  23321  toponmre  23322  neiss  23338  opnneissb  23343  ssnei2  23345  innei  23354  neiptoptop  23360  ordtcld1  23426  ordtcld2  23427  lmconst  23490  cnpnei  23493  iscncl  23498  cnss1  23505  cnss2  23506  cncnpi  23507  cncnp  23509  cnconst2  23512  cnrest  23514  cnpresti  23517  cnpdis  23522  paste  23523  lmcnp  23533  cnhaus  23583  hauscmp  23636  2ndcomap  23688  1stcelcls  23691  1stccnp  23692  llyrest  23715  nllyrest  23716  llyidm  23718  nllyidm  23719  ssref  23742  reftr  23744  refun0  23745  dissnref  23758  kgentopon  23768  kgenidm  23777  kgencn3  23788  txcld  23833  neitx  23837  tx1cn  23839  tx2cn  23840  ptcld  23843  xkoccn  23849  txcnp  23850  ptcnp  23852  txcnmpt  23854  ptcn  23857  txdis1cn  23865  ptrescn  23869  txkgen  23882  xkoco1cn  23887  xkoco2cn  23888  xkococn  23890  xkoinjcn  23917  qtoptop2  23929  qtopuni  23932  qtopid  23935  qtopkgen  23940  basqtop  23941  tgqtop  23942  qtopss  23945  qtopeu  23946  qtoprest  23947  kqopn  23964  kqcld  23965  kqreglem2  23972  reghmph  24023  ordthmeolem  24031  qtopf1  24046  opnfbas  24072  isfil2  24086  fbasweak  24095  fsubbas  24097  filconn  24113  fbasrn  24114  rnelfmlem  24182  flimss2  24202  flimss1  24203  hausflim  24211  flimclslem  24214  flimsncls  24216  cnpflfi  24229  flfcnp2  24237  fclsfnflim  24257  cnextfvval  24295  cnextfres1  24298  symgtgp  24336  opnsubg  24338  ghmcnp  24345  qustgpopn  24350  qustgplem  24351  qustgphaus  24353  tsmsfbas  24358  ustfilxp  24443  utoptop  24464  utopbas  24465  restutopopn  24468  iducn  24512  cstucnd  24513  ucncn  24514  fmucnd  24521  cfilufg  24522  trcfilu  24523  cfiluweak  24524  neipcfilu  24525  psmetres2  24544  isxmetd  24556  xmetpsmet  24578  imasf1oxmet  24605  xblss2ps  24631  xblss2  24632  xblcntrps  24640  xblcntr  24641  blcld  24735  metustfbas  24787  cfilucfil  24789  restmetu  24800  ngptgp  24866  tngngpd  24883  nrmtngnrm  24888  tngnrg  24904  nlmvscn  24917  nrginvrcn  24922  nmo0  24965  nmoeq0  24966  nmoid  24972  nghmcn  24975  0nmhm  24985  blcvx  25028  iccntr  25052  xrge0tsms  25065  xmetdcn2  25068  metdstri  25082  metdscn  25087  rescncf  25129  cncfco  25139  oprpiece1res2  25184  cnheibor  25187  cnllycmp  25188  bndth  25190  ishtpyd  25207  isphtpyd  25218  pcoval2  25248  nmhmcn  25352  ipcn  25478  lmnn  25495  cfilss  25502  iscfil3  25505  cfilfcls  25506  cmetcaulem  25520  iscmet3lem2  25524  cfilres  25528  lmcau  25545  flimcfil  25546  cncmet  25554  rlmbn  25593  minveclem3b  25660  pjthlem1  25669  pjth2  25672  ivthlem3  25685  ovolssnul  25719  ovolctb  25722  ovoliunnul  25739  ovolsca  25747  ovolicopnf  25756  voliunlem2  25783  volsup  25788  dyadmaxlem  25829  vitalilem5  25844  mbfres  25876  mbfss  25878  mbfmulc2re  25880  mbfadd  25893  mbfmulc2  25895  mbflim  25900  i1faddlem  25925  i1fmullem  25926  mbfmul  25958  itg2mulc  25979  itg2cnlem1  25993  ibl0  26019  iblposlem  26024  itgreval  26029  iblneg  26035  iblss  26037  iblss2  26038  itgle  26042  iblconst  26050  iblabs  26061  iblabsr  26062  iblmulc2  26063  bddmulibl  26071  limciun  26126  limcun  26127  dvres2lem  26142  dvidlem  26147  dvcnp2  26152  dvcn  26153  cpnres  26169  dvaddbr  26170  dvmulbr  26171  dvcobr  26178  dvcjbr  26181  dvrec  26187  dvcnvlem  26208  dvferm  26220  dvlip2  26227  dveq0  26232  dv11cn  26233  dvivthlem1  26240  lhop1  26246  lhop2  26247  lhop  26248  dvcnvre  26251  dvfsumlem3  26260  dvfsumlem4  26261  dvfsumrlim  26263  dvfsum2  26266  ftc1a  26269  ftc1lem4  26271  ftc1lem6  26273  ftc1  26274  coe1mul3  26329  deg1addle2  26332  deg1sublt  26340  fta1blem  26401  drnguc1p  26404  ig1prsp  26411  plyco0  26422  plyeq0lem  26440  dgrub  26464  dgreq  26474  dgradd2  26498  dgrmul  26500  dgrcolem2  26504  dgrco  26505  plycpn  26523  plydivlem4  26530  plydiveu  26532  vieta1lem2  26545  vieta1  26546  aalioulem2  26569  aalioulem3  26570  aaliou3lem7  26585  tayl0  26598  ulmcn  26635  ulmdvlem3  26638  psercn  26662  abelth  26677  pilem3  26689  efif1olem1  26780  abslogimle  26811  argregt0  26848  argrege0  26849  logf1o2  26888  cxpsqrtlem  26940  cxpcn3  26986  abscxpbnd  26991  logreclem  27000  ang180lem2  27048  ang180lem3  27049  xrlimcnp  27206  harmonicbnd4  27248  fsumharmonic  27249  lgamgulmlem5  27270  lgambdd  27274  basellem4  27321  dvdsppwf1o  27423  dvdsflf1o  27424  fsumfldivdiaglem  27426  chpeq0  27445  chteq0  27446  chtub  27449  chpub  27457  dchrelbasd  27476  dchrmulcl  27486  dchrinv  27498  bposlem1  27521  bposlem2  27522  lgsdirprm  27568  lgsqrlem2  27584  lgsqrlem3  27585  lgsdchr  27592  lgseisenlem1  27612  lgseisenlem2  27613  lgseisenlem3  27614  lgsquadlem1  27617  2sqlem8  27663  2sqblem  27668  2sqmod  27673  chebbnd1lem1  27706  dchrisumlem1  27726  dchrisumlem2  27727  dchrisumlem3  27728  dchrisum0fno1  27748  pntrmax  27801  pntpbnd1a  27822  pntibndlem3  27829  pntlemn  27837  pntlemi  27841  pntlem3  27846  pntleml  27848  ostth1  27870  ostth2  27874  ostth3  27875  nosepon  27902  nolesgn2ores  27909  nogesgn1ores  27911  nosupres  27944  nosupbnd1lem2  27946  nosupbnd2lem1  27952  noinfres  27959  noinfbnd1lem2  27961  noinfbnd2lem1  27967  eqcuts3  28070  cofcutrtime  28193  divmuldivsd  28498  divdivs1d  28499  onsbnd  28547  nnsgt0  28605  bdayfinbndlem1  28733  ercgrg  28860  motco  28883  cnvmot  28884  legso  28942  mirmot  29027  colopp  29127  hphl  29129  lmicom  29173  lmimid  29179  lmimot  29183  hypcgrlem1  29185  hypcgrlem2  29186  trgcopyeulem  29192  inagswap  29240  inaghl  29244  cgrg3col4  29252  prlngd  29297  prlngref  29298  dfprlng2  29305  brbtwn2  29363  axlowdimlem3  29402  axlowdimlem16  29415  axcontlem8  29429  fusgrfis  29791  nbgr2vtx1edg  29811  0vtxrgr  30037  0vtxrusgr  30038  ewlkle  30066  wlk1ewlk  30100  uspgr2wlkeq2  30107  wlkp1lem8  30139  trlontrl  30173  pthonpth  30214  pthdlem2  30234  wlklnwwlkln1  30337  wlknewwlksn  30356  wwlksnred  30361  wwlksnredwwlkn0  30365  2trlond  30408  2pthond  30411  elwwlks2ons3im  30423  clwlkclwwlklem2a1  30463  clwlkclwwlkf1  30481  clwwlkel  30517  clwwlkwwlksb  30525  wwlksext2clwwlk  30528  1ewlk  30586  0trlon  30595  0pthon  30598  1pthond  30615  3trlond  30654  3pthond  30656  3spthond  30658  eupthres  30696  2clwwlk2clwwlk  30831  numclwwlk1lem2foa  30835  numclwwlk1lem2f1  30838  nvabs  31154  vacn  31176  nmcvcn  31177  nmblore  31268  0lno  31272  0blo  31274  nmlno0lem  31275  occl  31786  pjhthlem1  31873  pjpjpre  31901  nmopre  32352  nmlnop0iALT  32477  nmophmi  32513  leoprf2  32609  stlesi  32723  disjdifprg  33050  disjun0  33070  fsuppcurry1  33197  fsuppcurry2  33198  fpwrelmap  33206  fzspl  33262  dfmgc2lem  33437  pwrssmgc  33442  xrge0tsmsd  33515  psgnfzto1stlem  33542  fzto1st1  33544  evpmid  33590  pnfinf  33625  isarchiofld  33641  rmfsupp2  33679  fracfld  33751  dvdsruassoi  33819  nsgmgc  33843  qsdrngi  33899  deg1addlt  34012  ply1degltdimlem  34134  lbsdiflsp0  34138  fedgmul  34143  fldexttr  34170  fldextid  34171  irngnzply1lem  34202  finextalg  34210  minplyelirng  34227  irredminply  34228  algextdeglem8  34236  rtelextdg2lem  34238  constrsslem  34253  constrllcllem  34264  constrlccllem  34265  constrcccllem  34266  qtopt1  34347  reff  34351  locfinreflem  34352  metideq  34405  metider  34406  pstmxmet  34409  qqhval2lem  34493  qqhcn  34503  qqhucn  34504  pwsiga  34642  prsiga  34643  measle0  34721  mbfmcst  34772  1stmbfm  34773  2ndmbfm  34774  imambfm  34775  cnmbfm  34776  mbfmco  34777  mbfmco2  34778  0elcarsg  34820  carsgclctun  34834  sibfof  34853  oddpwdc  34867  eulerpartlemmf  34888  eulerpartlemgs2  34893  0rrv  34964  ballotlemfc0  35006  ballotlemfcc  35007  signstfveq0  35087  breprexplemc  35142  bnj1452  35563  usgrgt2cycl  35725  acycgr1v  35730  derangen  35753  subfacval3  35770  cvmseu  35857  cvmliftmolem2  35863  cvmliftlem7  35872  cvmliftlem15  35879  cvmlift2lem9a  35884  cvmlift2lem9  35892  cvmlift2lem10  35893  cvmlift2lem11  35894  cvmlift2lem12  35895  cvmlift3lem6  35905  cvmlift3lem8  35907  ex-sategoelel  36002  ex-sategoelelomsuc  36007  mclsppslem  36164  mclspps  36165  wsuclem  36404  nadddilem2  36803  fness  36970  fnetr  36972  fnessref  36978  refssfne  36979  neibastop1  36980  neibastop2  36982  tailfb  36998  filnetlem3  37001  weiunfrlem  37085  bj-finsumval0  38039  bj-rvecvec  38053  dfgcd3  38078  lindsadd  38369  poimirlem13  38384  poimirlem15  38386  poimirlem24  38395  poimirlem28  38399  mblfinlem2  38409  ovoliunnfl  38413  volsupnfl  38416  mbfresfi  38417  iblabsnc  38435  iblmulc2nc  38436  ftc1cnnclem  38442  ftc1cnnc  38443  ftc1anc  38452  sdclem2  38494  metf1o  38507  ismtyhmeolem  38556  ismtyres  38560  heibor1lem  38561  bfplem2  38575  bfp  38576  rrncmslem  38584  iccbnd  38592  icccmpALT  38593  rngogrphom  38723  rngoisoco  38734  keridl  38784  lsmcv2  39904  lsatcv0  39906  lcvexchlem4  39912  lcvexchlem5  39913  l1cvpat  39929  lfl0f  39944  lfladdcl  39946  lflnegcl  39950  lkrlss  39970  eqlkr  39974  lkrlsp  39977  lkrlsp2  39978  lshpkrcl  39991  lkrin  40039  1cvrjat  40350  llni  40383  llnle  40393  lplni  40407  lplnle  40415  llncvrlpln2  40432  2atmat  40436  lvoli  40450  lplncvrlvol2  40490  elpaddri  40677  paddclN  40717  pclclN  40766  pclfinN  40775  0psubclN  40818  1psubclN  40819  atpsubclN  40820  pmapsubclN  40821  osumclN  40842  pexmidN  40844  pexmidlem6N  40850  lhp2lt  40876  lautcnv  40965  idlaut  40971  lautco  40972  idldil  40989  ldilcnv  40990  ldilco  40991  ltrncnv  41021  idltrn  41025  cdleme16d  41156  cdleme50laut  41422  cdleme50ldil  41423  cdleme50ltrn  41432  ltrnco  41594  dian0  41914  dia0eldmN  41915  dia1eldmN  41916  dialss  41921  diaintclN  41933  docaclN  41999  doca2N  42001  djajN  42012  dibintclN  42042  diblss  42045  dicvaddcl  42065  dicvscacl  42066  dicn0  42067  cdlemn11a  42082  dihord2cN  42096  dihord11b  42097  dihord6apre  42131  dihmeetlem1N  42165  dihglblem5apreN  42166  dihpN  42211  dihjatcclem4  42296  dochkr1  42353  islpoldN  42359  lcfrlem31  42448  mapdpglem18  42564  mapdheq2  42604  mapdheq4  42607  mapdh6aN  42610  hdmap1l6a  42684  hdmap14lem4a  42746  lcmineqlem4  42900  frlmfzoccat  43395  drnginvmuld  43411  evlselvlem  43436  evlselv  43437  fsuppind  43438  fsuppssind  43441  prjspvs  43458  irrapxlem4  43668  pell1234qrdich  43704  pell1qr1  43714  pell14qrgap  43718  pellqrexplicit  43720  rmspecfund  43752  fzmaxdif  43824  acongeq  43826  jm2.23  43839  jm3.1  43863  lmhmlnmsplit  43930  hbt  43973  dgrsub2  43978  proot1ex  44039  cantnfub  44164  cantnfresb  44167  cantnf2  44168  tfsconcatfv2  44183  tfsconcatrn  44185  tfsconcatb0  44187  naddcnff  44205  naddcnffo  44207  naddcnfid1  44210  naddcnfid2  44211  clublem  44452  dftrcl3  44562  mnugrud  45110  hashnzfz2  45147  dvconstbi  45160  ubelsupr  45856  restopn3  45985  wessf1ornlem  46019  lefldiveq  46127  iccintsng  46355  climsuse  46440  mullimc  46448  limcdm0  46450  limccog  46452  mullimcf  46455  constlimc  46456  idlimc  46458  limcperiod  46460  limsupre  46471  limcleqr  46474  neglimc  46477  addlimc  46478  0ellimcdiv  46479  xlimliminflimsup  46692  cncfshift  46704  cncfperiod  46709  cncfuni  46716  icccncfext  46717  cncfiooicclem1  46723  fperdvper  46749  ioodvbdlimc1lem2  46762  ioodvbdlimc2lem  46764  mbfres2cn  46788  iblsplit  46796  stoweidlem7  46837  stoweidlem13  46843  stoweidlem26  46856  wallispilem3  46897  stirlinglem6  46909  stirlinglem10  46913  dirkercncf  46937  fourierdlem6  46943  fourierdlem11  46948  fourierdlem12  46949  fourierdlem15  46952  fourierdlem26  46963  fourierdlem42  46979  fourierdlem50  46986  fourierdlem51  46987  fourierdlem52  46988  fourierdlem54  46990  fourierdlem62  46998  fourierdlem79  47015  fourierdlem102  47038  fourierdlem114  47050  etransclem23  47087  chnsubseq  47710  3f1oss1  47965  zgeltp1eq  48199  nnmul2  48220  setsnidel  48279  preimafvsnel  48281  iccpartres  48320  prpair  48403  fpprel2  48659  isubgrsubgr  48787  grimidvtxedg  48803  grimcnv  48806  isuspgrim  48814  upgrimpthslem2  48826  stgrnbgr0  48882  uhgrimgrlim  48905  clnbgr3stgrgrlim  48937  gpg5nbgrvtx03starlem2  48987  gpg5nbgrvtx13starlem2  48990  gpg5edgnedg  49048  isassintop  49127  rhmsubcALTV  49202  srhmsubcALTV  49242  fldhmsubcALTV  49250  rmfsupp  49305  scmfsupp  49307  mptcfsupp  49309  lcoel0  49360  lincsumcl  49363  lincscmcl  49364  lcoss  49368  lindsrng01  49400  lincreslvec3  49414  lindssnlvec  49418  zgtp1leeq  49453  lubsscl  49888  glbsscl  49889  idmon  49948  idepi  49949  iinfssc  49985  iinfsubc  49986  discsubc  49992  nelsubclem  49995  imassc  50081  imasubc3  50084  isnatd  50151  swapfiso  50213  fucoppc  50338  thinciso  50398  diagciso  50467  termolmd  50598  wrdf1d  50775