Theorem mpbir2and 711

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 510	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 256	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  elpreimad  7064  fveqressseq  7085  fmptsng  7174  fmptsnd  7175  fnprb  7217  fntpb  7218  fpr3g  8292  frrlem4  8296  1ellim  8520  isfsuppd  9403  fdmfifsupp  9411  fczfsuppd  9422  fsuppmptif  9435  fsuppco2  9439  fsuppcor  9440  dffi3  9467  suppr  9507  infpr  9539  ordtypelem7  9560  cantnf0  9711  cantnfp1lem1  9714  cantnfp1lem2  9715  cantnfp1lem3  9716  cantnflem1a  9721  cantnflem1d  9724  cantnflem1  9725  cantnf  9729  rankpwi  9859  carduni  10017  fin23lem32  10378  fpwwe2lem5  10669  fpwwe2lem11  10675  fpwwe2lem12  10676  fpwwe2  10677  inttsk  10808  grutsk1  10855  add20  11767  supaddc  12227  supadd  12228  supmul  12232  suprzcl  12688  uzid  12883  uzwo3  12973  rpnnen1lem5  13011  xrletrid  13182  xrre  13196  xrre3  13198  xleadd1a  13280  xlemul1a  13315  elioc2  13435  elico2  13436  elicc2  13437  elfz1eq  13560  fzadd2  13584  fznatpl1  13603  elfz1uz  13619  nn0fz0  13647  fzctr  13661  fzo1fzo0n0  13731  fzoaddel  13733  elincfzoext  13738  flid  13822  flval3  13829  fladdz  13839  fldiv  13874  modid  13910  hashf1lem1  14468  hashf1lem1OLD  14469  pfxccatin12d  14748  repswpfx  14788  2cshw  14816  pfx2  14951  wwlktovf1  14961  sqeqd  15166  01sqrexlem7  15248  max0add  15310  abs2difabs  15334  rddif  15340  fzomaxdiflem  15342  rexico  15353  icodiamlt  15435  limsupgre  15478  rlim3  15495  icco1  15537  rlimclim  15543  rlimuni  15547  rlimresb  15562  isercolllem2  15665  isercolllem3  15666  isercoll  15667  caucvgrlem  15672  caurcvgr  15673  iseraltlem3  15683  fsum00  15797  o1fsum  15812  bitsfzolem  16429  bitsfzo  16430  bitsmod  16431  bitscmp  16433  gcd0id  16514  gcdneg  16517  bezoutlem4  16538  nn0seqcvgd  16566  lcmneg  16599  lcmfunsnlem2lem2  16635  qredeq  16653  prmind2  16681  eulerthlem2  16779  pcpremul  16840  pcidlem  16869  pcgcd1  16874  fldivp1  16894  pcfaclem  16895  4sqlem17  16958  vdwlem1  16978  vdwlem6  16983  vdwlem12  16989  vdwlem13  16990  0ram  17017  ram0  17019  ramub1lem1  17023  invco  17782  sectmon  17793  monsect  17794  invid  17798  ssctr  17836  ssceq  17837  0ssc  17851  0subcat  17852  catsubcat  17853  issubc3  17863  fullsubc  17864  funcinv  17887  fthmon  17944  fuccocl  17984  fucidcl  17985  invfuc  17994  2initoinv  18027  2termoinv  18034  elhomai  18050  setcmon  18104  setcepi  18105  catcisolem  18127  curf2cl  18251  yonedalem4c  18297  yonedalem3  18300  yoniso  18305  lublecl  18381  isacs3lem  18562  tsrdir  18624  rabsubmgmd  18692  submgmid  18694  subsubmgm  18698  mgmhmima  18703  mgmhmeql  18704  mnd1  18764  sgrp2nmndlem4  18913  sgrp2nmndlem5  18914  0subg  19141  nmznsg  19158  ghmpreima  19228  ghmeql  19229  ghmnsgpreima  19231  kerf1ghm  19237  cntzsgrpcl  19324  cntzsubm  19328  cntzsubg  19329  cntzmhm  19331  symgextfo  19416  symgfixf1  19431  symgfixfolem1  19432  odlem2  19533  finodsubmsubg  19561  gexlem2  19576  gexcl2  19583  sylow1lem5  19596  subgslw  19610  slwhash  19618  fislw  19619  sylow3lem1  19621  lsmsubg  19648  efgredlemd  19738  efgredlem  19741  efgcpbllemb  19749  frgpuplem  19766  cyggeninv  19877  iscygd  19881  iscygodd  19882  gsumzadd  19916  gsumconst  19928  gsumpt  19956  gsum2dlem2  19965  gsum2d  19966  gsum2d2lem  19967  dprdfcntz  20011  eldprdi  20014  subgdmdprd  20030  subgdprd  20031  dprdpr  20046  ablfac1c  20067  ablfac1eu  20069  ablfaclem3  20083  ring1  20285  subrngint  20538  rhmimasubrng  20544  cntzsubrng  20545  rhmeql  20583  rhmima  20584  cntzsubr  20586  rnghmsscmap2  20603  rnghmsscmap  20604  rnghmsubcsetc  20607  zrzeroorngc  20618  rhmsscmap2  20632  rhmsscmap  20633  rhmsubcsetc  20636  rhmsscrnghm  20639  rhmsubcrngc  20642  srhmsubc  20654  rhmsubc  20663  issubdrg  20755  fldhmsubc  20760  imadrhmcl  20772  isabvd  20787  abvdiv  20804  lsslsp  20988  lsslspOLD  20989  lmhmima  21021  lmhmpreima  21022  lmhmeql  21029  lsmcl  21057  lspfixed  21105  rnglidlrng  21232  rngqiprngim  21289  rng2idl1cntr  21290  qsssubdrg  21419  gzrngunit  21426  pzriprnglem8  21474  evpmodpmf1o  21588  ocvpj  21711  dsmm0cl  21734  dsmmacl  21735  dsmmsubg  21737  dsmmlss  21738  frlmsplit2  21767  uvcff  21785  lindfrn  21815  f1lindf  21816  lindsss  21818  issubassa  21860  issubassa2  21885  snifpsrbag  21915  psrbaglesupp  21917  psrbaglesuppOLD  21918  psrbaglecl  21919  psrbagleclOLD  21920  psrbagaddcl  21921  psrbagaddclOLD  21922  psrbagcon  21923  psrbagconOLD  21924  mplsubglem  22004  mpllsslem  22005  mplassa  22027  subrgmpl  22035  mplcoe5  22043  mplbas2  22045  mplind  22079  mpfind  22118  ismhp2  22132  mhpmulcl  22139  mhplss  22145  ply1assa  22185  coe1tmmul2  22263  coe1tmmul  22264  cply1coe0bi  22290  dmatid  22485  dmatsubcl  22488  dmatscmcl  22493  scmatid  22504  scmataddcl  22506  scmatsubcl  22507  scmatmulcl  22508  smatvscl  22514  scmatrhmcl  22518  mat0scmat  22528  mat1scmat  22529  mdet0pr  22582  chmaidscmat  22838  distop  22986  indistopon  22992  ppttop  22998  epttop  23000  mretopd  23084  toponmre  23085  neiss  23101  opnneissb  23106  ssnei2  23108  innei  23117  neiptoptop  23123  ordtcld1  23189  ordtcld2  23190  lmconst  23253  cnpnei  23256  iscncl  23261  cnss1  23268  cnss2  23269  cncnpi  23270  cncnp  23272  cnconst2  23275  cnrest  23277  cnpresti  23280  cnpdis  23285  paste  23286  lmcnp  23296  cnhaus  23346  hauscmp  23399  2ndcomap  23450  1stcelcls  23453  1stccnp  23454  llyrest  23477  nllyrest  23478  llyidm  23480  nllyidm  23481  ssref  23504  reftr  23506  refun0  23507  dissnref  23520  kgentopon  23530  kgenidm  23539  kgencn3  23550  txcld  23595  neitx  23599  tx1cn  23601  tx2cn  23602  ptcld  23605  xkoccn  23611  txcnp  23612  ptcnp  23614  txcnmpt  23616  ptcn  23619  txdis1cn  23627  ptrescn  23631  txkgen  23644  xkoco1cn  23649  xkoco2cn  23650  xkococn  23652  xkoinjcn  23679  qtoptop2  23691  qtopuni  23694  qtopid  23697  qtopkgen  23702  basqtop  23703  tgqtop  23704  qtopss  23707  qtopeu  23708  qtoprest  23709  kqopn  23726  kqcld  23727  kqreglem2  23734  reghmph  23785  ordthmeolem  23793  qtopf1  23808  opnfbas  23834  isfil2  23848  fbasweak  23857  fsubbas  23859  filconn  23875  fbasrn  23876  rnelfmlem  23944  flimss2  23964  flimss1  23965  hausflim  23973  flimclslem  23976  flimsncls  23978  cnpflfi  23991  flfcnp2  23999  fclsfnflim  24019  cnextfvval  24057  cnextfres1  24060  symgtgp  24098  opnsubg  24100  ghmcnp  24107  qustgpopn  24112  qustgplem  24113  qustgphaus  24115  tsmsfbas  24120  ustfilxp  24205  utoptop  24227  utopbas  24228  restutopopn  24231  iducn  24276  cstucnd  24277  ucncn  24278  fmucnd  24285  cfilufg  24286  trcfilu  24287  cfiluweak  24288  neipcfilu  24289  psmetres2  24308  isxmetd  24320  xmetpsmet  24342  imasf1oxmet  24369  xblss2ps  24395  xblss2  24396  xblcntrps  24404  xblcntr  24405  blcld  24502  metustfbas  24554  cfilucfil  24556  restmetu  24567  ngptgp  24633  tngngpd  24658  nrmtngnrm  24663  tngnrg  24679  nlmvscn  24692  nrginvrcn  24697  nmo0  24740  nmoeq0  24741  nmoid  24747  nghmcn  24750  0nmhm  24760  blcvx  24802  iccntr  24825  xrge0tsms  24838  xmetdcn2  24841  metdstri  24855  metdscn  24860  rescncf  24905  cncfco  24915  oprpiece1res2  24965  cnheibor  24969  cnllycmp  24970  bndth  24972  ishtpyd  24989  isphtpyd  25000  pcoval2  25031  nmhmcn  25135  ipcn  25262  lmnn  25279  cfilss  25286  iscfil3  25289  cfilfcls  25290  cmetcaulem  25304  iscmet3lem2  25308  cfilres  25312  lmcau  25329  flimcfil  25330  cncmet  25338  rlmbn  25377  minveclem3b  25444  pjthlem1  25453  pjth2  25456  ivthlem3  25470  ovolssnul  25504  ovolctb  25507  ovoliunnul  25524  ovolsca  25532  ovolicopnf  25541  voliunlem2  25568  volsup  25573  dyadmaxlem  25614  vitalilem5  25629  mbfres  25661  mbfss  25663  mbfmulc2re  25665  mbfadd  25678  mbfmulc2  25680  mbflim  25685  i1faddlem  25710  i1fmullem  25711  mbfmul  25744  itg2mulc  25765  itg2cnlem1  25779  ibl0  25804  iblposlem  25809  itgreval  25814  iblneg  25820  iblss  25822  iblss2  25823  itgle  25827  iblconst  25835  iblabs  25846  iblabsr  25847  iblmulc2  25848  bddmulibl  25856  limciun  25911  limcun  25912  dvres2lem  25927  dvidlem  25932  dvcnp2  25937  dvcnp2OLD  25938  dvcn  25939  cpnres  25955  dvaddbr  25956  dvmulbr  25957  dvmulbrOLD  25958  dvcobr  25965  dvcobrOLD  25966  dvcjbr  25969  dvrec  25975  dvcnvlem  25996  dvferm  26008  dvlip2  26016  dveq0  26021  dv11cn  26022  dvivthlem1  26029  lhop1  26035  lhop2  26036  lhop  26037  dvcnvre  26040  dvfsumlem3  26051  dvfsumlem4  26052  dvfsumrlim  26054  dvfsum2  26057  ftc1a  26060  ftc1lem4  26062  ftc1lem6  26064  ftc1  26065  coe1mul3  26123  deg1addle2  26126  deg1sublt  26134  fta1blem  26195  drnguc1p  26198  ig1prsp  26205  plyco0  26216  plyeq0lem  26234  dgrub  26258  dgreq  26268  dgradd2  26293  dgrmul  26295  dgrcolem2  26299  dgrco  26300  plycpn  26314  plydivlem4  26321  plydiveu  26323  vieta1lem2  26336  vieta1  26337  aalioulem2  26358  aalioulem3  26359  aaliou3lem7  26374  tayl0  26386  ulmcn  26425  ulmdvlem3  26428  psercn  26453  abelth  26468  pilem3  26480  efif1olem1  26566  abslogimle  26597  argregt0  26634  argrege0  26635  logf1o2  26674  cxpsqrtlem  26726  cxpcn3  26773  abscxpbnd  26778  logreclem  26787  ang180lem2  26835  ang180lem3  26836  xrlimcnp  26993  harmonicbnd4  27036  fsumharmonic  27037  lgamgulmlem5  27058  lgambdd  27062  basellem4  27109  dvdsppwf1o  27211  dvdsflf1o  27212  fsumfldivdiaglem  27214  chpeq0  27234  chteq0  27235  chtub  27238  chpub  27246  dchrelbasd  27265  dchrmulcl  27275  dchrinv  27287  bposlem1  27310  bposlem2  27311  lgsdirprm  27357  lgsqrlem2  27373  lgsqrlem3  27374  lgsdchr  27381  lgseisenlem1  27401  lgseisenlem2  27402  lgseisenlem3  27403  lgsquadlem1  27406  2sqlem8  27452  2sqblem  27457  2sqmod  27462  chebbnd1lem1  27495  dchrisumlem1  27515  dchrisumlem2  27516  dchrisumlem3  27517  dchrisum0fno1  27537  pntrmax  27590  pntpbnd1a  27611  pntibndlem3  27618  pntlemn  27626  pntlemi  27630  pntlem3  27635  pntleml  27637  ostth1  27659  ostth2  27663  ostth3  27664  nosepon  27692  nolesgn2ores  27699  nogesgn1ores  27701  nosupres  27734  nosupbnd1lem2  27736  nosupbnd2lem1  27742  noinfres  27749  noinfbnd1lem2  27751  noinfbnd2lem1  27757  cofcutrtime  27941  divmuldivsd  28228  nnsgt0  28307  ercgrg  28441  motco  28464  cnvmot  28465  legso  28523  mirmot  28599  colopp  28693  hphl  28695  lmicom  28712  lmimid  28718  lmimot  28722  hypcgrlem1  28723  hypcgrlem2  28724  trgcopyeulem  28729  inagswap  28765  inaghl  28769  cgrg3col4  28777  brbtwn2  28836  axlowdimlem3  28875  axlowdimlem16  28888  axcontlem8  28902  fusgrfis  29263  nbgr2vtx1edg  29283  0vtxrgr  29510  0vtxrusgr  29511  ewlkle  29539  wlk1ewlk  29574  uspgr2wlkeq2  29581  wlkp1lem8  29614  trlontrl  29645  pthonpth  29682  pthdlem2  29702  wlklnwwlkln1  29799  wlknewwlksn  29818  wwlksnred  29823  wwlksnredwwlkn0  29827  2trlond  29870  2pthond  29873  elwwlks2ons3im  29885  clwlkclwwlklem2a1  29922  clwlkclwwlkf1  29940  clwwlkel  29976  clwwlkwwlksb  29984  wwlksext2clwwlk  29987  1ewlk  30045  0trlon  30054  0pthon  30057  1pthond  30074  3trlond  30103  3pthond  30105  3spthond  30107  eupthres  30145  2clwwlk2clwwlk  30280  numclwwlk1lem2foa  30284  numclwwlk1lem2f1  30287  nvabs  30602  vacn  30624  nmcvcn  30625  nmblore  30716  0lno  30720  0blo  30722  nmlno0lem  30723  occl  31234  pjhthlem1  31321  pjpjpre  31349  nmopre  31800  nmlnop0iALT  31925  nmophmi  31961  leoprf2  32057  stlesi  32171  disjdifprg  32495  disjun0  32515  fsuppcurry1  32639  fsuppcurry2  32640  fpwrelmap  32647  fzspl  32695  dfmgc2lem  32868  pwrssmgc  32873  xrge0tsmsd  32930  ogrpaddlt  32956  ogrpsublt  32960  psgnfzto1stlem  32982  fzto1st1  32984  evpmid  33030  pnfinf  33052  rmfsupp2  33108  fracfld  33163  ornglmullt  33190  orngrmullt  33191  orngmullt  33192  ofldlt1  33196  isarchiofld  33200  dvdsruassoi  33265  nsgmgc  33293  drngidl  33314  qsdrngi  33376  deg1addlt  33473  ply1degltdimlem  33523  lbsdiflsp0  33527  fedgmul  33532  fldexttr  33553  fldextid  33554  irngnzply1lem  33572  irredminply  33589  algextdeglem8  33597  rtelextdg2lem  33599  constrsslem  33613  qtopt1  33663  reff  33667  locfinreflem  33668  metideq  33721  metider  33722  pstmxmet  33725  qqhval2lem  33809  qqhcn  33819  qqhucn  33820  pwsiga  33976  prsiga  33977  measle0  34054  mbfmcst  34106  1stmbfm  34107  2ndmbfm  34108  imambfm  34109  cnmbfm  34110  mbfmco  34111  mbfmco2  34112  0elcarsg  34154  carsgclctun  34168  sibfof  34187  oddpwdc  34201  eulerpartlemmf  34222  eulerpartlemgs2  34227  0rrv  34298  ballotlemfc0  34339  ballotlemfcc  34340  signstfveq0  34436  breprexplemc  34491  bnj1452  34910  usgrgt2cycl  34971  acycgr1v  34990  derangen  35013  subfacval3  35030  cvmseu  35117  cvmliftmolem2  35123  cvmliftlem7  35132  cvmliftlem15  35139  cvmlift2lem9a  35144  cvmlift2lem9  35152  cvmlift2lem10  35153  cvmlift2lem11  35154  cvmlift2lem12  35155  cvmlift3lem6  35165  cvmlift3lem8  35167  ex-sategoelel  35262  ex-sategoelelomsuc  35267  mclsppslem  35424  mclspps  35425  wsuclem  35662  fness  36074  fnetr  36076  fnessref  36082  refssfne  36083  neibastop1  36084  neibastop2  36086  tailfb  36102  filnetlem3  36105  bj-finsumval0  37005  bj-rvecvec  37019  dfgcd3  37044  lindsadd  37327  poimirlem13  37347  poimirlem15  37349  poimirlem24  37358  poimirlem28  37362  mblfinlem2  37372  ovoliunnfl  37376  volsupnfl  37379  mbfresfi  37380  iblabsnc  37398  iblmulc2nc  37399  ftc1cnnclem  37405  ftc1cnnc  37406  ftc1anc  37415  sdclem2  37456  metf1o  37469  ismtyhmeolem  37518  ismtyres  37522  heibor1lem  37523  bfplem2  37537  bfp  37538  rrncmslem  37546  iccbnd  37554  icccmpALT  37555  rngogrphom  37685  rngoisoco  37696  keridl  37746  lsmcv2  38740  lsatcv0  38742  lcvexchlem4  38748  lcvexchlem5  38749  l1cvpat  38765  lfl0f  38780  lfladdcl  38782  lflnegcl  38786  lkrlss  38806  eqlkr  38810  lkrlsp  38813  lkrlsp2  38814  lshpkrcl  38827  lkrin  38875  1cvrjat  39187  llni  39220  llnle  39230  lplni  39244  lplnle  39252  llncvrlpln2  39269  2atmat  39273  lvoli  39287  lplncvrlvol2  39327  elpaddri  39514  paddclN  39554  pclclN  39603  pclfinN  39612  0psubclN  39655  1psubclN  39656  atpsubclN  39657  pmapsubclN  39658  osumclN  39679  pexmidN  39681  pexmidlem6N  39687  lhp2lt  39713  lautcnv  39802  idlaut  39808  lautco  39809  idldil  39826  ldilcnv  39827  ldilco  39828  ltrncnv  39858  idltrn  39862  cdleme16d  39993  cdleme50laut  40259  cdleme50ldil  40260  cdleme50ltrn  40269  ltrnco  40431  dian0  40751  dia0eldmN  40752  dia1eldmN  40753  dialss  40758  diaintclN  40770  docaclN  40836  doca2N  40838  djajN  40849  dibintclN  40879  diblss  40882  dicvaddcl  40902  dicvscacl  40903  dicn0  40904  cdlemn11a  40919  dihord2cN  40933  dihord11b  40934  dihord6apre  40968  dihmeetlem1N  41002  dihglblem5apreN  41003  dihpN  41048  dihjatcclem4  41133  dochkr1  41190  islpoldN  41196  lcfrlem31  41285  mapdpglem18  41401  mapdheq2  41441  mapdheq4  41444  mapdh6aN  41447  hdmap1l6a  41521  hdmap14lem4a  41583  lcmineqlem4  41744  frlmfzoccat  42195  drnginvmuld  42217  psrbagres  42236  evlselvlem  42276  evlselv  42277  fsuppind  42280  fsuppssind  42283  prjspvs  42300  irrapxlem4  42519  pell1234qrdich  42555  pell1qr1  42565  pell14qrgap  42569  pellqrexplicit  42571  rmspecfund  42603  fzmaxdif  42676  acongeq  42678  jm2.23  42691  jm3.1  42715  lmhmlnmsplit  42785  hbt  42828  dgrsub2  42833  proot1ex  42898  cantnfub  43024  cantnfresb  43027  cantnf2  43028  tfsconcatfv2  43043  tfsconcatrn  43045  tfsconcatb0  43047  naddcnff  43065  naddcnffo  43067  naddcnfid1  43070  naddcnfid2  43071  clublem  43314  dftrcl3  43424  mnugrud  43995  hashnzfz2  44032  dvconstbi  44045  ubelsupr  44656  restopn3  44792  wessf1ornlem  44828  lefldiveq  44943  iccintsng  45177  climsuse  45265  mullimc  45273  limcdm0  45275  limccog  45277  mullimcf  45280  constlimc  45281  idlimc  45283  limcperiod  45285  limsupre  45298  limcleqr  45301  neglimc  45304  addlimc  45305  0ellimcdiv  45306  xlimliminflimsup  45519  cncfshift  45531  cncfperiod  45536  cncfuni  45543  icccncfext  45544  cncfiooicclem1  45550  fperdvper  45576  ioodvbdlimc1lem2  45589  ioodvbdlimc2lem  45591  mbfres2cn  45615  iblsplit  45623  stoweidlem7  45664  stoweidlem13  45670  stoweidlem26  45683  wallispilem3  45724  stirlinglem6  45736  stirlinglem10  45740  dirkercncf  45764  fourierdlem6  45770  fourierdlem11  45775  fourierdlem12  45776  fourierdlem15  45779  fourierdlem26  45790  fourierdlem42  45806  fourierdlem50  45813  fourierdlem51  45814  fourierdlem52  45815  fourierdlem54  45817  fourierdlem62  45825  fourierdlem79  45842  fourierdlem102  45865  fourierdlem114  45877  etransclem23  45914  zgeltp1eq  46958  setsnidel  46985  preimafvsnel  46987  iccpartres  47026  prpair  47109  fpprel2  47349  isubgrsubgr  47470  isuspgrim  47490  grimidvtxedg  47491  grimcnv  47494  uhgrimgrlim  47529  isassintop  47623  rhmsubcALTV  47698  srhmsubcALTV  47738  fldhmsubcALTV  47746  rmfsupp  47789  mndpfsupp  47791  scmfsupp  47793  mptcfsupp  47795  lcoel0  47847  lincsumcl  47850  lincscmcl  47851  lcoss  47855  lindsrng01  47887  lincreslvec3  47901  lindssnlvec  47905  zgtp1leeq  47940  lubsscl  48330  glbsscl  48331  idmon  48373  idepi  48374  thinciso  48417