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  7000  fveqressseq  7020  fmptsng  7112  fmptsnd  7113  fnprb  7152  fntpb  7153  fpr3g  8224  frrlem4  8228  1ellim  8422  isfsuppd  9268  fdmfifsupp  9277  fsuppmptif  9301  fsuppco2  9305  fsuppcor  9306  dffi3  9333  suppr  9374  infpr  9407  ordtypelem7  9428  cantnf0  9585  cantnfp1lem1  9588  cantnfp1lem2  9589  cantnfp1lem3  9590  cantnflem1a  9595  cantnflem1d  9598  cantnflem1  9599  cantnf  9603  rankpwi  9736  carduni  9894  fin23lem32  10255  fpwwe2lem5  10547  fpwwe2lem11  10553  fpwwe2lem12  10554  fpwwe2  10555  inttsk  10686  grutsk1  10733  add20  11651  supaddc  12112  supadd  12113  supmul  12117  suprzcl  12598  uzid  12792  uzwo3  12882  rpnnen1lem5  12920  xrletrid  13095  xrre  13110  xrre3  13112  xleadd1a  13194  xlemul1a  13229  elioc2  13351  elico2  13352  elicc2  13353  elfz1eq  13478  fzadd2  13502  fznatpl1  13521  elfz1uz  13537  nn0fz0  13568  fzctr  13583  fzo1fzo0n0  13659  fzoaddel  13661  elincfzoext  13667  flid  13756  flval3  13763  fladdz  13773  fldiv  13808  modid  13844  hashf1lem1  14406  pfxccatin12d  14696  repswpfx  14736  2cshw  14764  pfx2  14898  wwlktovf1  14908  sqeqd  15117  01sqrexlem7  15199  max0add  15261  abs2difabs  15286  rddif  15292  fzomaxdiflem  15294  rexico  15305  icodiamlt  15389  limsupgre  15432  rlim3  15449  icco1  15491  rlimclim  15497  rlimuni  15501  rlimresb  15516  isercolllem2  15617  isercolllem3  15618  isercoll  15619  caucvgrlem  15624  caurcvgr  15625  iseraltlem3  15635  fsum00  15750  o1fsum  15765  bitsfzolem  16392  bitsfzo  16393  bitsmod  16394  bitscmp  16396  gcd0id  16477  gcdneg  16480  bezoutlem4  16500  nn0seqcvgd  16528  lcmneg  16561  lcmfunsnlem2lem2  16597  qredeq  16615  prmind2  16643  eulerthlem2  16741  pcpremul  16803  pcidlem  16832  pcgcd1  16837  fldivp1  16857  pcfaclem  16858  4sqlem17  16921  vdwlem1  16941  vdwlem6  16946  vdwlem12  16952  vdwlem13  16953  0ram  16980  ram0  16982  ramub1lem1  16986  invco  17727  sectmon  17738  monsect  17739  invid  17743  ssctr  17781  ssceq  17782  0ssc  17793  0subcat  17794  catsubcat  17795  issubc3  17805  fullsubc  17806  funcinv  17829  fthmon  17885  fuccocl  17923  fucidcl  17924  invfuc  17933  2initoinv  17966  2termoinv  17973  elhomai  17989  setcmon  18043  setcepi  18044  catcisolem  18066  curf2cl  18186  yonedalem4c  18232  yonedalem3  18235  yoniso  18240  lublecl  18314  isacs3lem  18497  tsrdir  18559  chnccat  18581  rabsubmgmd  18661  submgmid  18663  subsubmgm  18667  mgmhmima  18672  mgmhmeql  18673  mndpfsupp  18724  mnd1  18736  sgrp2nmndlem4  18888  sgrp2nmndlem5  18889  0subg  19116  nmznsg  19132  ghmpreima  19202  ghmeql  19203  ghmnsgpreima  19205  kerf1ghm  19211  cntzsgrpcl  19298  cntzsubm  19302  cntzsubg  19303  cntzmhm  19305  symgextfo  19386  symgfixf1  19401  symgfixfolem1  19402  odlem2  19503  finodsubmsubg  19531  gexlem2  19546  gexcl2  19553  sylow1lem5  19566  subgslw  19580  slwhash  19588  fislw  19589  sylow3lem1  19591  lsmsubg  19618  efgredlemd  19708  efgredlem  19711  efgcpbllemb  19719  frgpuplem  19736  cyggeninv  19847  iscygd  19851  iscygodd  19852  gsumzadd  19886  gsumconst  19898  gsumpt  19926  gsum2dlem2  19935  gsum2d  19936  gsum2d2lem  19937  dprdfcntz  19981  eldprdi  19984  subgdmdprd  20000  subgdprd  20001  dprdpr  20016  ablfac1c  20037  ablfac1eu  20039  ablfaclem3  20053  ogrpaddlt  20102  ogrpsublt  20106  ring1  20280  subrngint  20526  rhmimasubrng  20532  cntzsubrng  20533  rhmeql  20569  rhmima  20570  cntzsubr  20572  rnghmsscmap2  20595  rnghmsscmap  20596  rnghmsubcsetc  20599  zrzeroorngc  20610  rhmsscmap2  20624  rhmsscmap  20625  rhmsubcsetc  20628  rhmsscrnghm  20631  rhmsubcrngc  20634  srhmsubc  20646  rhmsubc  20655  issubdrg  20746  fldhmsubc  20751  imadrhmcl  20763  isabvd  20778  abvdiv  20795  ornglmullt  20835  orngrmullt  20836  orngmullt  20837  ofldlt1  20841  lsslsp  20999  lmhmima  21031  lmhmpreima  21032  lmhmeql  21039  lsmcl  21067  lspfixed  21115  rnglidlrng  21234  rngqiprngim  21291  rng2idl1cntr  21292  qsssubdrg  21395  gzrngunit  21402  pzriprnglem8  21457  evpmodpmf1o  21565  ocvpj  21686  dsmm0cl  21709  dsmmacl  21710  dsmmsubg  21712  dsmmlss  21713  frlmsplit2  21742  uvcff  21760  lindfrn  21790  f1lindf  21791  lindsss  21793  issubassa  21836  issubassa2  21861  snifpsrbag  21889  psrbaglesupp  21891  psrbaglecl  21892  psrbagaddcl  21893  psrbagcon  21894  mplsubglem  21966  mpllsslem  21967  mplassa  21989  subrgmpl  21999  mplcoe5  22007  mplbas2  22009  mplind  22037  mpfind  22082  ismhp2  22096  mhpmulcl  22104  mhplss  22110  ply1assa  22151  coe1tmmul2  22229  coe1tmmul  22230  cply1coe0bi  22255  dmatid  22448  dmatsubcl  22451  dmatscmcl  22456  scmatid  22467  scmataddcl  22469  scmatsubcl  22470  scmatmulcl  22471  smatvscl  22477  scmatrhmcl  22481  mat0scmat  22491  mat1scmat  22492  mdet0pr  22545  chmaidscmat  22801  distop  22948  indistopon  22954  ppttop  22960  epttop  22962  mretopd  23045  toponmre  23046  neiss  23062  opnneissb  23067  ssnei2  23069  innei  23078  neiptoptop  23084  ordtcld1  23150  ordtcld2  23151  lmconst  23214  cnpnei  23217  iscncl  23222  cnss1  23229  cnss2  23230  cncnpi  23231  cncnp  23233  cnconst2  23236  cnrest  23238  cnpresti  23241  cnpdis  23246  paste  23247  lmcnp  23257  cnhaus  23307  hauscmp  23360  2ndcomap  23411  1stcelcls  23414  1stccnp  23415  llyrest  23438  nllyrest  23439  llyidm  23441  nllyidm  23442  ssref  23465  reftr  23467  refun0  23468  dissnref  23481  kgentopon  23491  kgenidm  23500  kgencn3  23511  txcld  23556  neitx  23560  tx1cn  23562  tx2cn  23563  ptcld  23566  xkoccn  23572  txcnp  23573  ptcnp  23575  txcnmpt  23577  ptcn  23580  txdis1cn  23588  ptrescn  23592  txkgen  23605  xkoco1cn  23610  xkoco2cn  23611  xkococn  23613  xkoinjcn  23640  qtoptop2  23652  qtopuni  23655  qtopid  23658  qtopkgen  23663  basqtop  23664  tgqtop  23665  qtopss  23668  qtopeu  23669  qtoprest  23670  kqopn  23687  kqcld  23688  kqreglem2  23695  reghmph  23746  ordthmeolem  23754  qtopf1  23769  opnfbas  23795  isfil2  23809  fbasweak  23818  fsubbas  23820  filconn  23836  fbasrn  23837  rnelfmlem  23905  flimss2  23925  flimss1  23926  hausflim  23934  flimclslem  23937  flimsncls  23939  cnpflfi  23952  flfcnp2  23960  fclsfnflim  23980  cnextfvval  24018  cnextfres1  24021  symgtgp  24059  opnsubg  24061  ghmcnp  24068  qustgpopn  24073  qustgplem  24074  qustgphaus  24076  tsmsfbas  24081  ustfilxp  24166  utoptop  24187  utopbas  24188  restutopopn  24191  iducn  24235  cstucnd  24236  ucncn  24237  fmucnd  24244  cfilufg  24245  trcfilu  24246  cfiluweak  24247  neipcfilu  24248  psmetres2  24267  isxmetd  24279  xmetpsmet  24301  imasf1oxmet  24328  xblss2ps  24354  xblss2  24355  xblcntrps  24363  xblcntr  24364  blcld  24458  metustfbas  24510  cfilucfil  24512  restmetu  24523  ngptgp  24589  tngngpd  24606  nrmtngnrm  24611  tngnrg  24627  nlmvscn  24640  nrginvrcn  24645  nmo0  24688  nmoeq0  24689  nmoid  24695  nghmcn  24698  0nmhm  24708  blcvx  24751  iccntr  24775  xrge0tsms  24788  xmetdcn2  24791  metdstri  24805  metdscn  24810  rescncf  24852  cncfco  24862  oprpiece1res2  24907  cnheibor  24910  cnllycmp  24911  bndth  24913  ishtpyd  24930  isphtpyd  24941  pcoval2  24971  nmhmcn  25075  ipcn  25201  lmnn  25218  cfilss  25225  iscfil3  25228  cfilfcls  25229  cmetcaulem  25243  iscmet3lem2  25247  cfilres  25251  lmcau  25268  flimcfil  25269  cncmet  25277  rlmbn  25316  minveclem3b  25383  pjthlem1  25392  pjth2  25395  ivthlem3  25408  ovolssnul  25442  ovolctb  25445  ovoliunnul  25462  ovolsca  25470  ovolicopnf  25479  voliunlem2  25506  volsup  25511  dyadmaxlem  25552  vitalilem5  25567  mbfres  25599  mbfss  25601  mbfmulc2re  25603  mbfadd  25616  mbfmulc2  25618  mbflim  25623  i1faddlem  25648  i1fmullem  25649  mbfmul  25681  itg2mulc  25702  itg2cnlem1  25716  ibl0  25742  iblposlem  25747  itgreval  25752  iblneg  25758  iblss  25760  iblss2  25761  itgle  25765  iblconst  25773  iblabs  25784  iblabsr  25785  iblmulc2  25786  bddmulibl  25794  limciun  25849  limcun  25850  dvres2lem  25865  dvidlem  25870  dvcnp2  25875  dvcn  25876  cpnres  25892  dvaddbr  25893  dvmulbr  25894  dvcobr  25901  dvcjbr  25904  dvrec  25910  dvcnvlem  25931  dvferm  25943  dvlip2  25950  dveq0  25955  dv11cn  25956  dvivthlem1  25963  lhop1  25969  lhop2  25970  lhop  25971  dvcnvre  25974  dvfsumlem3  25983  dvfsumlem4  25984  dvfsumrlim  25986  dvfsum2  25989  ftc1a  25992  ftc1lem4  25994  ftc1lem6  25996  ftc1  25997  coe1mul3  26052  deg1addle2  26055  deg1sublt  26063  fta1blem  26124  drnguc1p  26127  ig1prsp  26134  plyco0  26145  plyeq0lem  26163  dgrub  26187  dgreq  26197  dgradd2  26221  dgrmul  26223  dgrcolem2  26227  dgrco  26228  plycpn  26243  plydivlem4  26250  plydiveu  26252  vieta1lem2  26265  vieta1  26266  aalioulem2  26287  aalioulem3  26288  aaliou3lem7  26303  tayl0  26315  ulmcn  26352  ulmdvlem3  26355  psercn  26379  abelth  26394  pilem3  26406  efif1olem1  26494  abslogimle  26525  argregt0  26562  argrege0  26563  logf1o2  26602  cxpsqrtlem  26654  cxpcn3  26700  abscxpbnd  26705  logreclem  26714  ang180lem2  26762  ang180lem3  26763  xrlimcnp  26920  harmonicbnd4  26962  fsumharmonic  26963  lgamgulmlem5  26984  lgambdd  26988  basellem4  27035  dvdsppwf1o  27137  dvdsflf1o  27138  fsumfldivdiaglem  27140  chpeq0  27159  chteq0  27160  chtub  27163  chpub  27171  dchrelbasd  27190  dchrmulcl  27200  dchrinv  27212  bposlem1  27235  bposlem2  27236  lgsdirprm  27282  lgsqrlem2  27298  lgsqrlem3  27299  lgsdchr  27306  lgseisenlem1  27326  lgseisenlem2  27327  lgseisenlem3  27328  lgsquadlem1  27331  2sqlem8  27377  2sqblem  27382  2sqmod  27387  chebbnd1lem1  27420  dchrisumlem1  27440  dchrisumlem2  27441  dchrisumlem3  27442  dchrisum0fno1  27462  pntrmax  27515  pntpbnd1a  27536  pntibndlem3  27543  pntlemn  27551  pntlemi  27555  pntlem3  27560  pntleml  27562  ostth1  27584  ostth2  27588  ostth3  27589  nosepon  27617  nolesgn2ores  27624  nogesgn1ores  27626  nosupres  27659  nosupbnd1lem2  27661  nosupbnd2lem1  27667  noinfres  27674  noinfbnd1lem2  27676  noinfbnd2lem1  27682  eqcuts3  27784  cofcutrtime  27907  divmuldivsd  28212  divdivs1d  28213  onsbnd  28261  nnsgt0  28319  bdayfinbndlem1  28447  ercgrg  28573  motco  28596  cnvmot  28597  legso  28655  mirmot  28731  colopp  28825  hphl  28827  lmicom  28844  lmimid  28850  lmimot  28854  hypcgrlem1  28855  hypcgrlem2  28856  trgcopyeulem  28861  inagswap  28897  inaghl  28901  cgrg3col4  28909  brbtwn2  28962  axlowdimlem3  29001  axlowdimlem16  29014  axcontlem8  29028  fusgrfis  29387  nbgr2vtx1edg  29407  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  30731  vacn  30753  nmcvcn  30754  nmblore  30845  0lno  30849  0blo  30851  nmlno0lem  30852  occl  31363  pjhthlem1  31450  pjpjpre  31478  nmopre  31929  nmlnop0iALT  32054  nmophmi  32090  leoprf2  32186  stlesi  32300  disjdifprg  32633  disjun0  32653  fsuppcurry1  32785  fsuppcurry2  32786  fpwrelmap  32794  fzspl  32850  dfmgc2lem  33043  pwrssmgc  33048  xrge0tsmsd  33122  psgnfzto1stlem  33149  fzto1st1  33151  evpmid  33197  pnfinf  33232  isarchiofld  33248  rmfsupp2  33287  fracfld  33357  dvdsruassoi  33432  nsgmgc  33460  drngidl  33481  qsdrngi  33543  deg1addlt  33648  ply1degltdimlem  33754  lbsdiflsp0  33758  fedgmul  33763  fldexttr  33790  fldextid  33791  irngnzply1lem  33822  finextalg  33830  minplyelirng  33847  irredminply  33848  algextdeglem8  33856  rtelextdg2lem  33858  constrsslem  33873  constrllcllem  33884  constrlccllem  33885  constrcccllem  33886  qtopt1  33967  reff  33971  locfinreflem  33972  metideq  34025  metider  34026  pstmxmet  34029  qqhval2lem  34113  qqhcn  34123  qqhucn  34124  pwsiga  34262  prsiga  34263  measle0  34340  mbfmcst  34391  1stmbfm  34392  2ndmbfm  34393  imambfm  34394  cnmbfm  34395  mbfmco  34396  mbfmco2  34397  0elcarsg  34439  carsgclctun  34453  sibfof  34472  oddpwdc  34486  eulerpartlemmf  34507  eulerpartlemgs2  34512  0rrv  34583  ballotlemfc0  34625  ballotlemfcc  34626  signstfveq0  34709  breprexplemc  34764  bnj1452  35182  usgrgt2cycl  35300  acycgr1v  35319  derangen  35342  subfacval3  35359  cvmseu  35446  cvmliftmolem2  35452  cvmliftlem7  35461  cvmliftlem15  35468  cvmlift2lem9a  35473  cvmlift2lem9  35481  cvmlift2lem10  35482  cvmlift2lem11  35483  cvmlift2lem12  35484  cvmlift3lem6  35494  cvmlift3lem8  35496  ex-sategoelel  35591  ex-sategoelelomsuc  35596  mclsppslem  35753  mclspps  35754  wsuclem  35993  fness  36519  fnetr  36521  fnessref  36527  refssfne  36528  neibastop1  36529  neibastop2  36531  tailfb  36547  filnetlem3  36550  weiunfrlem  36634  bj-finsumval0  37587  bj-rvecvec  37601  dfgcd3  37626  lindsadd  37922  poimirlem13  37942  poimirlem15  37944  poimirlem24  37953  poimirlem28  37957  mblfinlem2  37967  ovoliunnfl  37971  volsupnfl  37974  mbfresfi  37975  iblabsnc  37993  iblmulc2nc  37994  ftc1cnnclem  38000  ftc1cnnc  38001  ftc1anc  38010  sdclem2  38051  metf1o  38064  ismtyhmeolem  38113  ismtyres  38117  heibor1lem  38118  bfplem2  38132  bfp  38133  rrncmslem  38141  iccbnd  38149  icccmpALT  38150  rngogrphom  38280  rngoisoco  38291  keridl  38341  lsmcv2  39463  lsatcv0  39465  lcvexchlem4  39471  lcvexchlem5  39472  l1cvpat  39488  lfl0f  39503  lfladdcl  39505  lflnegcl  39509  lkrlss  39529  eqlkr  39533  lkrlsp  39536  lkrlsp2  39537  lshpkrcl  39550  lkrin  39598  1cvrjat  39909  llni  39942  llnle  39952  lplni  39966  lplnle  39974  llncvrlpln2  39991  2atmat  39995  lvoli  40009  lplncvrlvol2  40049  elpaddri  40236  paddclN  40276  pclclN  40325  pclfinN  40334  0psubclN  40377  1psubclN  40378  atpsubclN  40379  pmapsubclN  40380  osumclN  40401  pexmidN  40403  pexmidlem6N  40409  lhp2lt  40435  lautcnv  40524  idlaut  40530  lautco  40531  idldil  40548  ldilcnv  40549  ldilco  40550  ltrncnv  40580  idltrn  40584  cdleme16d  40715  cdleme50laut  40981  cdleme50ldil  40982  cdleme50ltrn  40991  ltrnco  41153  dian0  41473  dia0eldmN  41474  dia1eldmN  41475  dialss  41480  diaintclN  41492  docaclN  41558  doca2N  41560  djajN  41571  dibintclN  41601  diblss  41604  dicvaddcl  41624  dicvscacl  41625  dicn0  41626  cdlemn11a  41641  dihord2cN  41655  dihord11b  41656  dihord6apre  41690  dihmeetlem1N  41724  dihglblem5apreN  41725  dihpN  41770  dihjatcclem4  41855  dochkr1  41912  islpoldN  41918  lcfrlem31  42007  mapdpglem18  42123  mapdheq2  42163  mapdheq4  42166  mapdh6aN  42169  hdmap1l6a  42243  hdmap14lem4a  42305  lcmineqlem4  42459  frlmfzoccat  42938  drnginvmuld  42960  psrbagres  42977  evlselvlem  43007  evlselv  43008  fsuppind  43011  fsuppssind  43014  prjspvs  43031  irrapxlem4  43241  pell1234qrdich  43277  pell1qr1  43287  pell14qrgap  43291  pellqrexplicit  43293  rmspecfund  43325  fzmaxdif  43397  acongeq  43399  jm2.23  43412  jm3.1  43436  lmhmlnmsplit  43503  hbt  43546  dgrsub2  43551  proot1ex  43612  cantnfub  43737  cantnfresb  43740  cantnf2  43741  tfsconcatfv2  43756  tfsconcatrn  43758  tfsconcatb0  43760  naddcnff  43778  naddcnffo  43780  naddcnfid1  43783  naddcnfid2  43784  clublem  44025  dftrcl3  44135  mnugrud  44699  hashnzfz2  44736  dvconstbi  44749  ubelsupr  45439  restopn3  45569  wessf1ornlem  45603  lefldiveq  45713  iccintsng  45941  climsuse  46026  mullimc  46034  limcdm0  46036  limccog  46038  mullimcf  46041  constlimc  46042  idlimc  46044  limcperiod  46046  limsupre  46057  limcleqr  46060  neglimc  46063  addlimc  46064  0ellimcdiv  46065  xlimliminflimsup  46278  cncfshift  46290  cncfperiod  46295  cncfuni  46302  icccncfext  46303  cncfiooicclem1  46309  fperdvper  46335  ioodvbdlimc1lem2  46348  ioodvbdlimc2lem  46350  mbfres2cn  46374  iblsplit  46382  stoweidlem7  46423  stoweidlem13  46429  stoweidlem26  46442  wallispilem3  46483  stirlinglem6  46495  stirlinglem10  46499  dirkercncf  46523  fourierdlem6  46529  fourierdlem11  46534  fourierdlem12  46535  fourierdlem15  46538  fourierdlem26  46549  fourierdlem42  46565  fourierdlem50  46572  fourierdlem51  46573  fourierdlem52  46574  fourierdlem54  46576  fourierdlem62  46584  fourierdlem79  46601  fourierdlem102  46624  fourierdlem114  46636  etransclem23  46673  chnsubseq  47298  3f1oss1  47511  zgeltp1eq  47745  nnmul2  47766  setsnidel  47825  preimafvsnel  47827  iccpartres  47866  prpair  47949  fpprel2  48205  isubgrsubgr  48333  grimidvtxedg  48349  grimcnv  48352  isuspgrim  48360  upgrimpthslem2  48372  stgrnbgr0  48428  uhgrimgrlim  48451  clnbgr3stgrgrlim  48483  gpg5nbgrvtx03starlem2  48533  gpg5nbgrvtx13starlem2  48536  gpg5edgnedg  48594  isassintop  48674  rhmsubcALTV  48749  srhmsubcALTV  48789  fldhmsubcALTV  48797  rmfsupp  48837  scmfsupp  48839  mptcfsupp  48841  lcoel0  48892  lincsumcl  48895  lincscmcl  48896  lcoss  48900  lindsrng01  48932  lincreslvec3  48946  lindssnlvec  48950  zgtp1leeq  48985  lubsscl  49423  glbsscl  49424  idmon  49483  idepi  49484  iinfssc  49520  iinfsubc  49521  discsubc  49527  nelsubclem  49530  imassc  49616  imasubc3  49619  isnatd  49686  swapfiso  49748  fucoppc  49873  thinciso  49933  diagciso  50002  termolmd  50133