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  7117  fmptsnd  7118  fnprb  7157  fntpb  7158  fpr3g  8230  frrlem4  8234  1ellim  8428  isfsuppd  9274  fdmfifsupp  9283  fczfsuppd  9294  fsuppmptif  9307  fsuppco2  9311  fsuppcor  9312  dffi3  9339  suppr  9380  infpr  9413  ordtypelem7  9434  cantnf0  9589  cantnfp1lem1  9592  cantnfp1lem2  9593  cantnfp1lem3  9594  cantnflem1a  9599  cantnflem1d  9602  cantnflem1  9603  cantnf  9607  rankpwi  9740  carduni  9898  fin23lem32  10259  fpwwe2lem5  10551  fpwwe2lem11  10557  fpwwe2lem12  10558  fpwwe2  10559  inttsk  10690  grutsk1  10737  add20  11654  supaddc  12114  supadd  12115  supmul  12119  suprzcl  12577  uzid  12771  uzwo3  12861  rpnnen1lem5  12899  xrletrid  13074  xrre  13089  xrre3  13091  xleadd1a  13173  xlemul1a  13208  elioc2  13330  elico2  13331  elicc2  13332  elfz1eq  13456  fzadd2  13480  fznatpl1  13499  elfz1uz  13515  nn0fz0  13546  fzctr  13561  fzo1fzo0n0  13636  fzoaddel  13638  elincfzoext  13644  flid  13733  flval3  13740  fladdz  13750  fldiv  13785  modid  13821  hashf1lem1  14383  pfxccatin12d  14673  repswpfx  14713  2cshw  14741  pfx2  14875  wwlktovf1  14885  sqeqd  15094  01sqrexlem7  15176  max0add  15238  abs2difabs  15263  rddif  15269  fzomaxdiflem  15271  rexico  15282  icodiamlt  15366  limsupgre  15409  rlim3  15426  icco1  15468  rlimclim  15474  rlimuni  15478  rlimresb  15493  isercolllem2  15594  isercolllem3  15595  isercoll  15596  caucvgrlem  15601  caurcvgr  15602  iseraltlem3  15612  fsum00  15726  o1fsum  15741  bitsfzolem  16366  bitsfzo  16367  bitsmod  16368  bitscmp  16370  gcd0id  16451  gcdneg  16454  bezoutlem4  16474  nn0seqcvgd  16502  lcmneg  16535  lcmfunsnlem2lem2  16571  qredeq  16589  prmind2  16617  eulerthlem2  16714  pcpremul  16776  pcidlem  16805  pcgcd1  16810  fldivp1  16830  pcfaclem  16831  4sqlem17  16894  vdwlem1  16914  vdwlem6  16919  vdwlem12  16925  vdwlem13  16926  0ram  16953  ram0  16955  ramub1lem1  16959  invco  17700  sectmon  17711  monsect  17712  invid  17716  ssctr  17754  ssceq  17755  0ssc  17766  0subcat  17767  catsubcat  17768  issubc3  17778  fullsubc  17779  funcinv  17802  fthmon  17858  fuccocl  17896  fucidcl  17897  invfuc  17906  2initoinv  17939  2termoinv  17946  elhomai  17962  setcmon  18016  setcepi  18017  catcisolem  18039  curf2cl  18159  yonedalem4c  18205  yonedalem3  18208  yoniso  18213  lublecl  18287  isacs3lem  18470  tsrdir  18532  chnccat  18554  rabsubmgmd  18634  submgmid  18636  subsubmgm  18640  mgmhmima  18645  mgmhmeql  18646  mndpfsupp  18697  mnd1  18709  sgrp2nmndlem4  18858  sgrp2nmndlem5  18859  0subg  19086  nmznsg  19102  ghmpreima  19172  ghmeql  19173  ghmnsgpreima  19175  kerf1ghm  19181  cntzsgrpcl  19268  cntzsubm  19272  cntzsubg  19273  cntzmhm  19275  symgextfo  19356  symgfixf1  19371  symgfixfolem1  19372  odlem2  19473  finodsubmsubg  19501  gexlem2  19516  gexcl2  19523  sylow1lem5  19536  subgslw  19550  slwhash  19558  fislw  19559  sylow3lem1  19561  lsmsubg  19588  efgredlemd  19678  efgredlem  19681  efgcpbllemb  19689  frgpuplem  19706  cyggeninv  19817  iscygd  19821  iscygodd  19822  gsumzadd  19856  gsumconst  19868  gsumpt  19896  gsum2dlem2  19905  gsum2d  19906  gsum2d2lem  19907  dprdfcntz  19951  eldprdi  19954  subgdmdprd  19970  subgdprd  19971  dprdpr  19986  ablfac1c  20007  ablfac1eu  20009  ablfaclem3  20023  ogrpaddlt  20072  ogrpsublt  20076  ring1  20250  subrngint  20498  rhmimasubrng  20504  cntzsubrng  20505  rhmeql  20541  rhmima  20542  cntzsubr  20544  rnghmsscmap2  20567  rnghmsscmap  20568  rnghmsubcsetc  20571  zrzeroorngc  20582  rhmsscmap2  20596  rhmsscmap  20597  rhmsubcsetc  20600  rhmsscrnghm  20603  rhmsubcrngc  20606  srhmsubc  20618  rhmsubc  20627  issubdrg  20718  fldhmsubc  20723  imadrhmcl  20735  isabvd  20750  abvdiv  20767  ornglmullt  20807  orngrmullt  20808  orngmullt  20809  ofldlt1  20813  lsslsp  20971  lsslspOLD  20972  lmhmima  21004  lmhmpreima  21005  lmhmeql  21012  lsmcl  21040  lspfixed  21088  rnglidlrng  21207  rngqiprngim  21264  rng2idl1cntr  21265  qsssubdrg  21386  gzrngunit  21393  pzriprnglem8  21448  evpmodpmf1o  21556  ocvpj  21677  dsmm0cl  21700  dsmmacl  21701  dsmmsubg  21703  dsmmlss  21704  frlmsplit2  21733  uvcff  21751  lindfrn  21781  f1lindf  21782  lindsss  21784  issubassa  21827  issubassa2  21853  snifpsrbag  21881  psrbaglesupp  21883  psrbaglecl  21884  psrbagaddcl  21885  psrbagcon  21886  mplsubglem  21959  mpllsslem  21960  mplassa  21982  subrgmpl  21992  mplcoe5  22000  mplbas2  22002  mplind  22030  mpfind  22075  ismhp2  22089  mhpmulcl  22097  mhplss  22103  ply1assa  22145  coe1tmmul2  22223  coe1tmmul  22224  cply1coe0bi  22251  dmatid  22444  dmatsubcl  22447  dmatscmcl  22452  scmatid  22463  scmataddcl  22465  scmatsubcl  22466  scmatmulcl  22467  smatvscl  22473  scmatrhmcl  22477  mat0scmat  22487  mat1scmat  22488  mdet0pr  22541  chmaidscmat  22797  distop  22944  indistopon  22950  ppttop  22956  epttop  22958  mretopd  23041  toponmre  23042  neiss  23058  opnneissb  23063  ssnei2  23065  innei  23074  neiptoptop  23080  ordtcld1  23146  ordtcld2  23147  lmconst  23210  cnpnei  23213  iscncl  23218  cnss1  23225  cnss2  23226  cncnpi  23227  cncnp  23229  cnconst2  23232  cnrest  23234  cnpresti  23237  cnpdis  23242  paste  23243  lmcnp  23253  cnhaus  23303  hauscmp  23356  2ndcomap  23407  1stcelcls  23410  1stccnp  23411  llyrest  23434  nllyrest  23435  llyidm  23437  nllyidm  23438  ssref  23461  reftr  23463  refun0  23464  dissnref  23477  kgentopon  23487  kgenidm  23496  kgencn3  23507  txcld  23552  neitx  23556  tx1cn  23558  tx2cn  23559  ptcld  23562  xkoccn  23568  txcnp  23569  ptcnp  23571  txcnmpt  23573  ptcn  23576  txdis1cn  23584  ptrescn  23588  txkgen  23601  xkoco1cn  23606  xkoco2cn  23607  xkococn  23609  xkoinjcn  23636  qtoptop2  23648  qtopuni  23651  qtopid  23654  qtopkgen  23659  basqtop  23660  tgqtop  23661  qtopss  23664  qtopeu  23665  qtoprest  23666  kqopn  23683  kqcld  23684  kqreglem2  23691  reghmph  23742  ordthmeolem  23750  qtopf1  23765  opnfbas  23791  isfil2  23805  fbasweak  23814  fsubbas  23816  filconn  23832  fbasrn  23833  rnelfmlem  23901  flimss2  23921  flimss1  23922  hausflim  23930  flimclslem  23933  flimsncls  23935  cnpflfi  23948  flfcnp2  23956  fclsfnflim  23976  cnextfvval  24014  cnextfres1  24017  symgtgp  24055  opnsubg  24057  ghmcnp  24064  qustgpopn  24069  qustgplem  24070  qustgphaus  24072  tsmsfbas  24077  ustfilxp  24162  utoptop  24183  utopbas  24184  restutopopn  24187  iducn  24231  cstucnd  24232  ucncn  24233  fmucnd  24240  cfilufg  24241  trcfilu  24242  cfiluweak  24243  neipcfilu  24244  psmetres2  24263  isxmetd  24275  xmetpsmet  24297  imasf1oxmet  24324  xblss2ps  24350  xblss2  24351  xblcntrps  24359  xblcntr  24360  blcld  24454  metustfbas  24506  cfilucfil  24508  restmetu  24519  ngptgp  24585  tngngpd  24602  nrmtngnrm  24607  tngnrg  24623  nlmvscn  24636  nrginvrcn  24641  nmo0  24684  nmoeq0  24685  nmoid  24691  nghmcn  24694  0nmhm  24704  blcvx  24747  iccntr  24771  xrge0tsms  24784  xmetdcn2  24787  metdstri  24801  metdscn  24806  rescncf  24851  cncfco  24861  oprpiece1res2  24911  cnheibor  24915  cnllycmp  24916  bndth  24918  ishtpyd  24935  isphtpyd  24946  pcoval2  24977  nmhmcn  25081  ipcn  25207  lmnn  25224  cfilss  25231  iscfil3  25234  cfilfcls  25235  cmetcaulem  25249  iscmet3lem2  25253  cfilres  25257  lmcau  25274  flimcfil  25275  cncmet  25283  rlmbn  25322  minveclem3b  25389  pjthlem1  25398  pjth2  25401  ivthlem3  25415  ovolssnul  25449  ovolctb  25452  ovoliunnul  25469  ovolsca  25477  ovolicopnf  25486  voliunlem2  25513  volsup  25518  dyadmaxlem  25559  vitalilem5  25574  mbfres  25606  mbfss  25608  mbfmulc2re  25610  mbfadd  25623  mbfmulc2  25625  mbflim  25630  i1faddlem  25655  i1fmullem  25656  mbfmul  25688  itg2mulc  25709  itg2cnlem1  25723  ibl0  25749  iblposlem  25754  itgreval  25759  iblneg  25765  iblss  25767  iblss2  25768  itgle  25772  iblconst  25780  iblabs  25791  iblabsr  25792  iblmulc2  25793  bddmulibl  25801  limciun  25856  limcun  25857  dvres2lem  25872  dvidlem  25877  dvcnp2  25882  dvcnp2OLD  25883  dvcn  25884  cpnres  25900  dvaddbr  25901  dvmulbr  25902  dvmulbrOLD  25903  dvcobr  25910  dvcobrOLD  25911  dvcjbr  25914  dvrec  25920  dvcnvlem  25941  dvferm  25953  dvlip2  25961  dveq0  25966  dv11cn  25967  dvivthlem1  25974  lhop1  25980  lhop2  25981  lhop  25982  dvcnvre  25985  dvfsumlem3  25996  dvfsumlem4  25997  dvfsumrlim  25999  dvfsum2  26002  ftc1a  26005  ftc1lem4  26007  ftc1lem6  26009  ftc1  26010  coe1mul3  26065  deg1addle2  26068  deg1sublt  26076  fta1blem  26137  drnguc1p  26140  ig1prsp  26147  plyco0  26158  plyeq0lem  26176  dgrub  26200  dgreq  26210  dgradd2  26235  dgrmul  26237  dgrcolem2  26241  dgrco  26242  plycpn  26258  plydivlem4  26265  plydiveu  26267  vieta1lem2  26280  vieta1  26281  aalioulem2  26302  aalioulem3  26303  aaliou3lem7  26318  tayl0  26330  ulmcn  26369  ulmdvlem3  26372  psercn  26397  abelth  26412  pilem3  26424  efif1olem1  26512  abslogimle  26543  argregt0  26580  argrege0  26581  logf1o2  26620  cxpsqrtlem  26672  cxpcn3  26719  abscxpbnd  26724  logreclem  26733  ang180lem2  26781  ang180lem3  26782  xrlimcnp  26939  harmonicbnd4  26982  fsumharmonic  26983  lgamgulmlem5  27004  lgambdd  27008  basellem4  27055  dvdsppwf1o  27157  dvdsflf1o  27158  fsumfldivdiaglem  27160  chpeq0  27180  chteq0  27181  chtub  27184  chpub  27192  dchrelbasd  27211  dchrmulcl  27221  dchrinv  27233  bposlem1  27256  bposlem2  27257  lgsdirprm  27303  lgsqrlem2  27319  lgsqrlem3  27320  lgsdchr  27327  lgseisenlem1  27347  lgseisenlem2  27348  lgseisenlem3  27349  lgsquadlem1  27352  2sqlem8  27398  2sqblem  27403  2sqmod  27408  chebbnd1lem1  27441  dchrisumlem1  27461  dchrisumlem2  27462  dchrisumlem3  27463  dchrisum0fno1  27483  pntrmax  27536  pntpbnd1a  27557  pntibndlem3  27564  pntlemn  27572  pntlemi  27576  pntlem3  27581  pntleml  27583  ostth1  27605  ostth2  27609  ostth3  27610  nosepon  27638  nolesgn2ores  27645  nogesgn1ores  27647  nosupres  27680  nosupbnd1lem2  27682  nosupbnd2lem1  27688  noinfres  27695  noinfbnd1lem2  27697  noinfbnd2lem1  27703  eqcuts3  27805  cofcutrtime  27928  divmuldivsd  28233  divdivs1d  28234  onsbnd  28282  nnsgt0  28340  bdayfinbndlem1  28468  ercgrg  28594  motco  28617  cnvmot  28618  legso  28676  mirmot  28752  colopp  28846  hphl  28848  lmicom  28865  lmimid  28871  lmimot  28875  hypcgrlem1  28876  hypcgrlem2  28877  trgcopyeulem  28882  inagswap  28918  inaghl  28922  cgrg3col4  28930  brbtwn2  28983  axlowdimlem3  29022  axlowdimlem16  29035  axcontlem8  29049  fusgrfis  29408  nbgr2vtx1edg  29428  0vtxrgr  29655  0vtxrusgr  29656  ewlkle  29684  wlk1ewlk  29718  uspgr2wlkeq2  29725  wlkp1lem8  29757  trlontrl  29787  pthonpth  29826  pthdlem2  29846  wlklnwwlkln1  29946  wlknewwlksn  29965  wwlksnred  29970  wwlksnredwwlkn0  29974  2trlond  30017  2pthond  30020  elwwlks2ons3im  30032  clwlkclwwlklem2a1  30072  clwlkclwwlkf1  30090  clwwlkel  30126  clwwlkwwlksb  30134  wwlksext2clwwlk  30137  1ewlk  30195  0trlon  30204  0pthon  30207  1pthond  30224  3trlond  30253  3pthond  30255  3spthond  30257  eupthres  30295  2clwwlk2clwwlk  30430  numclwwlk1lem2foa  30434  numclwwlk1lem2f1  30437  nvabs  30752  vacn  30774  nmcvcn  30775  nmblore  30866  0lno  30870  0blo  30872  nmlno0lem  30873  occl  31384  pjhthlem1  31471  pjpjpre  31499  nmopre  31950  nmlnop0iALT  32075  nmophmi  32111  leoprf2  32207  stlesi  32321  disjdifprg  32654  disjun0  32674  fsuppcurry1  32806  fsuppcurry2  32807  fpwrelmap  32815  fzspl  32872  dfmgc2lem  33080  pwrssmgc  33085  xrge0tsmsd  33159  psgnfzto1stlem  33186  fzto1st1  33188  evpmid  33234  pnfinf  33269  isarchiofld  33285  rmfsupp2  33324  fracfld  33394  dvdsruassoi  33469  nsgmgc  33497  drngidl  33518  qsdrngi  33580  deg1addlt  33685  ply1degltdimlem  33792  lbsdiflsp0  33796  fedgmul  33801  fldexttr  33828  fldextid  33829  irngnzply1lem  33860  finextalg  33868  minplyelirng  33885  irredminply  33886  algextdeglem8  33894  rtelextdg2lem  33896  constrsslem  33911  constrllcllem  33922  constrlccllem  33923  constrcccllem  33924  qtopt1  34005  reff  34009  locfinreflem  34010  metideq  34063  metider  34064  pstmxmet  34067  qqhval2lem  34151  qqhcn  34161  qqhucn  34162  pwsiga  34300  prsiga  34301  measle0  34378  mbfmcst  34429  1stmbfm  34430  2ndmbfm  34431  imambfm  34432  cnmbfm  34433  mbfmco  34434  mbfmco2  34435  0elcarsg  34477  carsgclctun  34491  sibfof  34510  oddpwdc  34524  eulerpartlemmf  34545  eulerpartlemgs2  34550  0rrv  34621  ballotlemfc0  34663  ballotlemfcc  34664  signstfveq0  34747  breprexplemc  34802  bnj1452  35221  usgrgt2cycl  35337  acycgr1v  35356  derangen  35379  subfacval3  35396  cvmseu  35483  cvmliftmolem2  35489  cvmliftlem7  35498  cvmliftlem15  35505  cvmlift2lem9a  35510  cvmlift2lem9  35518  cvmlift2lem10  35519  cvmlift2lem11  35520  cvmlift2lem12  35521  cvmlift3lem6  35531  cvmlift3lem8  35533  ex-sategoelel  35628  ex-sategoelelomsuc  35633  mclsppslem  35790  mclspps  35791  wsuclem  36030  fness  36556  fnetr  36558  fnessref  36564  refssfne  36565  neibastop1  36566  neibastop2  36568  tailfb  36584  filnetlem3  36587  weiunfrlem  36671  bj-finsumval0  37503  bj-rvecvec  37517  dfgcd3  37542  lindsadd  37827  poimirlem13  37847  poimirlem15  37849  poimirlem24  37858  poimirlem28  37862  mblfinlem2  37872  ovoliunnfl  37876  volsupnfl  37879  mbfresfi  37880  iblabsnc  37898  iblmulc2nc  37899  ftc1cnnclem  37905  ftc1cnnc  37906  ftc1anc  37915  sdclem2  37956  metf1o  37969  ismtyhmeolem  38018  ismtyres  38022  heibor1lem  38023  bfplem2  38037  bfp  38038  rrncmslem  38046  iccbnd  38054  icccmpALT  38055  rngogrphom  38185  rngoisoco  38196  keridl  38246  lsmcv2  39368  lsatcv0  39370  lcvexchlem4  39376  lcvexchlem5  39377  l1cvpat  39393  lfl0f  39408  lfladdcl  39410  lflnegcl  39414  lkrlss  39434  eqlkr  39438  lkrlsp  39441  lkrlsp2  39442  lshpkrcl  39455  lkrin  39503  1cvrjat  39814  llni  39847  llnle  39857  lplni  39871  lplnle  39879  llncvrlpln2  39896  2atmat  39900  lvoli  39914  lplncvrlvol2  39954  elpaddri  40141  paddclN  40181  pclclN  40230  pclfinN  40239  0psubclN  40282  1psubclN  40283  atpsubclN  40284  pmapsubclN  40285  osumclN  40306  pexmidN  40308  pexmidlem6N  40314  lhp2lt  40340  lautcnv  40429  idlaut  40435  lautco  40436  idldil  40453  ldilcnv  40454  ldilco  40455  ltrncnv  40485  idltrn  40489  cdleme16d  40620  cdleme50laut  40886  cdleme50ldil  40887  cdleme50ltrn  40896  ltrnco  41058  dian0  41378  dia0eldmN  41379  dia1eldmN  41380  dialss  41385  diaintclN  41397  docaclN  41463  doca2N  41465  djajN  41476  dibintclN  41506  diblss  41509  dicvaddcl  41529  dicvscacl  41530  dicn0  41531  cdlemn11a  41546  dihord2cN  41560  dihord11b  41561  dihord6apre  41595  dihmeetlem1N  41629  dihglblem5apreN  41630  dihpN  41675  dihjatcclem4  41760  dochkr1  41817  islpoldN  41823  lcfrlem31  41912  mapdpglem18  42028  mapdheq2  42068  mapdheq4  42071  mapdh6aN  42074  hdmap1l6a  42148  hdmap14lem4a  42210  lcmineqlem4  42365  frlmfzoccat  42838  drnginvmuld  42860  psrbagres  42877  evlselvlem  42907  evlselv  42908  fsuppind  42911  fsuppssind  42914  prjspvs  42931  irrapxlem4  43145  pell1234qrdich  43181  pell1qr1  43191  pell14qrgap  43195  pellqrexplicit  43197  rmspecfund  43229  fzmaxdif  43301  acongeq  43303  jm2.23  43316  jm3.1  43340  lmhmlnmsplit  43407  hbt  43450  dgrsub2  43455  proot1ex  43516  cantnfub  43641  cantnfresb  43644  cantnf2  43645  tfsconcatfv2  43660  tfsconcatrn  43662  tfsconcatb0  43664  naddcnff  43682  naddcnffo  43684  naddcnfid1  43687  naddcnfid2  43688  clublem  43929  dftrcl3  44039  mnugrud  44603  hashnzfz2  44640  dvconstbi  44653  ubelsupr  45343  restopn3  45473  wessf1ornlem  45507  lefldiveq  45617  iccintsng  45846  climsuse  45931  mullimc  45939  limcdm0  45941  limccog  45943  mullimcf  45946  constlimc  45947  idlimc  45949  limcperiod  45951  limsupre  45962  limcleqr  45965  neglimc  45968  addlimc  45969  0ellimcdiv  45970  xlimliminflimsup  46183  cncfshift  46195  cncfperiod  46200  cncfuni  46207  icccncfext  46208  cncfiooicclem1  46214  fperdvper  46240  ioodvbdlimc1lem2  46253  ioodvbdlimc2lem  46255  mbfres2cn  46279  iblsplit  46287  stoweidlem7  46328  stoweidlem13  46334  stoweidlem26  46347  wallispilem3  46388  stirlinglem6  46400  stirlinglem10  46404  dirkercncf  46428  fourierdlem6  46434  fourierdlem11  46439  fourierdlem12  46440  fourierdlem15  46443  fourierdlem26  46454  fourierdlem42  46470  fourierdlem50  46477  fourierdlem51  46478  fourierdlem52  46479  fourierdlem54  46481  fourierdlem62  46489  fourierdlem79  46506  fourierdlem102  46529  fourierdlem114  46541  etransclem23  46578  chnsubseq  47201  3f1oss1  47398  zgeltp1eq  47632  setsnidel  47700  preimafvsnel  47702  iccpartres  47741  prpair  47824  fpprel2  48064  isubgrsubgr  48192  grimidvtxedg  48208  grimcnv  48211  isuspgrim  48219  upgrimpthslem2  48231  stgrnbgr0  48287  uhgrimgrlim  48310  clnbgr3stgrgrlim  48342  gpg5nbgrvtx03starlem2  48392  gpg5nbgrvtx13starlem2  48395  gpg5edgnedg  48453  isassintop  48533  rhmsubcALTV  48608  srhmsubcALTV  48648  fldhmsubcALTV  48656  rmfsupp  48696  scmfsupp  48698  mptcfsupp  48700  lcoel0  48751  lincsumcl  48754  lincscmcl  48755  lcoss  48759  lindsrng01  48791  lincreslvec3  48805  lindssnlvec  48809  zgtp1leeq  48844  lubsscl  49282  glbsscl  49283  idmon  49342  idepi  49343  iinfssc  49379  iinfsubc  49380  discsubc  49386  nelsubclem  49389  imassc  49475  imasubc3  49478  isnatd  49545  swapfiso  49607  fucoppc  49732  thinciso  49792  diagciso  49861  termolmd  49992