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  7079  fveqressseq  7099  fmptsng  7188  fmptsnd  7189  fnprb  7228  fntpb  7229  fpr3g  8310  frrlem4  8314  1ellim  8536  isfsuppd  9406  fdmfifsupp  9415  fczfsuppd  9426  fsuppmptif  9439  fsuppco2  9443  fsuppcor  9444  dffi3  9471  suppr  9511  infpr  9543  ordtypelem7  9564  cantnf0  9715  cantnfp1lem1  9718  cantnfp1lem2  9719  cantnfp1lem3  9720  cantnflem1a  9725  cantnflem1d  9728  cantnflem1  9729  cantnf  9733  rankpwi  9863  carduni  10021  fin23lem32  10384  fpwwe2lem5  10675  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  inttsk  10814  grutsk1  10861  add20  11775  supaddc  12235  supadd  12236  supmul  12240  suprzcl  12698  uzid  12893  uzwo3  12985  rpnnen1lem5  13023  xrletrid  13197  xrre  13211  xrre3  13213  xleadd1a  13295  xlemul1a  13330  elioc2  13450  elico2  13451  elicc2  13452  elfz1eq  13575  fzadd2  13599  fznatpl1  13618  elfz1uz  13634  nn0fz0  13665  fzctr  13680  fzo1fzo0n0  13754  fzoaddel  13756  elincfzoext  13762  flid  13848  flval3  13855  fladdz  13865  fldiv  13900  modid  13936  hashf1lem1  14494  pfxccatin12d  14783  repswpfx  14823  2cshw  14851  pfx2  14986  wwlktovf1  14996  sqeqd  15205  01sqrexlem7  15287  max0add  15349  abs2difabs  15373  rddif  15379  fzomaxdiflem  15381  rexico  15392  icodiamlt  15474  limsupgre  15517  rlim3  15534  icco1  15576  rlimclim  15582  rlimuni  15586  rlimresb  15601  isercolllem2  15702  isercolllem3  15703  isercoll  15704  caucvgrlem  15709  caurcvgr  15710  iseraltlem3  15720  fsum00  15834  o1fsum  15849  bitsfzolem  16471  bitsfzo  16472  bitsmod  16473  bitscmp  16475  gcd0id  16556  gcdneg  16559  bezoutlem4  16579  nn0seqcvgd  16607  lcmneg  16640  lcmfunsnlem2lem2  16676  qredeq  16694  prmind2  16722  eulerthlem2  16819  pcpremul  16881  pcidlem  16910  pcgcd1  16915  fldivp1  16935  pcfaclem  16936  4sqlem17  16999  vdwlem1  17019  vdwlem6  17024  vdwlem12  17030  vdwlem13  17031  0ram  17058  ram0  17060  ramub1lem1  17064  invco  17815  sectmon  17826  monsect  17827  invid  17831  ssctr  17869  ssceq  17870  0ssc  17882  0subcat  17883  catsubcat  17884  issubc3  17894  fullsubc  17895  funcinv  17918  fthmon  17974  fuccocl  18012  fucidcl  18013  invfuc  18022  2initoinv  18055  2termoinv  18062  elhomai  18078  setcmon  18132  setcepi  18133  catcisolem  18155  curf2cl  18276  yonedalem4c  18322  yonedalem3  18325  yoniso  18330  lublecl  18406  isacs3lem  18587  tsrdir  18649  rabsubmgmd  18717  submgmid  18719  subsubmgm  18723  mgmhmima  18728  mgmhmeql  18729  mndpfsupp  18780  mnd1  18792  sgrp2nmndlem4  18941  sgrp2nmndlem5  18942  0subg  19169  nmznsg  19186  ghmpreima  19256  ghmeql  19257  ghmnsgpreima  19259  kerf1ghm  19265  cntzsgrpcl  19352  cntzsubm  19356  cntzsubg  19357  cntzmhm  19359  symgextfo  19440  symgfixf1  19455  symgfixfolem1  19456  odlem2  19557  finodsubmsubg  19585  gexlem2  19600  gexcl2  19607  sylow1lem5  19620  subgslw  19634  slwhash  19642  fislw  19643  sylow3lem1  19645  lsmsubg  19672  efgredlemd  19762  efgredlem  19765  efgcpbllemb  19773  frgpuplem  19790  cyggeninv  19901  iscygd  19905  iscygodd  19906  gsumzadd  19940  gsumconst  19952  gsumpt  19980  gsum2dlem2  19989  gsum2d  19990  gsum2d2lem  19991  dprdfcntz  20035  eldprdi  20038  subgdmdprd  20054  subgdprd  20055  dprdpr  20070  ablfac1c  20091  ablfac1eu  20093  ablfaclem3  20107  ring1  20307  subrngint  20560  rhmimasubrng  20566  cntzsubrng  20567  rhmeql  20603  rhmima  20604  cntzsubr  20606  rnghmsscmap2  20629  rnghmsscmap  20630  rnghmsubcsetc  20633  zrzeroorngc  20644  rhmsscmap2  20658  rhmsscmap  20659  rhmsubcsetc  20662  rhmsscrnghm  20665  rhmsubcrngc  20668  srhmsubc  20680  rhmsubc  20689  issubdrg  20781  fldhmsubc  20786  imadrhmcl  20798  isabvd  20813  abvdiv  20830  lsslsp  21013  lsslspOLD  21014  lmhmima  21046  lmhmpreima  21047  lmhmeql  21054  lsmcl  21082  lspfixed  21130  rnglidlrng  21257  rngqiprngim  21314  rng2idl1cntr  21315  qsssubdrg  21444  gzrngunit  21451  pzriprnglem8  21499  evpmodpmf1o  21614  ocvpj  21737  dsmm0cl  21760  dsmmacl  21761  dsmmsubg  21763  dsmmlss  21764  frlmsplit2  21793  uvcff  21811  lindfrn  21841  f1lindf  21842  lindsss  21844  issubassa  21887  issubassa2  21912  snifpsrbag  21940  psrbaglesupp  21942  psrbaglecl  21943  psrbagaddcl  21944  psrbagcon  21945  mplsubglem  22019  mpllsslem  22020  mplassa  22042  subrgmpl  22050  mplcoe5  22058  mplbas2  22060  mplind  22094  mpfind  22131  ismhp2  22145  mhpmulcl  22153  mhplss  22159  ply1assa  22201  coe1tmmul2  22279  coe1tmmul  22280  cply1coe0bi  22306  dmatid  22501  dmatsubcl  22504  dmatscmcl  22509  scmatid  22520  scmataddcl  22522  scmatsubcl  22523  scmatmulcl  22524  smatvscl  22530  scmatrhmcl  22534  mat0scmat  22544  mat1scmat  22545  mdet0pr  22598  chmaidscmat  22854  distop  23002  indistopon  23008  ppttop  23014  epttop  23016  mretopd  23100  toponmre  23101  neiss  23117  opnneissb  23122  ssnei2  23124  innei  23133  neiptoptop  23139  ordtcld1  23205  ordtcld2  23206  lmconst  23269  cnpnei  23272  iscncl  23277  cnss1  23284  cnss2  23285  cncnpi  23286  cncnp  23288  cnconst2  23291  cnrest  23293  cnpresti  23296  cnpdis  23301  paste  23302  lmcnp  23312  cnhaus  23362  hauscmp  23415  2ndcomap  23466  1stcelcls  23469  1stccnp  23470  llyrest  23493  nllyrest  23494  llyidm  23496  nllyidm  23497  ssref  23520  reftr  23522  refun0  23523  dissnref  23536  kgentopon  23546  kgenidm  23555  kgencn3  23566  txcld  23611  neitx  23615  tx1cn  23617  tx2cn  23618  ptcld  23621  xkoccn  23627  txcnp  23628  ptcnp  23630  txcnmpt  23632  ptcn  23635  txdis1cn  23643  ptrescn  23647  txkgen  23660  xkoco1cn  23665  xkoco2cn  23666  xkococn  23668  xkoinjcn  23695  qtoptop2  23707  qtopuni  23710  qtopid  23713  qtopkgen  23718  basqtop  23719  tgqtop  23720  qtopss  23723  qtopeu  23724  qtoprest  23725  kqopn  23742  kqcld  23743  kqreglem2  23750  reghmph  23801  ordthmeolem  23809  qtopf1  23824  opnfbas  23850  isfil2  23864  fbasweak  23873  fsubbas  23875  filconn  23891  fbasrn  23892  rnelfmlem  23960  flimss2  23980  flimss1  23981  hausflim  23989  flimclslem  23992  flimsncls  23994  cnpflfi  24007  flfcnp2  24015  fclsfnflim  24035  cnextfvval  24073  cnextfres1  24076  symgtgp  24114  opnsubg  24116  ghmcnp  24123  qustgpopn  24128  qustgplem  24129  qustgphaus  24131  tsmsfbas  24136  ustfilxp  24221  utoptop  24243  utopbas  24244  restutopopn  24247  iducn  24292  cstucnd  24293  ucncn  24294  fmucnd  24301  cfilufg  24302  trcfilu  24303  cfiluweak  24304  neipcfilu  24305  psmetres2  24324  isxmetd  24336  xmetpsmet  24358  imasf1oxmet  24385  xblss2ps  24411  xblss2  24412  xblcntrps  24420  xblcntr  24421  blcld  24518  metustfbas  24570  cfilucfil  24572  restmetu  24583  ngptgp  24649  tngngpd  24674  nrmtngnrm  24679  tngnrg  24695  nlmvscn  24708  nrginvrcn  24713  nmo0  24756  nmoeq0  24757  nmoid  24763  nghmcn  24766  0nmhm  24776  blcvx  24819  iccntr  24843  xrge0tsms  24856  xmetdcn2  24859  metdstri  24873  metdscn  24878  rescncf  24923  cncfco  24933  oprpiece1res2  24983  cnheibor  24987  cnllycmp  24988  bndth  24990  ishtpyd  25007  isphtpyd  25018  pcoval2  25049  nmhmcn  25153  ipcn  25280  lmnn  25297  cfilss  25304  iscfil3  25307  cfilfcls  25308  cmetcaulem  25322  iscmet3lem2  25326  cfilres  25330  lmcau  25347  flimcfil  25348  cncmet  25356  rlmbn  25395  minveclem3b  25462  pjthlem1  25471  pjth2  25474  ivthlem3  25488  ovolssnul  25522  ovolctb  25525  ovoliunnul  25542  ovolsca  25550  ovolicopnf  25559  voliunlem2  25586  volsup  25591  dyadmaxlem  25632  vitalilem5  25647  mbfres  25679  mbfss  25681  mbfmulc2re  25683  mbfadd  25696  mbfmulc2  25698  mbflim  25703  i1faddlem  25728  i1fmullem  25729  mbfmul  25761  itg2mulc  25782  itg2cnlem1  25796  ibl0  25822  iblposlem  25827  itgreval  25832  iblneg  25838  iblss  25840  iblss2  25841  itgle  25845  iblconst  25853  iblabs  25864  iblabsr  25865  iblmulc2  25866  bddmulibl  25874  limciun  25929  limcun  25930  dvres2lem  25945  dvidlem  25950  dvcnp2  25955  dvcnp2OLD  25956  dvcn  25957  cpnres  25973  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcobr  25983  dvcobrOLD  25984  dvcjbr  25987  dvrec  25993  dvcnvlem  26014  dvferm  26026  dvlip2  26034  dveq0  26039  dv11cn  26040  dvivthlem1  26047  lhop1  26053  lhop2  26054  lhop  26055  dvcnvre  26058  dvfsumlem3  26069  dvfsumlem4  26070  dvfsumrlim  26072  dvfsum2  26075  ftc1a  26078  ftc1lem4  26080  ftc1lem6  26082  ftc1  26083  coe1mul3  26138  deg1addle2  26141  deg1sublt  26149  fta1blem  26210  drnguc1p  26213  ig1prsp  26220  plyco0  26231  plyeq0lem  26249  dgrub  26273  dgreq  26283  dgradd2  26308  dgrmul  26310  dgrcolem2  26314  dgrco  26315  plycpn  26331  plydivlem4  26338  plydiveu  26340  vieta1lem2  26353  vieta1  26354  aalioulem2  26375  aalioulem3  26376  aaliou3lem7  26391  tayl0  26403  ulmcn  26442  ulmdvlem3  26445  psercn  26470  abelth  26485  pilem3  26497  efif1olem1  26584  abslogimle  26615  argregt0  26652  argrege0  26653  logf1o2  26692  cxpsqrtlem  26744  cxpcn3  26791  abscxpbnd  26796  logreclem  26805  ang180lem2  26853  ang180lem3  26854  xrlimcnp  27011  harmonicbnd4  27054  fsumharmonic  27055  lgamgulmlem5  27076  lgambdd  27080  basellem4  27127  dvdsppwf1o  27229  dvdsflf1o  27230  fsumfldivdiaglem  27232  chpeq0  27252  chteq0  27253  chtub  27256  chpub  27264  dchrelbasd  27283  dchrmulcl  27293  dchrinv  27305  bposlem1  27328  bposlem2  27329  lgsdirprm  27375  lgsqrlem2  27391  lgsqrlem3  27392  lgsdchr  27399  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgsquadlem1  27424  2sqlem8  27470  2sqblem  27475  2sqmod  27480  chebbnd1lem1  27513  dchrisumlem1  27533  dchrisumlem2  27534  dchrisumlem3  27535  dchrisum0fno1  27555  pntrmax  27608  pntpbnd1a  27629  pntibndlem3  27636  pntlemn  27644  pntlemi  27648  pntlem3  27653  pntleml  27655  ostth1  27677  ostth2  27681  ostth3  27682  nosepon  27710  nolesgn2ores  27717  nogesgn1ores  27719  nosupres  27752  nosupbnd1lem2  27754  nosupbnd2lem1  27760  noinfres  27767  noinfbnd1lem2  27769  noinfbnd2lem1  27775  cofcutrtime  27961  divmuldivsd  28256  divdivs1d  28257  nnsgt0  28342  ercgrg  28525  motco  28548  cnvmot  28549  legso  28607  mirmot  28683  colopp  28777  hphl  28779  lmicom  28796  lmimid  28802  lmimot  28806  hypcgrlem1  28807  hypcgrlem2  28808  trgcopyeulem  28813  inagswap  28849  inaghl  28853  cgrg3col4  28861  brbtwn2  28920  axlowdimlem3  28959  axlowdimlem16  28972  axcontlem8  28986  fusgrfis  29347  nbgr2vtx1edg  29367  0vtxrgr  29594  0vtxrusgr  29595  ewlkle  29623  wlk1ewlk  29658  uspgr2wlkeq2  29665  wlkp1lem8  29698  trlontrl  29729  pthonpth  29768  pthdlem2  29788  wlklnwwlkln1  29888  wlknewwlksn  29907  wwlksnred  29912  wwlksnredwwlkn0  29916  2trlond  29959  2pthond  29962  elwwlks2ons3im  29974  clwlkclwwlklem2a1  30011  clwlkclwwlkf1  30029  clwwlkel  30065  clwwlkwwlksb  30073  wwlksext2clwwlk  30076  1ewlk  30134  0trlon  30143  0pthon  30146  1pthond  30163  3trlond  30192  3pthond  30194  3spthond  30196  eupthres  30234  2clwwlk2clwwlk  30369  numclwwlk1lem2foa  30373  numclwwlk1lem2f1  30376  nvabs  30691  vacn  30713  nmcvcn  30714  nmblore  30805  0lno  30809  0blo  30811  nmlno0lem  30812  occl  31323  pjhthlem1  31410  pjpjpre  31438  nmopre  31889  nmlnop0iALT  32014  nmophmi  32050  leoprf2  32146  stlesi  32260  disjdifprg  32588  disjun0  32608  fsuppcurry1  32736  fsuppcurry2  32737  fpwrelmap  32744  fzspl  32791  dfmgc2lem  32985  pwrssmgc  32990  xrge0tsmsd  33065  ogrpaddlt  33094  ogrpsublt  33098  psgnfzto1stlem  33120  fzto1st1  33122  evpmid  33168  pnfinf  33190  rmfsupp2  33242  fracfld  33310  ornglmullt  33337  orngrmullt  33338  orngmullt  33339  ofldlt1  33343  isarchiofld  33347  dvdsruassoi  33412  nsgmgc  33440  drngidl  33461  qsdrngi  33523  deg1addlt  33620  ply1degltdimlem  33673  lbsdiflsp0  33677  fedgmul  33682  fldexttr  33709  fldextid  33710  irngnzply1lem  33740  irredminply  33757  algextdeglem8  33765  rtelextdg2lem  33767  constrsslem  33782  qtopt1  33834  reff  33838  locfinreflem  33839  metideq  33892  metider  33893  pstmxmet  33896  qqhval2lem  33982  qqhcn  33992  qqhucn  33993  pwsiga  34131  prsiga  34132  measle0  34209  mbfmcst  34261  1stmbfm  34262  2ndmbfm  34263  imambfm  34264  cnmbfm  34265  mbfmco  34266  mbfmco2  34267  0elcarsg  34309  carsgclctun  34323  sibfof  34342  oddpwdc  34356  eulerpartlemmf  34377  eulerpartlemgs2  34382  0rrv  34453  ballotlemfc0  34495  ballotlemfcc  34496  signstfveq0  34592  breprexplemc  34647  bnj1452  35066  usgrgt2cycl  35135  acycgr1v  35154  derangen  35177  subfacval3  35194  cvmseu  35281  cvmliftmolem2  35287  cvmliftlem7  35296  cvmliftlem15  35303  cvmlift2lem9a  35308  cvmlift2lem9  35316  cvmlift2lem10  35317  cvmlift2lem11  35318  cvmlift2lem12  35319  cvmlift3lem6  35329  cvmlift3lem8  35331  ex-sategoelel  35426  ex-sategoelelomsuc  35431  mclsppslem  35588  mclspps  35589  wsuclem  35826  fness  36350  fnetr  36352  fnessref  36358  refssfne  36359  neibastop1  36360  neibastop2  36362  tailfb  36378  filnetlem3  36381  weiunfrlem  36465  bj-finsumval0  37286  bj-rvecvec  37300  dfgcd3  37325  lindsadd  37620  poimirlem13  37640  poimirlem15  37642  poimirlem24  37651  poimirlem28  37655  mblfinlem2  37665  ovoliunnfl  37669  volsupnfl  37672  mbfresfi  37673  iblabsnc  37691  iblmulc2nc  37692  ftc1cnnclem  37698  ftc1cnnc  37699  ftc1anc  37708  sdclem2  37749  metf1o  37762  ismtyhmeolem  37811  ismtyres  37815  heibor1lem  37816  bfplem2  37830  bfp  37831  rrncmslem  37839  iccbnd  37847  icccmpALT  37848  rngogrphom  37978  rngoisoco  37989  keridl  38039  lsmcv2  39030  lsatcv0  39032  lcvexchlem4  39038  lcvexchlem5  39039  l1cvpat  39055  lfl0f  39070  lfladdcl  39072  lflnegcl  39076  lkrlss  39096  eqlkr  39100  lkrlsp  39103  lkrlsp2  39104  lshpkrcl  39117  lkrin  39165  1cvrjat  39477  llni  39510  llnle  39520  lplni  39534  lplnle  39542  llncvrlpln2  39559  2atmat  39563  lvoli  39577  lplncvrlvol2  39617  elpaddri  39804  paddclN  39844  pclclN  39893  pclfinN  39902  0psubclN  39945  1psubclN  39946  atpsubclN  39947  pmapsubclN  39948  osumclN  39969  pexmidN  39971  pexmidlem6N  39977  lhp2lt  40003  lautcnv  40092  idlaut  40098  lautco  40099  idldil  40116  ldilcnv  40117  ldilco  40118  ltrncnv  40148  idltrn  40152  cdleme16d  40283  cdleme50laut  40549  cdleme50ldil  40550  cdleme50ltrn  40559  ltrnco  40721  dian0  41041  dia0eldmN  41042  dia1eldmN  41043  dialss  41048  diaintclN  41060  docaclN  41126  doca2N  41128  djajN  41139  dibintclN  41169  diblss  41172  dicvaddcl  41192  dicvscacl  41193  dicn0  41194  cdlemn11a  41209  dihord2cN  41223  dihord11b  41224  dihord6apre  41258  dihmeetlem1N  41292  dihglblem5apreN  41293  dihpN  41338  dihjatcclem4  41423  dochkr1  41480  islpoldN  41486  lcfrlem31  41575  mapdpglem18  41691  mapdheq2  41731  mapdheq4  41734  mapdh6aN  41737  hdmap1l6a  41811  hdmap14lem4a  41873  lcmineqlem4  42033  frlmfzoccat  42515  drnginvmuld  42537  psrbagres  42556  evlselvlem  42596  evlselv  42597  fsuppind  42600  fsuppssind  42603  prjspvs  42620  irrapxlem4  42836  pell1234qrdich  42872  pell1qr1  42882  pell14qrgap  42886  pellqrexplicit  42888  rmspecfund  42920  fzmaxdif  42993  acongeq  42995  jm2.23  43008  jm3.1  43032  lmhmlnmsplit  43099  hbt  43142  dgrsub2  43147  proot1ex  43208  cantnfub  43334  cantnfresb  43337  cantnf2  43338  tfsconcatfv2  43353  tfsconcatrn  43355  tfsconcatb0  43357  naddcnff  43375  naddcnffo  43377  naddcnfid1  43380  naddcnfid2  43381  clublem  43623  dftrcl3  43733  mnugrud  44303  hashnzfz2  44340  dvconstbi  44353  ubelsupr  45025  restopn3  45156  wessf1ornlem  45190  lefldiveq  45304  iccintsng  45536  climsuse  45623  mullimc  45631  limcdm0  45633  limccog  45635  mullimcf  45638  constlimc  45639  idlimc  45641  limcperiod  45643  limsupre  45656  limcleqr  45659  neglimc  45662  addlimc  45663  0ellimcdiv  45664  xlimliminflimsup  45877  cncfshift  45889  cncfperiod  45894  cncfuni  45901  icccncfext  45902  cncfiooicclem1  45908  fperdvper  45934  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  mbfres2cn  45973  iblsplit  45981  stoweidlem7  46022  stoweidlem13  46028  stoweidlem26  46041  wallispilem3  46082  stirlinglem6  46094  stirlinglem10  46098  dirkercncf  46122  fourierdlem6  46128  fourierdlem11  46133  fourierdlem12  46134  fourierdlem15  46137  fourierdlem26  46148  fourierdlem42  46164  fourierdlem50  46171  fourierdlem51  46172  fourierdlem52  46173  fourierdlem54  46175  fourierdlem62  46183  fourierdlem79  46200  fourierdlem102  46223  fourierdlem114  46235  etransclem23  46272  3f1oss1  47087  zgeltp1eq  47321  setsnidel  47364  preimafvsnel  47366  iccpartres  47405  prpair  47488  fpprel2  47728  isubgrsubgr  47855  isuspgrim  47875  grimidvtxedg  47876  grimcnv  47879  stgrnbgr0  47931  uhgrimgrlim  47954  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem2  48028  isassintop  48126  rhmsubcALTV  48201  srhmsubcALTV  48241  fldhmsubcALTV  48249  rmfsupp  48289  scmfsupp  48291  mptcfsupp  48293  lcoel0  48345  lincsumcl  48348  lincscmcl  48349  lcoss  48353  lindsrng01  48385  lincreslvec3  48399  lindssnlvec  48403  zgtp1leeq  48438  lubsscl  48857  glbsscl  48858  idmon  48908  idepi  48909  isnatd  48949  swapfiso  48991  thinciso  49117