Theorem mpbir2and 712

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  7092  fveqressseq  7113  fmptsng  7202  fmptsnd  7203  fnprb  7245  fntpb  7246  fpr3g  8326  frrlem4  8330  1ellim  8554  isfsuppd  9436  fdmfifsupp  9444  fczfsuppd  9455  fsuppmptif  9468  fsuppco2  9472  fsuppcor  9473  dffi3  9500  suppr  9540  infpr  9572  ordtypelem7  9593  cantnf0  9744  cantnfp1lem1  9747  cantnfp1lem2  9748  cantnfp1lem3  9749  cantnflem1a  9754  cantnflem1d  9757  cantnflem1  9758  cantnf  9762  rankpwi  9892  carduni  10050  fin23lem32  10413  fpwwe2lem5  10704  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  inttsk  10843  grutsk1  10890  add20  11802  supaddc  12262  supadd  12263  supmul  12267  suprzcl  12723  uzid  12918  uzwo3  13008  rpnnen1lem5  13046  xrletrid  13217  xrre  13231  xrre3  13233  xleadd1a  13315  xlemul1a  13350  elioc2  13470  elico2  13471  elicc2  13472  elfz1eq  13595  fzadd2  13619  fznatpl1  13638  elfz1uz  13654  nn0fz0  13682  fzctr  13697  fzo1fzo0n0  13767  fzoaddel  13769  elincfzoext  13774  flid  13859  flval3  13866  fladdz  13876  fldiv  13911  modid  13947  hashf1lem1  14504  pfxccatin12d  14793  repswpfx  14833  2cshw  14861  pfx2  14996  wwlktovf1  15006  sqeqd  15215  01sqrexlem7  15297  max0add  15359  abs2difabs  15383  rddif  15389  fzomaxdiflem  15391  rexico  15402  icodiamlt  15484  limsupgre  15527  rlim3  15544  icco1  15586  rlimclim  15592  rlimuni  15596  rlimresb  15611  isercolllem2  15714  isercolllem3  15715  isercoll  15716  caucvgrlem  15721  caurcvgr  15722  iseraltlem3  15732  fsum00  15846  o1fsum  15861  bitsfzolem  16480  bitsfzo  16481  bitsmod  16482  bitscmp  16484  gcd0id  16565  gcdneg  16568  bezoutlem4  16589  nn0seqcvgd  16617  lcmneg  16650  lcmfunsnlem2lem2  16686  qredeq  16704  prmind2  16732  eulerthlem2  16829  pcpremul  16890  pcidlem  16919  pcgcd1  16924  fldivp1  16944  pcfaclem  16945  4sqlem17  17008  vdwlem1  17028  vdwlem6  17033  vdwlem12  17039  vdwlem13  17040  0ram  17067  ram0  17069  ramub1lem1  17073  invco  17832  sectmon  17843  monsect  17844  invid  17848  ssctr  17886  ssceq  17887  0ssc  17901  0subcat  17902  catsubcat  17903  issubc3  17913  fullsubc  17914  funcinv  17937  fthmon  17994  fuccocl  18034  fucidcl  18035  invfuc  18044  2initoinv  18077  2termoinv  18084  elhomai  18100  setcmon  18154  setcepi  18155  catcisolem  18177  curf2cl  18301  yonedalem4c  18347  yonedalem3  18350  yoniso  18355  lublecl  18431  isacs3lem  18612  tsrdir  18674  rabsubmgmd  18742  submgmid  18744  subsubmgm  18748  mgmhmima  18753  mgmhmeql  18754  mnd1  18814  sgrp2nmndlem4  18963  sgrp2nmndlem5  18964  0subg  19191  nmznsg  19208  ghmpreima  19278  ghmeql  19279  ghmnsgpreima  19281  kerf1ghm  19287  cntzsgrpcl  19374  cntzsubm  19378  cntzsubg  19379  cntzmhm  19381  symgextfo  19464  symgfixf1  19479  symgfixfolem1  19480  odlem2  19581  finodsubmsubg  19609  gexlem2  19624  gexcl2  19631  sylow1lem5  19644  subgslw  19658  slwhash  19666  fislw  19667  sylow3lem1  19669  lsmsubg  19696  efgredlemd  19786  efgredlem  19789  efgcpbllemb  19797  frgpuplem  19814  cyggeninv  19925  iscygd  19929  iscygodd  19930  gsumzadd  19964  gsumconst  19976  gsumpt  20004  gsum2dlem2  20013  gsum2d  20014  gsum2d2lem  20015  dprdfcntz  20059  eldprdi  20062  subgdmdprd  20078  subgdprd  20079  dprdpr  20094  ablfac1c  20115  ablfac1eu  20117  ablfaclem3  20131  ring1  20333  subrngint  20586  rhmimasubrng  20592  cntzsubrng  20593  rhmeql  20631  rhmima  20632  cntzsubr  20634  rnghmsscmap2  20651  rnghmsscmap  20652  rnghmsubcsetc  20655  zrzeroorngc  20666  rhmsscmap2  20680  rhmsscmap  20681  rhmsubcsetc  20684  rhmsscrnghm  20687  rhmsubcrngc  20690  srhmsubc  20702  rhmsubc  20711  issubdrg  20803  fldhmsubc  20808  imadrhmcl  20820  isabvd  20835  abvdiv  20852  lsslsp  21036  lsslspOLD  21037  lmhmima  21069  lmhmpreima  21070  lmhmeql  21077  lsmcl  21105  lspfixed  21153  rnglidlrng  21280  rngqiprngim  21337  rng2idl1cntr  21338  qsssubdrg  21467  gzrngunit  21474  pzriprnglem8  21522  evpmodpmf1o  21637  ocvpj  21760  dsmm0cl  21783  dsmmacl  21784  dsmmsubg  21786  dsmmlss  21787  frlmsplit2  21816  uvcff  21834  lindfrn  21864  f1lindf  21865  lindsss  21867  issubassa  21910  issubassa2  21935  snifpsrbag  21963  psrbaglesupp  21965  psrbaglecl  21966  psrbagaddcl  21967  psrbagcon  21968  mplsubglem  22042  mpllsslem  22043  mplassa  22065  subrgmpl  22073  mplcoe5  22081  mplbas2  22083  mplind  22117  mpfind  22154  ismhp2  22168  mhpmulcl  22176  mhplss  22182  ply1assa  22222  coe1tmmul2  22300  coe1tmmul  22301  cply1coe0bi  22327  dmatid  22522  dmatsubcl  22525  dmatscmcl  22530  scmatid  22541  scmataddcl  22543  scmatsubcl  22544  scmatmulcl  22545  smatvscl  22551  scmatrhmcl  22555  mat0scmat  22565  mat1scmat  22566  mdet0pr  22619  chmaidscmat  22875  distop  23023  indistopon  23029  ppttop  23035  epttop  23037  mretopd  23121  toponmre  23122  neiss  23138  opnneissb  23143  ssnei2  23145  innei  23154  neiptoptop  23160  ordtcld1  23226  ordtcld2  23227  lmconst  23290  cnpnei  23293  iscncl  23298  cnss1  23305  cnss2  23306  cncnpi  23307  cncnp  23309  cnconst2  23312  cnrest  23314  cnpresti  23317  cnpdis  23322  paste  23323  lmcnp  23333  cnhaus  23383  hauscmp  23436  2ndcomap  23487  1stcelcls  23490  1stccnp  23491  llyrest  23514  nllyrest  23515  llyidm  23517  nllyidm  23518  ssref  23541  reftr  23543  refun0  23544  dissnref  23557  kgentopon  23567  kgenidm  23576  kgencn3  23587  txcld  23632  neitx  23636  tx1cn  23638  tx2cn  23639  ptcld  23642  xkoccn  23648  txcnp  23649  ptcnp  23651  txcnmpt  23653  ptcn  23656  txdis1cn  23664  ptrescn  23668  txkgen  23681  xkoco1cn  23686  xkoco2cn  23687  xkococn  23689  xkoinjcn  23716  qtoptop2  23728  qtopuni  23731  qtopid  23734  qtopkgen  23739  basqtop  23740  tgqtop  23741  qtopss  23744  qtopeu  23745  qtoprest  23746  kqopn  23763  kqcld  23764  kqreglem2  23771  reghmph  23822  ordthmeolem  23830  qtopf1  23845  opnfbas  23871  isfil2  23885  fbasweak  23894  fsubbas  23896  filconn  23912  fbasrn  23913  rnelfmlem  23981  flimss2  24001  flimss1  24002  hausflim  24010  flimclslem  24013  flimsncls  24015  cnpflfi  24028  flfcnp2  24036  fclsfnflim  24056  cnextfvval  24094  cnextfres1  24097  symgtgp  24135  opnsubg  24137  ghmcnp  24144  qustgpopn  24149  qustgplem  24150  qustgphaus  24152  tsmsfbas  24157  ustfilxp  24242  utoptop  24264  utopbas  24265  restutopopn  24268  iducn  24313  cstucnd  24314  ucncn  24315  fmucnd  24322  cfilufg  24323  trcfilu  24324  cfiluweak  24325  neipcfilu  24326  psmetres2  24345  isxmetd  24357  xmetpsmet  24379  imasf1oxmet  24406  xblss2ps  24432  xblss2  24433  xblcntrps  24441  xblcntr  24442  blcld  24539  metustfbas  24591  cfilucfil  24593  restmetu  24604  ngptgp  24670  tngngpd  24695  nrmtngnrm  24700  tngnrg  24716  nlmvscn  24729  nrginvrcn  24734  nmo0  24777  nmoeq0  24778  nmoid  24784  nghmcn  24787  0nmhm  24797  blcvx  24839  iccntr  24862  xrge0tsms  24875  xmetdcn2  24878  metdstri  24892  metdscn  24897  rescncf  24942  cncfco  24952  oprpiece1res2  25002  cnheibor  25006  cnllycmp  25007  bndth  25009  ishtpyd  25026  isphtpyd  25037  pcoval2  25068  nmhmcn  25172  ipcn  25299  lmnn  25316  cfilss  25323  iscfil3  25326  cfilfcls  25327  cmetcaulem  25341  iscmet3lem2  25345  cfilres  25349  lmcau  25366  flimcfil  25367  cncmet  25375  rlmbn  25414  minveclem3b  25481  pjthlem1  25490  pjth2  25493  ivthlem3  25507  ovolssnul  25541  ovolctb  25544  ovoliunnul  25561  ovolsca  25569  ovolicopnf  25578  voliunlem2  25605  volsup  25610  dyadmaxlem  25651  vitalilem5  25666  mbfres  25698  mbfss  25700  mbfmulc2re  25702  mbfadd  25715  mbfmulc2  25717  mbflim  25722  i1faddlem  25747  i1fmullem  25748  mbfmul  25781  itg2mulc  25802  itg2cnlem1  25816  ibl0  25842  iblposlem  25847  itgreval  25852  iblneg  25858  iblss  25860  iblss2  25861  itgle  25865  iblconst  25873  iblabs  25884  iblabsr  25885  iblmulc2  25886  bddmulibl  25894  limciun  25949  limcun  25950  dvres2lem  25965  dvidlem  25970  dvcnp2  25975  dvcnp2OLD  25976  dvcn  25977  cpnres  25993  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcobr  26003  dvcobrOLD  26004  dvcjbr  26007  dvrec  26013  dvcnvlem  26034  dvferm  26046  dvlip2  26054  dveq0  26059  dv11cn  26060  dvivthlem1  26067  lhop1  26073  lhop2  26074  lhop  26075  dvcnvre  26078  dvfsumlem3  26089  dvfsumlem4  26090  dvfsumrlim  26092  dvfsum2  26095  ftc1a  26098  ftc1lem4  26100  ftc1lem6  26102  ftc1  26103  coe1mul3  26158  deg1addle2  26161  deg1sublt  26169  fta1blem  26230  drnguc1p  26233  ig1prsp  26240  plyco0  26251  plyeq0lem  26269  dgrub  26293  dgreq  26303  dgradd2  26328  dgrmul  26330  dgrcolem2  26334  dgrco  26335  plycpn  26349  plydivlem4  26356  plydiveu  26358  vieta1lem2  26371  vieta1  26372  aalioulem2  26393  aalioulem3  26394  aaliou3lem7  26409  tayl0  26421  ulmcn  26460  ulmdvlem3  26463  psercn  26488  abelth  26503  pilem3  26515  efif1olem1  26602  abslogimle  26633  argregt0  26670  argrege0  26671  logf1o2  26710  cxpsqrtlem  26762  cxpcn3  26809  abscxpbnd  26814  logreclem  26823  ang180lem2  26871  ang180lem3  26872  xrlimcnp  27029  harmonicbnd4  27072  fsumharmonic  27073  lgamgulmlem5  27094  lgambdd  27098  basellem4  27145  dvdsppwf1o  27247  dvdsflf1o  27248  fsumfldivdiaglem  27250  chpeq0  27270  chteq0  27271  chtub  27274  chpub  27282  dchrelbasd  27301  dchrmulcl  27311  dchrinv  27323  bposlem1  27346  bposlem2  27347  lgsdirprm  27393  lgsqrlem2  27409  lgsqrlem3  27410  lgsdchr  27417  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgsquadlem1  27442  2sqlem8  27488  2sqblem  27493  2sqmod  27498  chebbnd1lem1  27531  dchrisumlem1  27551  dchrisumlem2  27552  dchrisumlem3  27553  dchrisum0fno1  27573  pntrmax  27626  pntpbnd1a  27647  pntibndlem3  27654  pntlemn  27662  pntlemi  27666  pntlem3  27671  pntleml  27673  ostth1  27695  ostth2  27699  ostth3  27700  nosepon  27728  nolesgn2ores  27735  nogesgn1ores  27737  nosupres  27770  nosupbnd1lem2  27772  nosupbnd2lem1  27778  noinfres  27785  noinfbnd1lem2  27787  noinfbnd2lem1  27793  cofcutrtime  27979  divmuldivsd  28274  divdivs1d  28275  nnsgt0  28360  ercgrg  28543  motco  28566  cnvmot  28567  legso  28625  mirmot  28701  colopp  28795  hphl  28797  lmicom  28814  lmimid  28820  lmimot  28824  hypcgrlem1  28825  hypcgrlem2  28826  trgcopyeulem  28831  inagswap  28867  inaghl  28871  cgrg3col4  28879  brbtwn2  28938  axlowdimlem3  28977  axlowdimlem16  28990  axcontlem8  29004  fusgrfis  29365  nbgr2vtx1edg  29385  0vtxrgr  29612  0vtxrusgr  29613  ewlkle  29641  wlk1ewlk  29676  uspgr2wlkeq2  29683  wlkp1lem8  29716  trlontrl  29747  pthonpth  29784  pthdlem2  29804  wlklnwwlkln1  29901  wlknewwlksn  29920  wwlksnred  29925  wwlksnredwwlkn0  29929  2trlond  29972  2pthond  29975  elwwlks2ons3im  29987  clwlkclwwlklem2a1  30024  clwlkclwwlkf1  30042  clwwlkel  30078  clwwlkwwlksb  30086  wwlksext2clwwlk  30089  1ewlk  30147  0trlon  30156  0pthon  30159  1pthond  30176  3trlond  30205  3pthond  30207  3spthond  30209  eupthres  30247  2clwwlk2clwwlk  30382  numclwwlk1lem2foa  30386  numclwwlk1lem2f1  30389  nvabs  30704  vacn  30726  nmcvcn  30727  nmblore  30818  0lno  30822  0blo  30824  nmlno0lem  30825  occl  31336  pjhthlem1  31423  pjpjpre  31451  nmopre  31902  nmlnop0iALT  32027  nmophmi  32063  leoprf2  32159  stlesi  32273  disjdifprg  32597  disjun0  32617  fsuppcurry1  32739  fsuppcurry2  32740  fpwrelmap  32747  fzspl  32795  dfmgc2lem  32968  pwrssmgc  32973  xrge0tsmsd  33041  ogrpaddlt  33067  ogrpsublt  33071  psgnfzto1stlem  33093  fzto1st1  33095  evpmid  33141  pnfinf  33163  rmfsupp2  33218  fracfld  33275  ornglmullt  33302  orngrmullt  33303  orngmullt  33304  ofldlt1  33308  isarchiofld  33312  dvdsruassoi  33377  nsgmgc  33405  drngidl  33426  qsdrngi  33488  deg1addlt  33585  ply1degltdimlem  33635  lbsdiflsp0  33639  fedgmul  33644  fldexttr  33671  fldextid  33672  irngnzply1lem  33690  irredminply  33707  algextdeglem8  33715  rtelextdg2lem  33717  constrsslem  33731  qtopt1  33781  reff  33785  locfinreflem  33786  metideq  33839  metider  33840  pstmxmet  33843  qqhval2lem  33927  qqhcn  33937  qqhucn  33938  pwsiga  34094  prsiga  34095  measle0  34172  mbfmcst  34224  1stmbfm  34225  2ndmbfm  34226  imambfm  34227  cnmbfm  34228  mbfmco  34229  mbfmco2  34230  0elcarsg  34272  carsgclctun  34286  sibfof  34305  oddpwdc  34319  eulerpartlemmf  34340  eulerpartlemgs2  34345  0rrv  34416  ballotlemfc0  34457  ballotlemfcc  34458  signstfveq0  34554  breprexplemc  34609  bnj1452  35028  usgrgt2cycl  35098  acycgr1v  35117  derangen  35140  subfacval3  35157  cvmseu  35244  cvmliftmolem2  35250  cvmliftlem7  35259  cvmliftlem15  35266  cvmlift2lem9a  35271  cvmlift2lem9  35279  cvmlift2lem10  35280  cvmlift2lem11  35281  cvmlift2lem12  35282  cvmlift3lem6  35292  cvmlift3lem8  35294  ex-sategoelel  35389  ex-sategoelelomsuc  35394  mclsppslem  35551  mclspps  35552  wsuclem  35789  fness  36315  fnetr  36317  fnessref  36323  refssfne  36324  neibastop1  36325  neibastop2  36327  tailfb  36343  filnetlem3  36346  weiunfrlem  36430  bj-finsumval0  37251  bj-rvecvec  37265  dfgcd3  37290  lindsadd  37573  poimirlem13  37593  poimirlem15  37595  poimirlem24  37604  poimirlem28  37608  mblfinlem2  37618  ovoliunnfl  37622  volsupnfl  37625  mbfresfi  37626  iblabsnc  37644  iblmulc2nc  37645  ftc1cnnclem  37651  ftc1cnnc  37652  ftc1anc  37661  sdclem2  37702  metf1o  37715  ismtyhmeolem  37764  ismtyres  37768  heibor1lem  37769  bfplem2  37783  bfp  37784  rrncmslem  37792  iccbnd  37800  icccmpALT  37801  rngogrphom  37931  rngoisoco  37942  keridl  37992  lsmcv2  38985  lsatcv0  38987  lcvexchlem4  38993  lcvexchlem5  38994  l1cvpat  39010  lfl0f  39025  lfladdcl  39027  lflnegcl  39031  lkrlss  39051  eqlkr  39055  lkrlsp  39058  lkrlsp2  39059  lshpkrcl  39072  lkrin  39120  1cvrjat  39432  llni  39465  llnle  39475  lplni  39489  lplnle  39497  llncvrlpln2  39514  2atmat  39518  lvoli  39532  lplncvrlvol2  39572  elpaddri  39759  paddclN  39799  pclclN  39848  pclfinN  39857  0psubclN  39900  1psubclN  39901  atpsubclN  39902  pmapsubclN  39903  osumclN  39924  pexmidN  39926  pexmidlem6N  39932  lhp2lt  39958  lautcnv  40047  idlaut  40053  lautco  40054  idldil  40071  ldilcnv  40072  ldilco  40073  ltrncnv  40103  idltrn  40107  cdleme16d  40238  cdleme50laut  40504  cdleme50ldil  40505  cdleme50ltrn  40514  ltrnco  40676  dian0  40996  dia0eldmN  40997  dia1eldmN  40998  dialss  41003  diaintclN  41015  docaclN  41081  doca2N  41083  djajN  41094  dibintclN  41124  diblss  41127  dicvaddcl  41147  dicvscacl  41148  dicn0  41149  cdlemn11a  41164  dihord2cN  41178  dihord11b  41179  dihord6apre  41213  dihmeetlem1N  41247  dihglblem5apreN  41248  dihpN  41293  dihjatcclem4  41378  dochkr1  41435  islpoldN  41441  lcfrlem31  41530  mapdpglem18  41646  mapdheq2  41686  mapdheq4  41689  mapdh6aN  41692  hdmap1l6a  41766  hdmap14lem4a  41828  lcmineqlem4  41989  frlmfzoccat  42460  drnginvmuld  42482  psrbagres  42501  evlselvlem  42541  evlselv  42542  fsuppind  42545  fsuppssind  42548  prjspvs  42565  irrapxlem4  42781  pell1234qrdich  42817  pell1qr1  42827  pell14qrgap  42831  pellqrexplicit  42833  rmspecfund  42865  fzmaxdif  42938  acongeq  42940  jm2.23  42953  jm3.1  42977  lmhmlnmsplit  43044  hbt  43087  dgrsub2  43092  proot1ex  43157  cantnfub  43283  cantnfresb  43286  cantnf2  43287  tfsconcatfv2  43302  tfsconcatrn  43304  tfsconcatb0  43306  naddcnff  43324  naddcnffo  43326  naddcnfid1  43329  naddcnfid2  43330  clublem  43572  dftrcl3  43682  mnugrud  44253  hashnzfz2  44290  dvconstbi  44303  ubelsupr  44920  restopn3  45056  wessf1ornlem  45092  lefldiveq  45207  iccintsng  45441  climsuse  45529  mullimc  45537  limcdm0  45539  limccog  45541  mullimcf  45544  constlimc  45545  idlimc  45547  limcperiod  45549  limsupre  45562  limcleqr  45565  neglimc  45568  addlimc  45569  0ellimcdiv  45570  xlimliminflimsup  45783  cncfshift  45795  cncfperiod  45800  cncfuni  45807  icccncfext  45808  cncfiooicclem1  45814  fperdvper  45840  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  mbfres2cn  45879  iblsplit  45887  stoweidlem7  45928  stoweidlem13  45934  stoweidlem26  45947  wallispilem3  45988  stirlinglem6  46000  stirlinglem10  46004  dirkercncf  46028  fourierdlem6  46034  fourierdlem11  46039  fourierdlem12  46040  fourierdlem15  46043  fourierdlem26  46054  fourierdlem42  46070  fourierdlem50  46077  fourierdlem51  46078  fourierdlem52  46079  fourierdlem54  46081  fourierdlem62  46089  fourierdlem79  46106  fourierdlem102  46129  fourierdlem114  46141  etransclem23  46178  3f1oss1  46990  zgeltp1eq  47224  setsnidel  47251  preimafvsnel  47253  iccpartres  47292  prpair  47375  fpprel2  47615  isubgrsubgr  47739  isuspgrim  47759  grimidvtxedg  47760  grimcnv  47763  uhgrimgrlim  47811  isassintop  47933  rhmsubcALTV  48008  srhmsubcALTV  48048  fldhmsubcALTV  48056  rmfsupp  48099  mndpfsupp  48101  scmfsupp  48103  mptcfsupp  48105  lcoel0  48157  lincsumcl  48160  lincscmcl  48161  lcoss  48165  lindsrng01  48197  lincreslvec3  48211  lindssnlvec  48215  zgtp1leeq  48250  lubsscl  48640  glbsscl  48641  idmon  48683  idepi  48684  thinciso  48727