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  7082  fveqressseq  7103  fmptsng  7196  fmptsnd  7197  fnprb  7237  fntpb  7238  fpr3g  8331  frrlem4  8335  1ellim  8534  isfsuppd  9386  fdmfifsupp  9394  fsuppmptif  9418  fsuppco2  9422  fsuppcor  9423  dffi3  9450  suppr  9491  infpr  9524  ordtypelem7  9545  cantnf0  9703  cantnfp1lem1  9706  cantnfp1lem2  9707  cantnfp1lem3  9708  cantnflem1a  9713  cantnflem1d  9716  cantnflem1  9717  cantnf  9721  rankpwi  9859  carduni  10089  fin23lem32  10449  fpwwe2lem5  10747  fpwwe2lem11  10753  fpwwe2lem12  10754  fpwwe2  10755  inttsk  10886  grutsk1  10933  add20  11855  supaddc  12311  supadd  12312  supmul  12316  suprzcl  12806  uzid  13007  uzwo3  13097  rpnnen1lem5  13136  xrletrid  13311  xrre  13326  xrre3  13328  xleadd1a  13410  xlemul1a  13445  elioc2  13567  elico2  13568  elicc2  13569  elfz1eq  13695  fzadd2  13720  fznatpl1  13739  elfz1uz  13755  nn0fz0  13786  fzctr  13801  fzo1fzo0n0  13877  fzoaddel  13879  elincfzoext  13885  f1resfz0f1d  13954  flid  13975  flval3  13982  fladdz  13992  fldiv  14027  modid  14063  hashf1lem1  14627  pfxccatin12d  14922  repswpfx  14964  2cshw  14992  pfx2  15127  wwlktovf1  15139  sqeqd  15362  01sqrexlem7  15444  max0add  15506  abs2difabs  15531  rddif  15537  fzomaxdiflem  15539  rexico  15550  icodiamlt  15634  limsupgre  15677  rlim3  15694  icco1  15736  rlimclim  15742  rlimuni  15746  rlimresb  15761  isercolllem2  15862  isercolllem3  15863  isercoll  15864  caucvgrlem  15869  caurcvgr  15870  iseraltlem3  15880  fsum00  15994  o1fsum  16009  bitsfzolem  16633  bitsfzo  16634  bitsmod  16635  bitscmp  16637  gcd0id  16720  gcdneg  16723  bezoutlem4  16744  nn0seqcvgd  16774  lcmneg  16807  lcmfunsnlem2lem2  16843  qredeq  16861  prmind2  16889  eulerthlem2  16988  pcpremul  17050  pcidlem  17079  pcgcd1  17084  fldivp1  17104  pcfaclem  17105  4sqlem17  17168  vdwlem1  17188  vdwlem6  17193  vdwlem12  17199  vdwlem13  17200  0ram  17227  ram0  17229  ramub1lem1  17233  invco  17975  sectmon  17986  monsect  17987  invid  17991  ssctr  18029  ssceq  18030  0ssc  18041  0subcat  18042  catsubcat  18043  issubc3  18053  fullsubc  18054  funcinv  18077  fthmon  18133  fuccocl  18171  fucidcl  18172  invfuc  18181  2initoinv  18214  2termoinv  18221  elhomai  18237  setcmon  18291  setcepi  18292  catcisolem  18314  curf2cl  18434  yonedalem4c  18480  yonedalem3  18483  yoniso  18488  lublecl  18562  isacs3lem  18745  tsrdir  18807  chnccat  18829  rabsubmgmd  18922  submgmid  18924  subsubmgm  18928  mgmhmima  18933  mgmhmeql  18934  mndpfsupp  18990  mnd1  19002  sgrp2nmndlem4  19156  sgrp2nmndlem5  19157  0subg  19391  nmznsg  19407  ghmpreima  19481  ghmeql  19482  ghmnsgpreima  19484  kerf1ghm  19490  cntzsgrpcl  19578  cntzsubm  19582  cntzsubg  19583  cntzmhm  19585  symgextfo  19666  symgfixf1  19681  symgfixfolem1  19682  odlem2  19783  finodsubmsubg  19811  gexlem2  19826  gexcl2  19833  sylow1lem5  19846  subgslw  19860  slwhash  19868  fislw  19869  sylow3lem1  19871  lsmsubg  19898  efgredlemd  19988  efgredlem  19991  efgcpbllemb  19999  frgpuplem  20016  cyggeninv  20127  iscygd  20131  iscygodd  20132  gsumzadd  20166  gsumconst  20178  gsumpt  20206  gsum2dlem2  20215  gsum2d  20216  gsum2d2lem  20217  dprdfcntz  20261  eldprdi  20264  subgdmdprd  20280  subgdprd  20281  dprdpr  20296  ablfac1c  20317  ablfac1eu  20319  ablfaclem3  20333  ogrpaddlt  20382  ogrpsublt  20386  ring1  20571  subrngint  20842  rhmimasubrng  20848  cntzsubrng  20849  rhmeql  20885  rhmima  20886  cntzsubr  20888  rnghmsscmap2  20911  rnghmsscmap  20912  rnghmsubcsetc  20915  zrzeroorngc  20926  rhmsscmap2  20940  rhmsscmap  20941  rhmsubcsetc  20944  rhmsscrnghm  20947  rhmsubcrngc  20950  srhmsubc  20962  rhmsubc  20971  issubdrg  21067  fldhmsubc  21072  imadrhmcl  21084  isabvd  21099  abvdiv  21116  ornglmullt  21156  orngrmullt  21157  orngmullt  21158  ofldlt1  21162  lsslsp  21320  lmhmima  21352  lmhmpreima  21353  lmhmeql  21360  lsmcl  21388  lspfixed  21436  rnglidlrng  21565  drngidl  21569  rngqiprngim  21630  rng2idl1cntr  21631  qsssubdrg  21762  gzrngunit  21769  pzriprnglem8  21824  evpmodpmf1o  21932  ocvpj  22053  dsmm0cl  22076  dsmmacl  22077  dsmmsubg  22079  dsmmlss  22080  frlmsplit2  22109  uvcff  22127  lindfrn  22157  f1lindf  22158  lindsss  22160  issubassa  22205  issubassa2  22230  snifpsrbag  22258  psrbaglesupp  22260  psrbaglecl  22261  psrbagaddcl  22262  psrbagcon  22263  psrbagres  22268  mplsubglem  22336  mpllsslem  22337  mplassa  22359  subrgmpl  22370  mplcoe5  22379  mplbas2  22381  mplind  22409  mpfind  22454  ismhp2  22492  mhpmulcl  22500  mhplss  22506  ply1assa  22547  coe1tmmul2  22625  coe1tmmul  22626  cply1coe0bi  22650  dmatid  22840  dmatsubcl  22843  dmatscmcl  22848  scmatid  22859  scmataddcl  22861  scmatsubcl  22862  scmatmulcl  22863  smatvscl  22869  scmatrhmcl  22873  mat0scmat  22883  mat1scmat  22884  mdet0pr  22937  chmaidscmat  23196  distop  23343  indistopon  23349  ppttop  23355  epttop  23357  mretopd  23440  toponmre  23441  neiss  23457  opnneissb  23462  ssnei2  23464  innei  23473  neiptoptop  23479  ordtcld1  23545  ordtcld2  23546  lmconst  23609  cnpnei  23612  iscncl  23617  cnss1  23624  cnss2  23625  cncnpi  23626  cncnp  23628  cnconst2  23631  cnrest  23633  cnpresti  23636  cnpdis  23641  paste  23642  lmcnp  23652  cnhaus  23702  hauscmp  23755  2ndcomap  23807  1stcelcls  23810  1stccnp  23811  llyrest  23834  nllyrest  23835  llyidm  23837  nllyidm  23838  ssref  23861  reftr  23863  refun0  23864  dissnref  23877  kgentopon  23887  kgenidm  23896  kgencn3  23907  txcld  23952  neitx  23956  tx1cn  23958  tx2cn  23959  ptcld  23962  xkoccn  23968  txcnp  23969  ptcnp  23971  txcnmpt  23973  ptcn  23976  txdis1cn  23984  ptrescn  23988  txkgen  24001  xkoco1cn  24006  xkoco2cn  24007  xkococn  24009  xkoinjcn  24036  qtoptop2  24048  qtopuni  24051  qtopid  24054  qtopkgen  24059  basqtop  24060  tgqtop  24061  qtopss  24064  qtopeu  24065  qtoprest  24066  kqopn  24083  kqcld  24084  kqreglem2  24091  reghmph  24142  ordthmeolem  24150  qtopf1  24165  opnfbas  24191  isfil2  24205  fbasweak  24214  fsubbas  24216  filconn  24232  fbasrn  24233  rnelfmlem  24301  flimss2  24321  flimss1  24322  hausflim  24330  flimclslem  24333  flimsncls  24335  cnpflfi  24348  flfcnp2  24356  fclsfnflim  24376  cnextfvval  24414  cnextfres1  24417  symgtgp  24455  opnsubg  24457  ghmcnp  24464  qustgpopn  24469  qustgplem  24470  qustgphaus  24472  tsmsfbas  24477  ustfilxp  24562  utoptop  24583  utopbas  24584  restutopopn  24587  iducn  24631  cstucnd  24632  ucncn  24633  fmucnd  24640  cfilufg  24641  trcfilu  24642  cfiluweak  24643  neipcfilu  24644  psmetres2  24663  isxmetd  24675  xmetpsmet  24697  imasf1oxmet  24724  xblss2ps  24750  xblss2  24751  xblcntrps  24759  xblcntr  24760  blcld  24854  metustfbas  24906  cfilucfil  24908  restmetu  24919  ngptgp  24985  tngngpd  25002  nrmtngnrm  25007  tngnrg  25023  nlmvscn  25036  nrginvrcn  25041  nmo0  25084  nmoeq0  25085  nmoid  25091  nghmcn  25094  0nmhm  25104  blcvx  25147  iccntr  25171  xrge0tsms  25184  xmetdcn2  25187  metdstri  25201  metdscn  25206  rescncf  25248  cncfco  25258  oprpiece1res2  25303  cnheibor  25306  cnllycmp  25307  bndth  25309  ishtpyd  25326  isphtpyd  25337  pcoval2  25367  nmhmcn  25471  ipcn  25597  lmnn  25614  cfilss  25621  iscfil3  25624  cfilfcls  25625  cmetcaulem  25639  iscmet3lem2  25643  cfilres  25647  lmcau  25664  flimcfil  25665  cncmet  25673  rlmbn  25712  minveclem3b  25779  pjthlem1  25788  pjth2  25791  ivthlem3  25804  ovolssnul  25838  ovolctb  25841  ovoliunnul  25858  ovolsca  25866  ovolicopnf  25875  voliunlem2  25902  volsup  25907  dyadmaxlem  25948  vitalilem5  25963  mbfres  25995  mbfss  25997  mbfmulc2re  25999  mbfadd  26012  mbfmulc2  26014  mbflim  26019  i1faddlem  26044  i1fmullem  26045  mbfmul  26077  itg2mulc  26098  itg2cnlem1  26112  ibl0  26137  iblposlem  26142  itgreval  26147  iblneg  26153  iblss  26155  iblss2  26156  itgle  26160  iblconst  26168  iblabs  26179  iblabsr  26180  iblmulc2  26181  bddmulibl  26189  limciun  26244  limcun  26245  dvres2lem  26260  dvidlem  26265  dvcnp2  26270  dvcn  26271  cpnres  26287  dvaddbr  26288  dvmulbr  26289  dvcobr  26296  dvcjbr  26299  dvrec  26305  dvcnvlem  26326  dvferm  26338  dvlip2  26345  dveq0  26350  dv11cn  26351  dvivthlem1  26358  lhop1  26364  lhop2  26365  lhop  26366  dvcnvre  26369  dvfsumlem3  26378  dvfsumlem4  26379  dvfsumrlim  26381  dvfsum2  26384  ftc1a  26387  ftc1lem4  26389  ftc1lem6  26391  ftc1  26392  coe1mul3  26447  deg1addle2  26450  deg1sublt  26458  fta1blem  26519  drnguc1p  26522  ig1prsp  26529  plyco0  26540  plyeq0lem  26559  dgrub  26583  dgreq  26593  dgradd2  26617  dgrmul  26619  dgrcolem2  26623  dgrco  26624  plycpn  26640  plydivlem4  26647  plydiveu  26649  vieta1lem2  26664  vieta1  26665  aalioulem2  26690  aalioulem3  26691  aaliou3lem7  26706  tayl0  26719  ulmcn  26756  ulmdvlem3  26759  psercn  26783  abelth  26798  pilem3  26810  efif1olem1  26900  abslogimle  26931  argregt0  26968  argrege0  26969  logf1o2  27008  cxpsqrtlem  27060  cxpcn3  27106  abscxpbnd  27111  logreclem  27120  ang180lem2  27168  ang180lem3  27169  xrlimcnp  27326  harmonicbnd4  27368  fsumharmonic  27369  lgamgulmlem5  27390  lgambdd  27394  basellem4  27441  dvdsppwf1o  27543  dvdsflf1o  27544  fsumfldivdiaglem  27546  chpeq0  27565  chteq0  27566  chtub  27569  chpub  27577  dchrelbasd  27596  dchrmulcl  27606  dchrinv  27618  bposlem1  27641  bposlem2  27642  lgsdirprm  27688  lgsqrlem2  27704  lgsqrlem3  27705  lgsdchr  27712  lgseisenlem1  27732  lgseisenlem2  27733  lgseisenlem3  27734  lgsquadlem1  27737  2sqlem8  27783  2sqblem  27788  2sqmod  27793  chebbnd1lem1  27826  dchrisumlem1  27846  dchrisumlem2  27847  dchrisumlem3  27848  dchrisum0fno1  27868  pntrmax  27921  pntpbnd1a  27942  pntibndlem3  27949  pntlemn  27957  pntlemi  27961  pntlem3  27966  pntleml  27968  ostth1  27990  ostth2  27994  ostth3  27995  nosepon  28052  nolesgn2ores  28059  nogesgn1ores  28061  nosupres  28094  nosupbnd1lem2  28096  nosupbnd2lem1  28102  noinfres  28109  noinfbnd1lem2  28111  noinfbnd2lem1  28117  eqcuts3  28220  cofcutrtime  28343  divmuldivsd  28648  divdivs1d  28649  onsbnd  28697  nnsgt0  28755  bdayfinbndlem1  28883  ercgrg  29010  motco  29033  cnvmot  29034  legso  29092  mirmot  29177  colopp  29277  hphl  29279  lmicom  29323  lmimid  29329  lmimot  29333  hypcgrlem1  29335  hypcgrlem2  29336  trgcopyeulem  29342  inagswap  29390  inaghl  29394  cgrg3col4  29402  prlngd  29447  prlngref  29448  dfprlng2  29455  brbtwn2  29513  axlowdimlem3  29552  axlowdimlem16  29565  axcontlem8  29579  fusgrfis  29941  nbgr2vtx1edg  29961  0vtxrgr  30187  0vtxrusgr  30188  ewlkle  30216  wlk1ewlk  30250  uspgr2wlkeq2  30257  wlkp1lem8  30289  trlontrl  30323  pthonpth  30364  pthdlem2  30384  wlklnwwlkln1  30487  wlknewwlksn  30506  wwlksnred  30511  wwlksnredwwlkn0  30515  2trlond  30558  2pthond  30561  elwwlks2ons3im  30573  clwlkclwwlklem2a1  30613  clwlkclwwlkf1  30631  clwwlkel  30667  clwwlkwwlksb  30675  wwlksext2clwwlk  30678  1ewlk  30736  0trlon  30745  0pthon  30748  1pthond  30765  3trlond  30804  3pthond  30806  3spthond  30808  eupthres  30846  2clwwlk2clwwlk  30981  numclwwlk1lem2foa  30985  numclwwlk1lem2f1  30988  nvabs  31304  vacn  31326  nmcvcn  31327  nmblore  31418  0lno  31422  0blo  31424  nmlno0lem  31425  occl  31936  pjhthlem1  32023  pjpjpre  32051  nmopre  32502  nmlnop0iALT  32627  nmophmi  32663  leoprf2  32759  stlesi  32873  disjdifprg  33241  disjun0  33261  fsuppcurry1  33386  fsuppcurry2  33387  fpwrelmap  33395  fzspl  33451  dfmgc2lem  33626  pwrssmgc  33631  xrge0tsmsd  33704  psgnfzto1stlem  33731  fzto1st1  33733  evpmid  33779  pnfinf  33814  isarchiofld  33830  rmfsupp2  33868  fracfld  33940  dvdsruassoi  34009  nsgmgc  34033  qsdrngi  34089  deg1addlt  34202  ply1degltdimlem  34324  lbsdiflsp0  34328  fedgmul  34333  fldexttr  34360  fldextid  34361  irngnzply1lem  34392  finextalg  34400  minplyelirng  34417  irredminply  34418  algextdeglem8  34426  rtelextdg2lem  34428  constrsslem  34443  constrllcllem  34454  constrlccllem  34455  constrcccllem  34456  qtopt1  34537  reff  34541  locfinreflem  34542  metideq  34595  metider  34596  pstmxmet  34599  qqhval2lem  34683  qqhcn  34693  qqhucn  34694  pwsiga  34832  prsiga  34833  measle0  34911  mbfmcst  34961  1stmbfm  34962  2ndmbfm  34963  imambfm  34964  cnmbfm  34965  mbfmco  34966  mbfmco2  34967  0elcarsg  35009  carsgclctun  35023  sibfof  35042  oddpwdc  35056  eulerpartlemmf  35077  eulerpartlemgs2  35082  0rrv  35153  ballotlemfc0  35195  ballotlemfcc  35196  signstfveq0  35276  breprexplemc  35331  bnj1452  35752  usgrgt2cycl  36066  acycgr1v  36071  derangen  36104  subfacval3  36121  cvmseu  36208  cvmliftmolem2  36214  cvmliftlem7  36223  cvmliftlem15  36230  cvmlift2lem9a  36235  cvmlift2lem9  36243  cvmlift2lem10  36244  cvmlift2lem11  36245  cvmlift2lem12  36246  cvmlift3lem6  36256  cvmlift3lem8  36258  ex-sategoelel  36353  ex-sategoelelomsuc  36358  mclsppslem  36515  mclspps  36516  wsuclem  36765  nadddilem2  37148  fness  37315  fnetr  37317  fnessref  37323  refssfne  37324  neibastop1  37325  neibastop2  37327  tailfb  37343  filnetlem3  37346  weiunfrlem  37430  bj-finsumval0  38398  bj-rvecvec  38412  dfgcd3  38437  lindsadd  38728  poimirlem13  38743  poimirlem15  38745  poimirlem24  38754  poimirlem28  38758  mblfinlem2  38768  ovoliunnfl  38772  volsupnfl  38775  mbfresfi  38776  iblabsnc  38794  iblmulc2nc  38795  ftc1cnnclem  38801  ftc1cnnc  38802  ftc1anc  38811  sdclem2  38868  metf1o  38881  ismtyhmeolem  38930  ismtyres  38934  heibor1lem  38935  bfplem2  38949  bfp  38950  rrncmslem  38958  iccbnd  38966  icccmpALT  38967  rngogrphom  39097  rngoisoco  39108  keridl  39158  lsmcv2  40278  lsatcv0  40280  lcvexchlem4  40286  lcvexchlem5  40287  l1cvpat  40303  lfl0f  40318  lfladdcl  40320  lflnegcl  40324  lkrlss  40344  eqlkr  40348  lkrlsp  40351  lkrlsp2  40352  lshpkrcl  40365  lkrin  40413  1cvrjat  40724  llni  40757  llnle  40767  lplni  40781  lplnle  40789  llncvrlpln2  40806  2atmat  40810  lvoli  40824  lplncvrlvol2  40864  elpaddri  41051  paddclN  41091  pclclN  41140  pclfinN  41149  0psubclN  41192  1psubclN  41193  atpsubclN  41194  pmapsubclN  41195  osumclN  41216  pexmidN  41218  pexmidlem6N  41224  lhp2lt  41250  lautcnv  41339  idlaut  41345  lautco  41346  idldil  41363  ldilcnv  41364  ldilco  41365  ltrncnv  41395  idltrn  41399  cdleme16d  41530  cdleme50laut  41796  cdleme50ldil  41797  cdleme50ltrn  41806  ltrnco  41968  dian0  42288  dia0eldmN  42289  dia1eldmN  42290  dialss  42295  diaintclN  42307  docaclN  42373  doca2N  42375  djajN  42386  dibintclN  42416  diblss  42419  dicvaddcl  42439  dicvscacl  42440  dicn0  42441  cdlemn11a  42456  dihord2cN  42470  dihord11b  42471  dihord6apre  42505  dihmeetlem1N  42539  dihglblem5apreN  42540  dihpN  42585  dihjatcclem4  42670  dochkr1  42727  islpoldN  42733  lcfrlem31  42822  mapdpglem18  42938  mapdheq2  42978  mapdheq4  42981  mapdh6aN  42984  hdmap1l6a  43058  hdmap14lem4a  43120  lcmineqlem4  43274  frlmfzoccat  43765  drnginvmuld  43781  evlselvlem  43809  evlselv  43810  fsuppind  43811  fsuppssind  43814  prjspvs  43831  frlmnzcoordsca  43851  prjspnnorm  43854  irrapxlem4  44025  pell1234qrdich  44061  pell1qr1  44071  pell14qrgap  44075  pellqrexplicit  44077  rmspecfund  44109  fzmaxdif  44181  acongeq  44183  jm2.23  44196  jm3.1  44220  lmhmlnmsplit  44282  hbt  44324  dgrsub2  44329  proot1ex  44390  cantnfub  44515  cantnfresb  44518  cantnf2  44519  tfsconcatfv2  44534  tfsconcatrn  44536  tfsconcatb0  44538  naddcnff  44556  naddcnffo  44558  naddcnfid1  44561  naddcnfid2  44562  clublem  44802  dftrcl3  44912  mnugrud  45460  hashnzfz2  45497  dvconstbi  45510  ubelsupr  46242  restopn3  46371  wessf1ornlem  46405  lefldiveq  46513  iccintsng  46740  climsuse  46825  mullimc  46833  limcdm0  46835  limccog  46837  mullimcf  46840  constlimc  46841  idlimc  46843  limcperiod  46845  limsupre  46856  limcleqr  46859  neglimc  46862  addlimc  46863  0ellimcdiv  46864  xlimliminflimsup  47077  cncfshift  47089  cncfperiod  47094  cncfuni  47101  icccncfext  47102  cncfiooicclem1  47108  fperdvper  47134  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  mbfres2cn  47173  iblsplit  47181  stoweidlem7  47222  stoweidlem13  47228  stoweidlem26  47241  wallispilem3  47282  stirlinglem6  47294  stirlinglem10  47298  dirkercncf  47322  fourierdlem6  47328  fourierdlem11  47333  fourierdlem12  47334  fourierdlem15  47337  fourierdlem26  47348  fourierdlem42  47364  fourierdlem50  47371  fourierdlem51  47372  fourierdlem52  47373  fourierdlem54  47375  fourierdlem62  47383  fourierdlem79  47400  fourierdlem102  47423  fourierdlem114  47435  etransclem23  47472  chnsubseq  48095  3f1oss1  48350  zgeltp1eq  48584  nnmul2  48605  setsnidel  48664  preimafvsnel  48666  iccpartres  48705  prpair  48788  fpprel2  49044  isubgrsubgr  49172  grimidvtxedg  49188  grimcnv  49191  isuspgrim  49199  upgrimpthslem2  49211  stgrnbgr0  49267  uhgrimgrlim  49290  clnbgr3stgrgrlim  49322  gpg5nbgrvtx03starlem2  49372  gpg5nbgrvtx13starlem2  49375  gpg5edgnedg  49433  isassintop  49512  rhmsubcALTV  49587  srhmsubcALTV  49627  fldhmsubcALTV  49635  rmfsupp  49690  scmfsupp  49692  mptcfsupp  49694  lcoel0  49745  lincsumcl  49748  lincscmcl  49749  lcoss  49753  lindsrng01  49785  lincreslvec3  49799  lindssnlvec  49803  zgtp1leeq  49838  lubsscl  50279  glbsscl  50280  idmon  50339  idepi  50340  iinfssc  50376  iinfsubc  50377  discsubc  50383  nelsubclem  50386  imassc  50474  imasubc3  50477  isnatd  50544  swapfiso  50612  fucoppc  50750  thinciso  50810  diagciso  50882  termolmd  51058  wrdf1d  51220