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  7058  fveqressseq  7079  fmptsng  7173  fmptsnd  7174  fnprb  7214  fntpb  7215  fpr3g  8303  frrlem4  8307  1ellim  8506  isfsuppd  9358  fdmfifsupp  9367  fsuppmptif  9391  fsuppco2  9395  fsuppcor  9396  dffi3  9423  suppr  9464  infpr  9497  ordtypelem7  9518  cantnf0  9676  cantnfp1lem1  9679  cantnfp1lem2  9680  cantnfp1lem3  9681  cantnflem1a  9686  cantnflem1d  9689  cantnflem1  9690  cantnf  9694  rankpwi  9832  carduni  10062  fin23lem32  10422  fpwwe2lem5  10720  fpwwe2lem11  10726  fpwwe2lem12  10727  fpwwe2  10728  inttsk  10859  grutsk1  10906  add20  11828  supaddc  12284  supadd  12285  supmul  12289  suprzcl  12779  uzid  12980  uzwo3  13070  rpnnen1lem5  13109  xrletrid  13284  xrre  13299  xrre3  13301  xleadd1a  13383  xlemul1a  13418  elioc2  13540  elico2  13541  elicc2  13542  elfz1eq  13668  fzadd2  13693  fznatpl1  13712  elfz1uz  13728  nn0fz0  13759  fzctr  13774  fzo1fzo0n0  13850  fzoaddel  13852  elincfzoext  13858  f1resfz0f1d  13927  flid  13948  flval3  13955  fladdz  13965  fldiv  14000  modid  14036  hashf1lem1  14600  pfxccatin12d  14894  repswpfx  14936  2cshw  14964  pfx2  15098  wwlktovf1  15110  sqeqd  15333  01sqrexlem7  15415  max0add  15477  abs2difabs  15502  rddif  15508  fzomaxdiflem  15510  rexico  15521  icodiamlt  15605  limsupgre  15648  rlim3  15665  icco1  15707  rlimclim  15713  rlimuni  15717  rlimresb  15732  isercolllem2  15833  isercolllem3  15834  isercoll  15835  caucvgrlem  15840  caurcvgr  15841  iseraltlem3  15851  fsum00  15965  o1fsum  15980  bitsfzolem  16604  bitsfzo  16605  bitsmod  16606  bitscmp  16608  gcd0id  16691  gcdneg  16694  bezoutlem4  16715  nn0seqcvgd  16745  lcmneg  16778  lcmfunsnlem2lem2  16814  qredeq  16832  prmind2  16860  eulerthlem2  16959  pcpremul  17021  pcidlem  17050  pcgcd1  17055  fldivp1  17075  pcfaclem  17076  4sqlem17  17139  vdwlem1  17159  vdwlem6  17164  vdwlem12  17170  vdwlem13  17171  0ram  17198  ram0  17200  ramub1lem1  17204  invco  17946  sectmon  17957  monsect  17958  invid  17962  ssctr  18000  ssceq  18001  0ssc  18012  0subcat  18013  catsubcat  18014  issubc3  18024  fullsubc  18025  funcinv  18048  fthmon  18104  fuccocl  18142  fucidcl  18143  invfuc  18152  2initoinv  18185  2termoinv  18192  elhomai  18208  setcmon  18262  setcepi  18263  catcisolem  18285  curf2cl  18405  yonedalem4c  18451  yonedalem3  18454  yoniso  18459  lublecl  18533  isacs3lem  18716  tsrdir  18778  chnccat  18800  rabsubmgmd  18893  submgmid  18895  subsubmgm  18899  mgmhmima  18904  mgmhmeql  18905  mndpfsupp  18961  mnd1  18973  sgrp2nmndlem4  19127  sgrp2nmndlem5  19128  0subg  19362  nmznsg  19378  ghmpreima  19452  ghmeql  19453  ghmnsgpreima  19455  kerf1ghm  19461  cntzsgrpcl  19548  cntzsubm  19552  cntzsubg  19553  cntzmhm  19555  symgextfo  19636  symgfixf1  19651  symgfixfolem1  19652  odlem2  19753  finodsubmsubg  19781  gexlem2  19796  gexcl2  19803  sylow1lem5  19816  subgslw  19830  slwhash  19838  fislw  19839  sylow3lem1  19841  lsmsubg  19868  efgredlemd  19958  efgredlem  19961  efgcpbllemb  19969  frgpuplem  19986  cyggeninv  20097  iscygd  20101  iscygodd  20102  gsumzadd  20136  gsumconst  20148  gsumpt  20176  gsum2dlem2  20185  gsum2d  20186  gsum2d2lem  20187  dprdfcntz  20231  eldprdi  20234  subgdmdprd  20250  subgdprd  20251  dprdpr  20266  ablfac1c  20287  ablfac1eu  20289  ablfaclem3  20303  ogrpaddlt  20352  ogrpsublt  20356  ring1  20541  subrngint  20812  rhmimasubrng  20818  cntzsubrng  20819  rhmeql  20855  rhmima  20856  cntzsubr  20858  rnghmsscmap2  20881  rnghmsscmap  20882  rnghmsubcsetc  20885  zrzeroorngc  20896  rhmsscmap2  20910  rhmsscmap  20911  rhmsubcsetc  20914  rhmsscrnghm  20917  rhmsubcrngc  20920  srhmsubc  20932  rhmsubc  20941  issubdrg  21037  fldhmsubc  21042  imadrhmcl  21054  isabvd  21069  abvdiv  21086  ornglmullt  21126  orngrmullt  21127  orngmullt  21128  ofldlt1  21132  lsslsp  21290  lmhmima  21322  lmhmpreima  21323  lmhmeql  21330  lsmcl  21358  lspfixed  21406  rnglidlrng  21535  drngidl  21539  rngqiprngim  21600  rng2idl1cntr  21601  qsssubdrg  21732  gzrngunit  21739  pzriprnglem8  21794  evpmodpmf1o  21902  ocvpj  22023  dsmm0cl  22046  dsmmacl  22047  dsmmsubg  22049  dsmmlss  22050  frlmsplit2  22079  uvcff  22097  lindfrn  22127  f1lindf  22128  lindsss  22130  issubassa  22175  issubassa2  22200  snifpsrbag  22228  psrbaglesupp  22230  psrbaglecl  22231  psrbagaddcl  22232  psrbagcon  22233  psrbagres  22238  mplsubglem  22306  mpllsslem  22307  mplassa  22329  subrgmpl  22340  mplcoe5  22349  mplbas2  22351  mplind  22379  mpfind  22424  ismhp2  22462  mhpmulcl  22470  mhplss  22476  ply1assa  22517  coe1tmmul2  22595  coe1tmmul  22596  cply1coe0bi  22620  dmatid  22810  dmatsubcl  22813  dmatscmcl  22818  scmatid  22829  scmataddcl  22831  scmatsubcl  22832  scmatmulcl  22833  smatvscl  22839  scmatrhmcl  22843  mat0scmat  22853  mat1scmat  22854  mdet0pr  22907  chmaidscmat  23166  distop  23313  indistopon  23319  ppttop  23325  epttop  23327  mretopd  23410  toponmre  23411  neiss  23427  opnneissb  23432  ssnei2  23434  innei  23443  neiptoptop  23449  ordtcld1  23515  ordtcld2  23516  lmconst  23579  cnpnei  23582  iscncl  23587  cnss1  23594  cnss2  23595  cncnpi  23596  cncnp  23598  cnconst2  23601  cnrest  23603  cnpresti  23606  cnpdis  23611  paste  23612  lmcnp  23622  cnhaus  23672  hauscmp  23725  2ndcomap  23777  1stcelcls  23780  1stccnp  23781  llyrest  23804  nllyrest  23805  llyidm  23807  nllyidm  23808  ssref  23831  reftr  23833  refun0  23834  dissnref  23847  kgentopon  23857  kgenidm  23866  kgencn3  23877  txcld  23922  neitx  23926  tx1cn  23928  tx2cn  23929  ptcld  23932  xkoccn  23938  txcnp  23939  ptcnp  23941  txcnmpt  23943  ptcn  23946  txdis1cn  23954  ptrescn  23958  txkgen  23971  xkoco1cn  23976  xkoco2cn  23977  xkococn  23979  xkoinjcn  24006  qtoptop2  24018  qtopuni  24021  qtopid  24024  qtopkgen  24029  basqtop  24030  tgqtop  24031  qtopss  24034  qtopeu  24035  qtoprest  24036  kqopn  24053  kqcld  24054  kqreglem2  24061  reghmph  24112  ordthmeolem  24120  qtopf1  24135  opnfbas  24161  isfil2  24175  fbasweak  24184  fsubbas  24186  filconn  24202  fbasrn  24203  rnelfmlem  24271  flimss2  24291  flimss1  24292  hausflim  24300  flimclslem  24303  flimsncls  24305  cnpflfi  24318  flfcnp2  24326  fclsfnflim  24346  cnextfvval  24384  cnextfres1  24387  symgtgp  24425  opnsubg  24427  ghmcnp  24434  qustgpopn  24439  qustgplem  24440  qustgphaus  24442  tsmsfbas  24447  ustfilxp  24532  utoptop  24553  utopbas  24554  restutopopn  24557  iducn  24601  cstucnd  24602  ucncn  24603  fmucnd  24610  cfilufg  24611  trcfilu  24612  cfiluweak  24613  neipcfilu  24614  psmetres2  24633  isxmetd  24645  xmetpsmet  24667  imasf1oxmet  24694  xblss2ps  24720  xblss2  24721  xblcntrps  24729  xblcntr  24730  blcld  24824  metustfbas  24876  cfilucfil  24878  restmetu  24889  ngptgp  24955  tngngpd  24972  nrmtngnrm  24977  tngnrg  24993  nlmvscn  25006  nrginvrcn  25011  nmo0  25054  nmoeq0  25055  nmoid  25061  nghmcn  25064  0nmhm  25074  blcvx  25117  iccntr  25141  xrge0tsms  25154  xmetdcn2  25157  metdstri  25171  metdscn  25176  rescncf  25218  cncfco  25228  oprpiece1res2  25273  cnheibor  25276  cnllycmp  25277  bndth  25279  ishtpyd  25296  isphtpyd  25307  pcoval2  25337  nmhmcn  25441  ipcn  25567  lmnn  25584  cfilss  25591  iscfil3  25594  cfilfcls  25595  cmetcaulem  25609  iscmet3lem2  25613  cfilres  25617  lmcau  25634  flimcfil  25635  cncmet  25643  rlmbn  25682  minveclem3b  25749  pjthlem1  25758  pjth2  25761  ivthlem3  25774  ovolssnul  25808  ovolctb  25811  ovoliunnul  25828  ovolsca  25836  ovolicopnf  25845  voliunlem2  25872  volsup  25877  dyadmaxlem  25918  vitalilem5  25933  mbfres  25965  mbfss  25967  mbfmulc2re  25969  mbfadd  25982  mbfmulc2  25984  mbflim  25989  i1faddlem  26014  i1fmullem  26015  mbfmul  26047  itg2mulc  26068  itg2cnlem1  26082  ibl0  26107  iblposlem  26112  itgreval  26117  iblneg  26123  iblss  26125  iblss2  26126  itgle  26130  iblconst  26138  iblabs  26149  iblabsr  26150  iblmulc2  26151  bddmulibl  26159  limciun  26214  limcun  26215  dvres2lem  26230  dvidlem  26235  dvcnp2  26240  dvcn  26241  cpnres  26257  dvaddbr  26258  dvmulbr  26259  dvcobr  26266  dvcjbr  26269  dvrec  26275  dvcnvlem  26296  dvferm  26308  dvlip2  26315  dveq0  26320  dv11cn  26321  dvivthlem1  26328  lhop1  26334  lhop2  26335  lhop  26336  dvcnvre  26339  dvfsumlem3  26348  dvfsumlem4  26349  dvfsumrlim  26351  dvfsum2  26354  ftc1a  26357  ftc1lem4  26359  ftc1lem6  26361  ftc1  26362  coe1mul3  26417  deg1addle2  26420  deg1sublt  26428  fta1blem  26489  drnguc1p  26492  ig1prsp  26499  plyco0  26510  plyeq0lem  26529  dgrub  26553  dgreq  26563  dgradd2  26587  dgrmul  26589  dgrcolem2  26593  dgrco  26594  plycpn  26610  plydivlem4  26617  plydiveu  26619  vieta1lem2  26634  vieta1  26635  aalioulem2  26660  aalioulem3  26661  aaliou3lem7  26676  tayl0  26689  ulmcn  26726  ulmdvlem3  26729  psercn  26753  abelth  26768  pilem3  26780  efif1olem1  26870  abslogimle  26901  argregt0  26938  argrege0  26939  logf1o2  26978  cxpsqrtlem  27030  cxpcn3  27076  abscxpbnd  27081  logreclem  27090  ang180lem2  27138  ang180lem3  27139  xrlimcnp  27296  harmonicbnd4  27338  fsumharmonic  27339  lgamgulmlem5  27360  lgambdd  27364  basellem4  27411  dvdsppwf1o  27513  dvdsflf1o  27514  fsumfldivdiaglem  27516  chpeq0  27535  chteq0  27536  chtub  27539  chpub  27547  dchrelbasd  27566  dchrmulcl  27576  dchrinv  27588  bposlem1  27611  bposlem2  27612  lgsdirprm  27658  lgsqrlem2  27674  lgsqrlem3  27675  lgsdchr  27682  lgseisenlem1  27702  lgseisenlem2  27703  lgseisenlem3  27704  lgsquadlem1  27707  2sqlem8  27753  2sqblem  27758  2sqmod  27763  chebbnd1lem1  27796  dchrisumlem1  27816  dchrisumlem2  27817  dchrisumlem3  27818  dchrisum0fno1  27838  pntrmax  27891  pntpbnd1a  27912  pntibndlem3  27919  pntlemn  27927  pntlemi  27931  pntlem3  27936  pntleml  27938  ostth1  27960  ostth2  27964  ostth3  27965  nosepon  28022  nolesgn2ores  28029  nogesgn1ores  28031  nosupres  28064  nosupbnd1lem2  28066  nosupbnd2lem1  28072  noinfres  28079  noinfbnd1lem2  28081  noinfbnd2lem1  28087  eqcuts3  28190  cofcutrtime  28313  divmuldivsd  28618  divdivs1d  28619  onsbnd  28667  nnsgt0  28725  bdayfinbndlem1  28853  ercgrg  28980  motco  29003  cnvmot  29004  legso  29062  mirmot  29147  colopp  29247  hphl  29249  lmicom  29293  lmimid  29299  lmimot  29303  hypcgrlem1  29305  hypcgrlem2  29306  trgcopyeulem  29312  inagswap  29360  inaghl  29364  cgrg3col4  29372  prlngd  29417  prlngref  29418  dfprlng2  29425  brbtwn2  29483  axlowdimlem3  29522  axlowdimlem16  29535  axcontlem8  29549  fusgrfis  29911  nbgr2vtx1edg  29931  0vtxrgr  30157  0vtxrusgr  30158  ewlkle  30186  wlk1ewlk  30220  uspgr2wlkeq2  30227  wlkp1lem8  30259  trlontrl  30293  pthonpth  30334  pthdlem2  30354  wlklnwwlkln1  30457  wlknewwlksn  30476  wwlksnred  30481  wwlksnredwwlkn0  30485  2trlond  30528  2pthond  30531  elwwlks2ons3im  30543  clwlkclwwlklem2a1  30583  clwlkclwwlkf1  30601  clwwlkel  30637  clwwlkwwlksb  30645  wwlksext2clwwlk  30648  1ewlk  30706  0trlon  30715  0pthon  30718  1pthond  30735  3trlond  30774  3pthond  30776  3spthond  30778  eupthres  30816  2clwwlk2clwwlk  30951  numclwwlk1lem2foa  30955  numclwwlk1lem2f1  30958  nvabs  31274  vacn  31296  nmcvcn  31297  nmblore  31388  0lno  31392  0blo  31394  nmlno0lem  31395  occl  31906  pjhthlem1  31993  pjpjpre  32021  nmopre  32472  nmlnop0iALT  32597  nmophmi  32633  leoprf2  32729  stlesi  32843  disjdifprg  33211  disjun0  33231  fsuppcurry1  33358  fsuppcurry2  33359  fpwrelmap  33367  fzspl  33423  dfmgc2lem  33598  pwrssmgc  33603  xrge0tsmsd  33676  psgnfzto1stlem  33703  fzto1st1  33705  evpmid  33751  pnfinf  33786  isarchiofld  33802  rmfsupp2  33840  fracfld  33912  dvdsruassoi  33981  nsgmgc  34005  qsdrngi  34061  deg1addlt  34174  ply1degltdimlem  34296  lbsdiflsp0  34300  fedgmul  34305  fldexttr  34332  fldextid  34333  irngnzply1lem  34364  finextalg  34372  minplyelirng  34389  irredminply  34390  algextdeglem8  34398  rtelextdg2lem  34400  constrsslem  34415  constrllcllem  34426  constrlccllem  34427  constrcccllem  34428  qtopt1  34509  reff  34513  locfinreflem  34514  metideq  34567  metider  34568  pstmxmet  34571  qqhval2lem  34655  qqhcn  34665  qqhucn  34666  pwsiga  34804  prsiga  34805  measle0  34883  mbfmcst  34933  1stmbfm  34934  2ndmbfm  34935  imambfm  34936  cnmbfm  34937  mbfmco  34938  mbfmco2  34939  0elcarsg  34981  carsgclctun  34995  sibfof  35014  oddpwdc  35028  eulerpartlemmf  35049  eulerpartlemgs2  35054  0rrv  35125  ballotlemfc0  35167  ballotlemfcc  35168  signstfveq0  35248  breprexplemc  35303  bnj1452  35724  usgrgt2cycl  35951  acycgr1v  35956  derangen  35979  subfacval3  35996  cvmseu  36083  cvmliftmolem2  36089  cvmliftlem7  36098  cvmliftlem15  36105  cvmlift2lem9a  36110  cvmlift2lem9  36118  cvmlift2lem10  36119  cvmlift2lem11  36120  cvmlift2lem12  36121  cvmlift3lem6  36131  cvmlift3lem8  36133  ex-sategoelel  36228  ex-sategoelelomsuc  36233  mclsppslem  36390  mclspps  36391  wsuclem  36629  nadddilem2  37012  fness  37179  fnetr  37181  fnessref  37187  refssfne  37188  neibastop1  37189  neibastop2  37191  tailfb  37207  filnetlem3  37210  weiunfrlem  37294  bj-finsumval0  38249  bj-rvecvec  38263  dfgcd3  38288  lindsadd  38579  poimirlem13  38594  poimirlem15  38596  poimirlem24  38605  poimirlem28  38609  mblfinlem2  38619  ovoliunnfl  38623  volsupnfl  38626  mbfresfi  38627  iblabsnc  38645  iblmulc2nc  38646  ftc1cnnclem  38652  ftc1cnnc  38653  ftc1anc  38662  sdclem2  38719  metf1o  38732  ismtyhmeolem  38781  ismtyres  38785  heibor1lem  38786  bfplem2  38800  bfp  38801  rrncmslem  38809  iccbnd  38817  icccmpALT  38818  rngogrphom  38948  rngoisoco  38959  keridl  39009  lsmcv2  40129  lsatcv0  40131  lcvexchlem4  40137  lcvexchlem5  40138  l1cvpat  40154  lfl0f  40169  lfladdcl  40171  lflnegcl  40175  lkrlss  40195  eqlkr  40199  lkrlsp  40202  lkrlsp2  40203  lshpkrcl  40216  lkrin  40264  1cvrjat  40575  llni  40608  llnle  40618  lplni  40632  lplnle  40640  llncvrlpln2  40657  2atmat  40661  lvoli  40675  lplncvrlvol2  40715  elpaddri  40902  paddclN  40942  pclclN  40991  pclfinN  41000  0psubclN  41043  1psubclN  41044  atpsubclN  41045  pmapsubclN  41046  osumclN  41067  pexmidN  41069  pexmidlem6N  41075  lhp2lt  41101  lautcnv  41190  idlaut  41196  lautco  41197  idldil  41214  ldilcnv  41215  ldilco  41216  ltrncnv  41246  idltrn  41250  cdleme16d  41381  cdleme50laut  41647  cdleme50ldil  41648  cdleme50ltrn  41657  ltrnco  41819  dian0  42139  dia0eldmN  42140  dia1eldmN  42141  dialss  42146  diaintclN  42158  docaclN  42224  doca2N  42226  djajN  42237  dibintclN  42267  diblss  42270  dicvaddcl  42290  dicvscacl  42291  dicn0  42292  cdlemn11a  42307  dihord2cN  42321  dihord11b  42322  dihord6apre  42356  dihmeetlem1N  42390  dihglblem5apreN  42391  dihpN  42436  dihjatcclem4  42521  dochkr1  42578  islpoldN  42584  lcfrlem31  42673  mapdpglem18  42789  mapdheq2  42829  mapdheq4  42832  mapdh6aN  42835  hdmap1l6a  42909  hdmap14lem4a  42971  lcmineqlem4  43125  frlmfzoccat  43615  drnginvmuld  43631  evlselvlem  43659  evlselv  43660  fsuppind  43661  fsuppssind  43664  prjspvs  43681  frlmnzcoordsca  43701  prjspnnorm  43704  irrapxlem4  43875  pell1234qrdich  43911  pell1qr1  43921  pell14qrgap  43925  pellqrexplicit  43927  rmspecfund  43959  fzmaxdif  44031  acongeq  44033  jm2.23  44046  jm3.1  44070  lmhmlnmsplit  44132  hbt  44175  dgrsub2  44180  proot1ex  44241  cantnfub  44366  cantnfresb  44369  cantnf2  44370  tfsconcatfv2  44385  tfsconcatrn  44387  tfsconcatb0  44389  naddcnff  44407  naddcnffo  44409  naddcnfid1  44412  naddcnfid2  44413  clublem  44653  dftrcl3  44763  mnugrud  45311  hashnzfz2  45348  dvconstbi  45361  ubelsupr  46080  restopn3  46209  wessf1ornlem  46243  lefldiveq  46351  iccintsng  46578  climsuse  46663  mullimc  46671  limcdm0  46673  limccog  46675  mullimcf  46678  constlimc  46679  idlimc  46681  limcperiod  46683  limsupre  46694  limcleqr  46697  neglimc  46700  addlimc  46701  0ellimcdiv  46702  xlimliminflimsup  46915  cncfshift  46927  cncfperiod  46932  cncfuni  46939  icccncfext  46940  cncfiooicclem1  46946  fperdvper  46972  ioodvbdlimc1lem2  46985  ioodvbdlimc2lem  46987  mbfres2cn  47011  iblsplit  47019  stoweidlem7  47060  stoweidlem13  47066  stoweidlem26  47079  wallispilem3  47120  stirlinglem6  47132  stirlinglem10  47136  dirkercncf  47160  fourierdlem6  47166  fourierdlem11  47171  fourierdlem12  47172  fourierdlem15  47175  fourierdlem26  47186  fourierdlem42  47202  fourierdlem50  47209  fourierdlem51  47210  fourierdlem52  47211  fourierdlem54  47213  fourierdlem62  47221  fourierdlem79  47238  fourierdlem102  47261  fourierdlem114  47273  etransclem23  47310  chnsubseq  47933  3f1oss1  48188  zgeltp1eq  48422  nnmul2  48443  setsnidel  48502  preimafvsnel  48504  iccpartres  48543  prpair  48626  fpprel2  48882  isubgrsubgr  49010  grimidvtxedg  49026  grimcnv  49029  isuspgrim  49037  upgrimpthslem2  49049  stgrnbgr0  49105  uhgrimgrlim  49128  clnbgr3stgrgrlim  49160  gpg5nbgrvtx03starlem2  49210  gpg5nbgrvtx13starlem2  49213  gpg5edgnedg  49271  isassintop  49350  rhmsubcALTV  49425  srhmsubcALTV  49465  fldhmsubcALTV  49473  rmfsupp  49528  scmfsupp  49530  mptcfsupp  49532  lcoel0  49583  lincsumcl  49586  lincscmcl  49587  lcoss  49591  lindsrng01  49623  lincreslvec3  49637  lindssnlvec  49641  zgtp1leeq  49676  lubsscl  50111  glbsscl  50112  idmon  50171  idepi  50172  iinfssc  50208  iinfsubc  50209  discsubc  50215  nelsubclem  50218  imassc  50304  imasubc3  50307  isnatd  50374  swapfiso  50436  fucoppc  50561  thinciso  50621  diagciso  50690  termolmd  50821  wrdf1d  50983