Theorem mpbir2and 713

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  7078  fveqressseq  7098  fmptsng  7187  fmptsnd  7188  fnprb  7227  fntpb  7228  fpr3g  8308  frrlem4  8312  1ellim  8534  isfsuppd  9403  fdmfifsupp  9412  fczfsuppd  9423  fsuppmptif  9436  fsuppco2  9440  fsuppcor  9441  dffi3  9468  suppr  9508  infpr  9540  ordtypelem7  9561  cantnf0  9712  cantnfp1lem1  9715  cantnfp1lem2  9716  cantnfp1lem3  9717  cantnflem1a  9722  cantnflem1d  9725  cantnflem1  9726  cantnf  9730  rankpwi  9860  carduni  10018  fin23lem32  10381  fpwwe2lem5  10672  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  inttsk  10811  grutsk1  10858  add20  11772  supaddc  12232  supadd  12233  supmul  12237  suprzcl  12695  uzid  12890  uzwo3  12982  rpnnen1lem5  13020  xrletrid  13193  xrre  13207  xrre3  13209  xleadd1a  13291  xlemul1a  13326  elioc2  13446  elico2  13447  elicc2  13448  elfz1eq  13571  fzadd2  13595  fznatpl1  13614  elfz1uz  13630  nn0fz0  13661  fzctr  13676  fzo1fzo0n0  13750  fzoaddel  13752  elincfzoext  13758  flid  13844  flval3  13851  fladdz  13861  fldiv  13896  modid  13932  hashf1lem1  14490  pfxccatin12d  14779  repswpfx  14819  2cshw  14847  pfx2  14982  wwlktovf1  14992  sqeqd  15201  01sqrexlem7  15283  max0add  15345  abs2difabs  15369  rddif  15375  fzomaxdiflem  15377  rexico  15388  icodiamlt  15470  limsupgre  15513  rlim3  15530  icco1  15572  rlimclim  15578  rlimuni  15582  rlimresb  15597  isercolllem2  15698  isercolllem3  15699  isercoll  15700  caucvgrlem  15705  caurcvgr  15706  iseraltlem3  15716  fsum00  15830  o1fsum  15845  bitsfzolem  16467  bitsfzo  16468  bitsmod  16469  bitscmp  16471  gcd0id  16552  gcdneg  16555  bezoutlem4  16575  nn0seqcvgd  16603  lcmneg  16636  lcmfunsnlem2lem2  16672  qredeq  16690  prmind2  16718  eulerthlem2  16815  pcpremul  16876  pcidlem  16905  pcgcd1  16910  fldivp1  16930  pcfaclem  16931  4sqlem17  16994  vdwlem1  17014  vdwlem6  17019  vdwlem12  17025  vdwlem13  17026  0ram  17053  ram0  17055  ramub1lem1  17059  invco  17818  sectmon  17829  monsect  17830  invid  17834  ssctr  17872  ssceq  17873  0ssc  17887  0subcat  17888  catsubcat  17889  issubc3  17899  fullsubc  17900  funcinv  17923  fthmon  17980  fuccocl  18020  fucidcl  18021  invfuc  18030  2initoinv  18063  2termoinv  18070  elhomai  18086  setcmon  18140  setcepi  18141  catcisolem  18163  curf2cl  18287  yonedalem4c  18333  yonedalem3  18336  yoniso  18341  lublecl  18418  isacs3lem  18599  tsrdir  18661  rabsubmgmd  18729  submgmid  18731  subsubmgm  18735  mgmhmima  18740  mgmhmeql  18741  mndpfsupp  18792  mnd1  18804  sgrp2nmndlem4  18953  sgrp2nmndlem5  18954  0subg  19181  nmznsg  19198  ghmpreima  19268  ghmeql  19269  ghmnsgpreima  19271  kerf1ghm  19277  cntzsgrpcl  19364  cntzsubm  19368  cntzsubg  19369  cntzmhm  19371  symgextfo  19454  symgfixf1  19469  symgfixfolem1  19470  odlem2  19571  finodsubmsubg  19599  gexlem2  19614  gexcl2  19621  sylow1lem5  19634  subgslw  19648  slwhash  19656  fislw  19657  sylow3lem1  19659  lsmsubg  19686  efgredlemd  19776  efgredlem  19779  efgcpbllemb  19787  frgpuplem  19804  cyggeninv  19915  iscygd  19919  iscygodd  19920  gsumzadd  19954  gsumconst  19966  gsumpt  19994  gsum2dlem2  20003  gsum2d  20004  gsum2d2lem  20005  dprdfcntz  20049  eldprdi  20052  subgdmdprd  20068  subgdprd  20069  dprdpr  20084  ablfac1c  20105  ablfac1eu  20107  ablfaclem3  20121  ring1  20323  subrngint  20576  rhmimasubrng  20582  cntzsubrng  20583  rhmeql  20619  rhmima  20620  cntzsubr  20622  rnghmsscmap2  20645  rnghmsscmap  20646  rnghmsubcsetc  20649  zrzeroorngc  20660  rhmsscmap2  20674  rhmsscmap  20675  rhmsubcsetc  20678  rhmsscrnghm  20681  rhmsubcrngc  20684  srhmsubc  20696  rhmsubc  20705  issubdrg  20797  fldhmsubc  20802  imadrhmcl  20814  isabvd  20829  abvdiv  20846  lsslsp  21030  lsslspOLD  21031  lmhmima  21063  lmhmpreima  21064  lmhmeql  21071  lsmcl  21099  lspfixed  21147  rnglidlrng  21274  rngqiprngim  21331  rng2idl1cntr  21332  qsssubdrg  21461  gzrngunit  21468  pzriprnglem8  21516  evpmodpmf1o  21631  ocvpj  21754  dsmm0cl  21777  dsmmacl  21778  dsmmsubg  21780  dsmmlss  21781  frlmsplit2  21810  uvcff  21828  lindfrn  21858  f1lindf  21859  lindsss  21861  issubassa  21904  issubassa2  21929  snifpsrbag  21957  psrbaglesupp  21959  psrbaglecl  21960  psrbagaddcl  21961  psrbagcon  21962  mplsubglem  22036  mpllsslem  22037  mplassa  22059  subrgmpl  22067  mplcoe5  22075  mplbas2  22077  mplind  22111  mpfind  22148  ismhp2  22162  mhpmulcl  22170  mhplss  22176  ply1assa  22216  coe1tmmul2  22294  coe1tmmul  22295  cply1coe0bi  22321  dmatid  22516  dmatsubcl  22519  dmatscmcl  22524  scmatid  22535  scmataddcl  22537  scmatsubcl  22538  scmatmulcl  22539  smatvscl  22545  scmatrhmcl  22549  mat0scmat  22559  mat1scmat  22560  mdet0pr  22613  chmaidscmat  22869  distop  23017  indistopon  23023  ppttop  23029  epttop  23031  mretopd  23115  toponmre  23116  neiss  23132  opnneissb  23137  ssnei2  23139  innei  23148  neiptoptop  23154  ordtcld1  23220  ordtcld2  23221  lmconst  23284  cnpnei  23287  iscncl  23292  cnss1  23299  cnss2  23300  cncnpi  23301  cncnp  23303  cnconst2  23306  cnrest  23308  cnpresti  23311  cnpdis  23316  paste  23317  lmcnp  23327  cnhaus  23377  hauscmp  23430  2ndcomap  23481  1stcelcls  23484  1stccnp  23485  llyrest  23508  nllyrest  23509  llyidm  23511  nllyidm  23512  ssref  23535  reftr  23537  refun0  23538  dissnref  23551  kgentopon  23561  kgenidm  23570  kgencn3  23581  txcld  23626  neitx  23630  tx1cn  23632  tx2cn  23633  ptcld  23636  xkoccn  23642  txcnp  23643  ptcnp  23645  txcnmpt  23647  ptcn  23650  txdis1cn  23658  ptrescn  23662  txkgen  23675  xkoco1cn  23680  xkoco2cn  23681  xkococn  23683  xkoinjcn  23710  qtoptop2  23722  qtopuni  23725  qtopid  23728  qtopkgen  23733  basqtop  23734  tgqtop  23735  qtopss  23738  qtopeu  23739  qtoprest  23740  kqopn  23757  kqcld  23758  kqreglem2  23765  reghmph  23816  ordthmeolem  23824  qtopf1  23839  opnfbas  23865  isfil2  23879  fbasweak  23888  fsubbas  23890  filconn  23906  fbasrn  23907  rnelfmlem  23975  flimss2  23995  flimss1  23996  hausflim  24004  flimclslem  24007  flimsncls  24009  cnpflfi  24022  flfcnp2  24030  fclsfnflim  24050  cnextfvval  24088  cnextfres1  24091  symgtgp  24129  opnsubg  24131  ghmcnp  24138  qustgpopn  24143  qustgplem  24144  qustgphaus  24146  tsmsfbas  24151  ustfilxp  24236  utoptop  24258  utopbas  24259  restutopopn  24262  iducn  24307  cstucnd  24308  ucncn  24309  fmucnd  24316  cfilufg  24317  trcfilu  24318  cfiluweak  24319  neipcfilu  24320  psmetres2  24339  isxmetd  24351  xmetpsmet  24373  imasf1oxmet  24400  xblss2ps  24426  xblss2  24427  xblcntrps  24435  xblcntr  24436  blcld  24533  metustfbas  24585  cfilucfil  24587  restmetu  24598  ngptgp  24664  tngngpd  24689  nrmtngnrm  24694  tngnrg  24710  nlmvscn  24723  nrginvrcn  24728  nmo0  24771  nmoeq0  24772  nmoid  24778  nghmcn  24781  0nmhm  24791  blcvx  24833  iccntr  24856  xrge0tsms  24869  xmetdcn2  24872  metdstri  24886  metdscn  24891  rescncf  24936  cncfco  24946  oprpiece1res2  24996  cnheibor  25000  cnllycmp  25001  bndth  25003  ishtpyd  25020  isphtpyd  25031  pcoval2  25062  nmhmcn  25166  ipcn  25293  lmnn  25310  cfilss  25317  iscfil3  25320  cfilfcls  25321  cmetcaulem  25335  iscmet3lem2  25339  cfilres  25343  lmcau  25360  flimcfil  25361  cncmet  25369  rlmbn  25408  minveclem3b  25475  pjthlem1  25484  pjth2  25487  ivthlem3  25501  ovolssnul  25535  ovolctb  25538  ovoliunnul  25555  ovolsca  25563  ovolicopnf  25572  voliunlem2  25599  volsup  25604  dyadmaxlem  25645  vitalilem5  25660  mbfres  25692  mbfss  25694  mbfmulc2re  25696  mbfadd  25709  mbfmulc2  25711  mbflim  25716  i1faddlem  25741  i1fmullem  25742  mbfmul  25775  itg2mulc  25796  itg2cnlem1  25810  ibl0  25836  iblposlem  25841  itgreval  25846  iblneg  25852  iblss  25854  iblss2  25855  itgle  25859  iblconst  25867  iblabs  25878  iblabsr  25879  iblmulc2  25880  bddmulibl  25888  limciun  25943  limcun  25944  dvres2lem  25959  dvidlem  25964  dvcnp2  25969  dvcnp2OLD  25970  dvcn  25971  cpnres  25987  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcobr  25997  dvcobrOLD  25998  dvcjbr  26001  dvrec  26007  dvcnvlem  26028  dvferm  26040  dvlip2  26048  dveq0  26053  dv11cn  26054  dvivthlem1  26061  lhop1  26067  lhop2  26068  lhop  26069  dvcnvre  26072  dvfsumlem3  26083  dvfsumlem4  26084  dvfsumrlim  26086  dvfsum2  26089  ftc1a  26092  ftc1lem4  26094  ftc1lem6  26096  ftc1  26097  coe1mul3  26152  deg1addle2  26155  deg1sublt  26163  fta1blem  26224  drnguc1p  26227  ig1prsp  26234  plyco0  26245  plyeq0lem  26263  dgrub  26287  dgreq  26297  dgradd2  26322  dgrmul  26324  dgrcolem2  26328  dgrco  26329  plycpn  26345  plydivlem4  26352  plydiveu  26354  vieta1lem2  26367  vieta1  26368  aalioulem2  26389  aalioulem3  26390  aaliou3lem7  26405  tayl0  26417  ulmcn  26456  ulmdvlem3  26459  psercn  26484  abelth  26499  pilem3  26511  efif1olem1  26598  abslogimle  26629  argregt0  26666  argrege0  26667  logf1o2  26706  cxpsqrtlem  26758  cxpcn3  26805  abscxpbnd  26810  logreclem  26819  ang180lem2  26867  ang180lem3  26868  xrlimcnp  27025  harmonicbnd4  27068  fsumharmonic  27069  lgamgulmlem5  27090  lgambdd  27094  basellem4  27141  dvdsppwf1o  27243  dvdsflf1o  27244  fsumfldivdiaglem  27246  chpeq0  27266  chteq0  27267  chtub  27270  chpub  27278  dchrelbasd  27297  dchrmulcl  27307  dchrinv  27319  bposlem1  27342  bposlem2  27343  lgsdirprm  27389  lgsqrlem2  27405  lgsqrlem3  27406  lgsdchr  27413  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgsquadlem1  27438  2sqlem8  27484  2sqblem  27489  2sqmod  27494  chebbnd1lem1  27527  dchrisumlem1  27547  dchrisumlem2  27548  dchrisumlem3  27549  dchrisum0fno1  27569  pntrmax  27622  pntpbnd1a  27643  pntibndlem3  27650  pntlemn  27658  pntlemi  27662  pntlem3  27667  pntleml  27669  ostth1  27691  ostth2  27695  ostth3  27696  nosepon  27724  nolesgn2ores  27731  nogesgn1ores  27733  nosupres  27766  nosupbnd1lem2  27768  nosupbnd2lem1  27774  noinfres  27781  noinfbnd1lem2  27783  noinfbnd2lem1  27789  cofcutrtime  27975  divmuldivsd  28270  divdivs1d  28271  nnsgt0  28356  ercgrg  28539  motco  28562  cnvmot  28563  legso  28621  mirmot  28697  colopp  28791  hphl  28793  lmicom  28810  lmimid  28816  lmimot  28820  hypcgrlem1  28821  hypcgrlem2  28822  trgcopyeulem  28827  inagswap  28863  inaghl  28867  cgrg3col4  28875  brbtwn2  28934  axlowdimlem3  28973  axlowdimlem16  28986  axcontlem8  29000  fusgrfis  29361  nbgr2vtx1edg  29381  0vtxrgr  29608  0vtxrusgr  29609  ewlkle  29637  wlk1ewlk  29672  uspgr2wlkeq2  29679  wlkp1lem8  29712  trlontrl  29743  pthonpth  29780  pthdlem2  29800  wlklnwwlkln1  29897  wlknewwlksn  29916  wwlksnred  29921  wwlksnredwwlkn0  29925  2trlond  29968  2pthond  29971  elwwlks2ons3im  29983  clwlkclwwlklem2a1  30020  clwlkclwwlkf1  30038  clwwlkel  30074  clwwlkwwlksb  30082  wwlksext2clwwlk  30085  1ewlk  30143  0trlon  30152  0pthon  30155  1pthond  30172  3trlond  30201  3pthond  30203  3spthond  30205  eupthres  30243  2clwwlk2clwwlk  30378  numclwwlk1lem2foa  30382  numclwwlk1lem2f1  30385  nvabs  30700  vacn  30722  nmcvcn  30723  nmblore  30814  0lno  30818  0blo  30820  nmlno0lem  30821  occl  31332  pjhthlem1  31419  pjpjpre  31447  nmopre  31898  nmlnop0iALT  32023  nmophmi  32059  leoprf2  32155  stlesi  32269  disjdifprg  32594  disjun0  32614  fsuppcurry1  32742  fsuppcurry2  32743  fpwrelmap  32750  fzspl  32797  dfmgc2lem  32969  pwrssmgc  32974  xrge0tsmsd  33047  ogrpaddlt  33076  ogrpsublt  33080  psgnfzto1stlem  33102  fzto1st1  33104  evpmid  33150  pnfinf  33172  rmfsupp2  33227  fracfld  33289  ornglmullt  33316  orngrmullt  33317  orngmullt  33318  ofldlt1  33322  isarchiofld  33326  dvdsruassoi  33391  nsgmgc  33419  drngidl  33440  qsdrngi  33502  deg1addlt  33599  ply1degltdimlem  33649  lbsdiflsp0  33653  fedgmul  33658  fldexttr  33685  fldextid  33686  irngnzply1lem  33704  irredminply  33721  algextdeglem8  33729  rtelextdg2lem  33731  constrsslem  33745  qtopt1  33795  reff  33799  locfinreflem  33800  metideq  33853  metider  33854  pstmxmet  33857  qqhval2lem  33943  qqhcn  33953  qqhucn  33954  pwsiga  34110  prsiga  34111  measle0  34188  mbfmcst  34240  1stmbfm  34241  2ndmbfm  34242  imambfm  34243  cnmbfm  34244  mbfmco  34245  mbfmco2  34246  0elcarsg  34288  carsgclctun  34302  sibfof  34321  oddpwdc  34335  eulerpartlemmf  34356  eulerpartlemgs2  34361  0rrv  34432  ballotlemfc0  34473  ballotlemfcc  34474  signstfveq0  34570  breprexplemc  34625  bnj1452  35044  usgrgt2cycl  35114  acycgr1v  35133  derangen  35156  subfacval3  35173  cvmseu  35260  cvmliftmolem2  35266  cvmliftlem7  35275  cvmliftlem15  35282  cvmlift2lem9a  35287  cvmlift2lem9  35295  cvmlift2lem10  35296  cvmlift2lem11  35297  cvmlift2lem12  35298  cvmlift3lem6  35308  cvmlift3lem8  35310  ex-sategoelel  35405  ex-sategoelelomsuc  35410  mclsppslem  35567  mclspps  35568  wsuclem  35806  fness  36331  fnetr  36333  fnessref  36339  refssfne  36340  neibastop1  36341  neibastop2  36343  tailfb  36359  filnetlem3  36362  weiunfrlem  36446  bj-finsumval0  37267  bj-rvecvec  37281  dfgcd3  37306  lindsadd  37599  poimirlem13  37619  poimirlem15  37621  poimirlem24  37630  poimirlem28  37634  mblfinlem2  37644  ovoliunnfl  37648  volsupnfl  37651  mbfresfi  37652  iblabsnc  37670  iblmulc2nc  37671  ftc1cnnclem  37677  ftc1cnnc  37678  ftc1anc  37687  sdclem2  37728  metf1o  37741  ismtyhmeolem  37790  ismtyres  37794  heibor1lem  37795  bfplem2  37809  bfp  37810  rrncmslem  37818  iccbnd  37826  icccmpALT  37827  rngogrphom  37957  rngoisoco  37968  keridl  38018  lsmcv2  39010  lsatcv0  39012  lcvexchlem4  39018  lcvexchlem5  39019  l1cvpat  39035  lfl0f  39050  lfladdcl  39052  lflnegcl  39056  lkrlss  39076  eqlkr  39080  lkrlsp  39083  lkrlsp2  39084  lshpkrcl  39097  lkrin  39145  1cvrjat  39457  llni  39490  llnle  39500  lplni  39514  lplnle  39522  llncvrlpln2  39539  2atmat  39543  lvoli  39557  lplncvrlvol2  39597  elpaddri  39784  paddclN  39824  pclclN  39873  pclfinN  39882  0psubclN  39925  1psubclN  39926  atpsubclN  39927  pmapsubclN  39928  osumclN  39949  pexmidN  39951  pexmidlem6N  39957  lhp2lt  39983  lautcnv  40072  idlaut  40078  lautco  40079  idldil  40096  ldilcnv  40097  ldilco  40098  ltrncnv  40128  idltrn  40132  cdleme16d  40263  cdleme50laut  40529  cdleme50ldil  40530  cdleme50ltrn  40539  ltrnco  40701  dian0  41021  dia0eldmN  41022  dia1eldmN  41023  dialss  41028  diaintclN  41040  docaclN  41106  doca2N  41108  djajN  41119  dibintclN  41149  diblss  41152  dicvaddcl  41172  dicvscacl  41173  dicn0  41174  cdlemn11a  41189  dihord2cN  41203  dihord11b  41204  dihord6apre  41238  dihmeetlem1N  41272  dihglblem5apreN  41273  dihpN  41318  dihjatcclem4  41403  dochkr1  41460  islpoldN  41466  lcfrlem31  41555  mapdpglem18  41671  mapdheq2  41711  mapdheq4  41714  mapdh6aN  41717  hdmap1l6a  41791  hdmap14lem4a  41853  lcmineqlem4  42013  frlmfzoccat  42491  drnginvmuld  42513  psrbagres  42532  evlselvlem  42572  evlselv  42573  fsuppind  42576  fsuppssind  42579  prjspvs  42596  irrapxlem4  42812  pell1234qrdich  42848  pell1qr1  42858  pell14qrgap  42862  pellqrexplicit  42864  rmspecfund  42896  fzmaxdif  42969  acongeq  42971  jm2.23  42984  jm3.1  43008  lmhmlnmsplit  43075  hbt  43118  dgrsub2  43123  proot1ex  43184  cantnfub  43310  cantnfresb  43313  cantnf2  43314  tfsconcatfv2  43329  tfsconcatrn  43331  tfsconcatb0  43333  naddcnff  43351  naddcnffo  43353  naddcnfid1  43356  naddcnfid2  43357  clublem  43599  dftrcl3  43709  mnugrud  44279  hashnzfz2  44316  dvconstbi  44329  ubelsupr  44957  restopn3  45093  wessf1ornlem  45127  lefldiveq  45242  iccintsng  45475  climsuse  45563  mullimc  45571  limcdm0  45573  limccog  45575  mullimcf  45578  constlimc  45579  idlimc  45581  limcperiod  45583  limsupre  45596  limcleqr  45599  neglimc  45602  addlimc  45603  0ellimcdiv  45604  xlimliminflimsup  45817  cncfshift  45829  cncfperiod  45834  cncfuni  45841  icccncfext  45842  cncfiooicclem1  45848  fperdvper  45874  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  mbfres2cn  45913  iblsplit  45921  stoweidlem7  45962  stoweidlem13  45968  stoweidlem26  45981  wallispilem3  46022  stirlinglem6  46034  stirlinglem10  46038  dirkercncf  46062  fourierdlem6  46068  fourierdlem11  46073  fourierdlem12  46074  fourierdlem15  46077  fourierdlem26  46088  fourierdlem42  46104  fourierdlem50  46111  fourierdlem51  46112  fourierdlem52  46113  fourierdlem54  46115  fourierdlem62  46123  fourierdlem79  46140  fourierdlem102  46163  fourierdlem114  46175  etransclem23  46212  3f1oss1  47024  zgeltp1eq  47258  setsnidel  47301  preimafvsnel  47303  iccpartres  47342  prpair  47425  fpprel2  47665  isubgrsubgr  47792  isuspgrim  47812  grimidvtxedg  47813  grimcnv  47816  stgrnbgr0  47866  uhgrimgrlim  47889  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx13starlem2  47962  isassintop  48053  rhmsubcALTV  48128  srhmsubcALTV  48168  fldhmsubcALTV  48176  rmfsupp  48217  scmfsupp  48219  mptcfsupp  48221  lcoel0  48273  lincsumcl  48276  lincscmcl  48277  lcoss  48281  lindsrng01  48313  lincreslvec3  48327  lindssnlvec  48331  zgtp1leeq  48366  lubsscl  48756  glbsscl  48757  idmon  48804  idepi  48805  thinciso  48860