MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbir2and Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 mpbir2and.1 . . 3 (𝜑𝜒)
2 mpbir2and.2 . . 3 (𝜑𝜃)
31, 2jca 510 . 2 (𝜑 → (𝜒𝜃))
4 mpbir2and.3 . 2 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
53, 4mpbird 256 1 (𝜑𝜓)
Colors of variables: wff setvar class
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  7065  fveqressseq  7086  fmptsng  7175  fmptsnd  7176  fnprb  7218  fntpb  7219  fpr3g  8289  frrlem4  8293  1ellim  8517  isfsuppd  9390  fdmfifsupp  9398  fczfsuppd  9409  fsuppmptif  9422  fsuppco2  9426  fsuppcor  9427  dffi3  9454  suppr  9494  infpr  9526  ordtypelem7  9547  cantnf0  9698  cantnfp1lem1  9701  cantnfp1lem2  9702  cantnfp1lem3  9703  cantnflem1a  9708  cantnflem1d  9711  cantnflem1  9712  cantnf  9716  rankpwi  9846  carduni  10004  fin23lem32  10367  fpwwe2lem5  10658  fpwwe2lem11  10664  fpwwe2lem12  10665  fpwwe2  10666  inttsk  10797  grutsk1  10844  add20  11756  supaddc  12211  supadd  12212  supmul  12216  suprzcl  12672  uzid  12867  uzwo3  12957  rpnnen1lem5  12995  xrletrid  13166  xrre  13180  xrre3  13182  xleadd1a  13264  xlemul1a  13299  elioc2  13419  elico2  13420  elicc2  13421  elfz1eq  13544  fzadd2  13568  fznatpl1  13587  elfz1uz  13603  nn0fz0  13631  fzctr  13645  fzo1fzo0n0  13715  fzoaddel  13717  elincfzoext  13722  flid  13805  flval3  13812  fladdz  13822  fldiv  13857  modid  13893  hashf1lem1  14447  hashf1lem1OLD  14448  pfxccatin12d  14727  repswpfx  14767  2cshw  14795  pfx2  14930  wwlktovf1  14940  sqeqd  15145  01sqrexlem7  15227  max0add  15289  abs2difabs  15313  rddif  15319  fzomaxdiflem  15321  rexico  15332  icodiamlt  15414  limsupgre  15457  rlim3  15474  icco1  15516  rlimclim  15522  rlimuni  15526  rlimresb  15541  isercolllem2  15644  isercolllem3  15645  isercoll  15646  caucvgrlem  15651  caurcvgr  15652  iseraltlem3  15662  fsum00  15776  o1fsum  15791  bitsfzolem  16408  bitsfzo  16409  bitsmod  16410  bitscmp  16412  gcd0id  16493  gcdneg  16496  bezoutlem4  16517  nn0seqcvgd  16540  lcmneg  16573  lcmfunsnlem2lem2  16609  qredeq  16627  prmind2  16655  eulerthlem2  16750  pcpremul  16811  pcidlem  16840  pcgcd1  16845  fldivp1  16865  pcfaclem  16866  4sqlem17  16929  vdwlem1  16949  vdwlem6  16954  vdwlem12  16960  vdwlem13  16961  0ram  16988  ram0  16990  ramub1lem1  16994  invco  17753  sectmon  17764  monsect  17765  invid  17769  ssctr  17807  ssceq  17808  0ssc  17822  0subcat  17823  catsubcat  17824  issubc3  17834  fullsubc  17835  funcinv  17858  fthmon  17915  fuccocl  17955  fucidcl  17956  invfuc  17965  2initoinv  17998  2termoinv  18005  elhomai  18021  setcmon  18075  setcepi  18076  catcisolem  18098  curf2cl  18222  yonedalem4c  18268  yonedalem3  18271  yoniso  18276  lublecl  18352  isacs3lem  18533  tsrdir  18595  rabsubmgmd  18663  submgmid  18665  subsubmgm  18669  mgmhmima  18674  mgmhmeql  18675  mnd1  18735  sgrp2nmndlem4  18884  sgrp2nmndlem5  18885  0subg  19110  nmznsg  19127  ghmpreima  19196  ghmeql  19197  ghmnsgpreima  19199  kerf1ghm  19205  cntzsgrpcl  19289  cntzsubm  19293  cntzsubg  19294  cntzmhm  19296  symgextfo  19381  symgfixf1  19396  symgfixfolem1  19397  odlem2  19498  finodsubmsubg  19526  gexlem2  19541  gexcl2  19548  sylow1lem5  19561  subgslw  19575  slwhash  19583  fislw  19584  sylow3lem1  19586  lsmsubg  19613  efgredlemd  19703  efgredlem  19706  efgcpbllemb  19714  frgpuplem  19731  cyggeninv  19842  iscygd  19846  iscygodd  19847  gsumzadd  19881  gsumconst  19893  gsumpt  19921  gsum2dlem2  19930  gsum2d  19931  gsum2d2lem  19932  dprdfcntz  19976  eldprdi  19979  subgdmdprd  19995  subgdprd  19996  dprdpr  20011  ablfac1c  20032  ablfac1eu  20034  ablfaclem3  20048  ring1  20250  subrngint  20501  rhmimasubrng  20507  cntzsubrng  20508  rhmeql  20546  rhmima  20547  cntzsubr  20549  rnghmsscmap2  20566  rnghmsscmap  20567  rnghmsubcsetc  20570  zrzeroorngc  20581  rhmsscmap2  20595  rhmsscmap  20596  rhmsubcsetc  20599  rhmsscrnghm  20602  rhmsubcrngc  20605  srhmsubc  20617  rhmsubc  20626  issubdrg  20672  fldhmsubc  20677  imadrhmcl  20689  isabvd  20704  abvdiv  20721  lsslsp  20903  lsslspOLD  20904  lmhmima  20936  lmhmpreima  20937  lmhmeql  20944  lsmcl  20972  lspfixed  21020  rnglidlrng  21146  rngqiprngim  21198  rng2idl1cntr  21199  qsssubdrg  21363  gzrngunit  21370  pzriprnglem8  21418  evpmodpmf1o  21532  ocvpj  21655  dsmm0cl  21678  dsmmacl  21679  dsmmsubg  21681  dsmmlss  21682  frlmsplit2  21711  uvcff  21729  lindfrn  21759  f1lindf  21760  lindsss  21762  issubassa  21804  issubassa2  21829  snifpsrbag  21859  psrbaglesupp  21861  psrbaglesuppOLD  21862  psrbaglecl  21863  psrbagleclOLD  21864  psrbagaddcl  21865  psrbagaddclOLD  21866  psrbagcon  21867  psrbagconOLD  21868  mplsubglem  21948  mpllsslem  21949  mplassa  21971  subrgmpl  21977  mplcoe5  21985  mplbas2  21987  mplind  22021  mpfind  22060  ismhp2  22074  mhpmulcl  22081  mhplss  22087  ply1assa  22127  coe1tmmul2  22204  coe1tmmul  22205  cply1coe0bi  22230  dmatid  22427  dmatsubcl  22430  dmatscmcl  22435  scmatid  22446  scmataddcl  22448  scmatsubcl  22449  scmatmulcl  22450  smatvscl  22456  scmatrhmcl  22460  mat0scmat  22470  mat1scmat  22471  mdet0pr  22524  chmaidscmat  22780  distop  22928  indistopon  22934  ppttop  22940  epttop  22942  mretopd  23026  toponmre  23027  neiss  23043  opnneissb  23048  ssnei2  23050  innei  23059  neiptoptop  23065  ordtcld1  23131  ordtcld2  23132  lmconst  23195  cnpnei  23198  iscncl  23203  cnss1  23210  cnss2  23211  cncnpi  23212  cncnp  23214  cnconst2  23217  cnrest  23219  cnpresti  23222  cnpdis  23227  paste  23228  lmcnp  23238  cnhaus  23288  hauscmp  23341  2ndcomap  23392  1stcelcls  23395  1stccnp  23396  llyrest  23419  nllyrest  23420  llyidm  23422  nllyidm  23423  ssref  23446  reftr  23448  refun0  23449  dissnref  23462  kgentopon  23472  kgenidm  23481  kgencn3  23492  txcld  23537  neitx  23541  tx1cn  23543  tx2cn  23544  ptcld  23547  xkoccn  23553  txcnp  23554  ptcnp  23556  txcnmpt  23558  ptcn  23561  txdis1cn  23569  ptrescn  23573  txkgen  23586  xkoco1cn  23591  xkoco2cn  23592  xkococn  23594  xkoinjcn  23621  qtoptop2  23633  qtopuni  23636  qtopid  23639  qtopkgen  23644  basqtop  23645  tgqtop  23646  qtopss  23649  qtopeu  23650  qtoprest  23651  kqopn  23668  kqcld  23669  kqreglem2  23676  reghmph  23727  ordthmeolem  23735  qtopf1  23750  opnfbas  23776  isfil2  23790  fbasweak  23799  fsubbas  23801  filconn  23817  fbasrn  23818  rnelfmlem  23886  flimss2  23906  flimss1  23907  hausflim  23915  flimclslem  23918  flimsncls  23920  cnpflfi  23933  flfcnp2  23941  fclsfnflim  23961  cnextfvval  23999  cnextfres1  24002  symgtgp  24040  opnsubg  24042  ghmcnp  24049  qustgpopn  24054  qustgplem  24055  qustgphaus  24057  tsmsfbas  24062  ustfilxp  24147  utoptop  24169  utopbas  24170  restutopopn  24173  iducn  24218  cstucnd  24219  ucncn  24220  fmucnd  24227  cfilufg  24228  trcfilu  24229  cfiluweak  24230  neipcfilu  24231  psmetres2  24250  isxmetd  24262  xmetpsmet  24284  imasf1oxmet  24311  xblss2ps  24337  xblss2  24338  xblcntrps  24346  xblcntr  24347  blcld  24444  metustfbas  24496  cfilucfil  24498  restmetu  24509  ngptgp  24575  tngngpd  24600  nrmtngnrm  24605  tngnrg  24621  nlmvscn  24634  nrginvrcn  24639  nmo0  24682  nmoeq0  24683  nmoid  24689  nghmcn  24692  0nmhm  24702  blcvx  24744  iccntr  24767  xrge0tsms  24780  xmetdcn2  24783  metdstri  24797  metdscn  24802  rescncf  24847  cncfco  24857  oprpiece1res2  24907  cnheibor  24911  cnllycmp  24912  bndth  24914  ishtpyd  24931  isphtpyd  24942  pcoval2  24973  nmhmcn  25077  ipcn  25204  lmnn  25221  cfilss  25228  iscfil3  25231  cfilfcls  25232  cmetcaulem  25246  iscmet3lem2  25250  cfilres  25254  lmcau  25271  flimcfil  25272  cncmet  25280  rlmbn  25319  minveclem3b  25386  pjthlem1  25395  pjth2  25398  ivthlem3  25412  ovolssnul  25446  ovolctb  25449  ovoliunnul  25466  ovolsca  25474  ovolicopnf  25483  voliunlem2  25510  volsup  25515  dyadmaxlem  25556  vitalilem5  25571  mbfres  25603  mbfss  25605  mbfmulc2re  25607  mbfadd  25620  mbfmulc2  25622  mbflim  25627  i1faddlem  25652  i1fmullem  25653  mbfmul  25686  itg2mulc  25707  itg2cnlem1  25721  ibl0  25746  iblposlem  25751  itgreval  25756  iblneg  25762  iblss  25764  iblss2  25765  itgle  25769  iblconst  25777  iblabs  25788  iblabsr  25789  iblmulc2  25790  bddmulibl  25798  limciun  25853  limcun  25854  dvres2lem  25869  dvidlem  25874  dvcnp2  25879  dvcnp2OLD  25880  dvcn  25881  cpnres  25897  dvaddbr  25898  dvmulbr  25899  dvmulbrOLD  25900  dvcobr  25907  dvcobrOLD  25908  dvcjbr  25911  dvrec  25917  dvcnvlem  25938  dvferm  25950  dvlip2  25958  dveq0  25963  dv11cn  25964  dvivthlem1  25971  lhop1  25977  lhop2  25978  lhop  25979  dvcnvre  25982  dvfsumlem3  25993  dvfsumlem4  25994  dvfsumrlim  25996  dvfsum2  25999  ftc1a  26002  ftc1lem4  26004  ftc1lem6  26006  ftc1  26007  coe1mul3  26065  deg1addle2  26068  deg1sublt  26076  fta1blem  26135  drnguc1p  26138  ig1prsp  26145  plyco0  26156  plyeq0lem  26174  dgrub  26198  dgreq  26208  dgradd2  26233  dgrmul  26235  dgrcolem2  26239  dgrco  26240  plycpn  26254  plydivlem4  26261  plydiveu  26263  vieta1lem2  26276  vieta1  26277  aalioulem2  26298  aalioulem3  26299  aaliou3lem7  26314  tayl0  26326  ulmcn  26365  ulmdvlem3  26368  psercn  26393  abelth  26408  pilem3  26420  efif1olem1  26506  abslogimle  26537  argregt0  26574  argrege0  26575  logf1o2  26614  cxpsqrtlem  26666  cxpcn3  26713  abscxpbnd  26718  logreclem  26724  ang180lem2  26772  ang180lem3  26773  xrlimcnp  26930  harmonicbnd4  26973  fsumharmonic  26974  lgamgulmlem5  26995  lgambdd  26999  basellem4  27046  dvdsppwf1o  27148  dvdsflf1o  27149  fsumfldivdiaglem  27151  chpeq0  27171  chteq0  27172  chtub  27175  chpub  27183  dchrelbasd  27202  dchrmulcl  27212  dchrinv  27224  bposlem1  27247  bposlem2  27248  lgsdirprm  27294  lgsqrlem2  27310  lgsqrlem3  27311  lgsdchr  27318  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgsquadlem1  27343  2sqlem8  27389  2sqblem  27394  2sqmod  27399  chebbnd1lem1  27432  dchrisumlem1  27452  dchrisumlem2  27453  dchrisumlem3  27454  dchrisum0fno1  27474  pntrmax  27527  pntpbnd1a  27548  pntibndlem3  27555  pntlemn  27563  pntlemi  27567  pntlem3  27572  pntleml  27574  ostth1  27596  ostth2  27600  ostth3  27601  nosepon  27628  nolesgn2ores  27635  nogesgn1ores  27637  nosupres  27670  nosupbnd1lem2  27672  nosupbnd2lem1  27678  noinfres  27685  noinfbnd1lem2  27687  noinfbnd2lem1  27693  cofcutrtime  27877  divmuldivsd  28164  nnsgt0  28243  ercgrg  28377  motco  28400  cnvmot  28401  legso  28459  mirmot  28535  colopp  28629  hphl  28631  lmicom  28648  lmimid  28654  lmimot  28658  hypcgrlem1  28659  hypcgrlem2  28660  trgcopyeulem  28665  inagswap  28701  inaghl  28705  cgrg3col4  28713  brbtwn2  28772  axlowdimlem3  28811  axlowdimlem16  28824  axcontlem8  28838  fusgrfis  29199  nbgr2vtx1edg  29219  0vtxrgr  29446  0vtxrusgr  29447  ewlkle  29475  wlk1ewlk  29510  uspgr2wlkeq2  29517  wlkp1lem8  29550  trlontrl  29581  pthonpth  29618  pthdlem2  29638  wlklnwwlkln1  29735  wlknewwlksn  29754  wwlksnred  29759  wwlksnredwwlkn0  29763  2trlond  29806  2pthond  29809  elwwlks2ons3im  29821  clwlkclwwlklem2a1  29858  clwlkclwwlkf1  29876  clwwlkel  29912  clwwlkwwlksb  29920  wwlksext2clwwlk  29923  1ewlk  29981  0trlon  29990  0pthon  29993  1pthond  30010  3trlond  30039  3pthond  30041  3spthond  30043  eupthres  30081  2clwwlk2clwwlk  30216  numclwwlk1lem2foa  30220  numclwwlk1lem2f1  30223  nvabs  30538  vacn  30560  nmcvcn  30561  nmblore  30652  0lno  30656  0blo  30658  nmlno0lem  30659  occl  31170  pjhthlem1  31257  pjpjpre  31285  nmopre  31736  nmlnop0iALT  31861  nmophmi  31897  leoprf2  31993  stlesi  32107  disjdifprg  32422  disjun0  32442  fsuppcurry1  32564  fsuppcurry2  32565  fpwrelmap  32572  fzspl  32615  dfmgc2lem  32779  pwrssmgc  32784  xrge0tsmsd  32828  ogrpaddlt  32854  ogrpsublt  32858  psgnfzto1stlem  32878  fzto1st1  32880  evpmid  32926  pnfinf  32948  rmfsupp2  33002  fracfld  33055  ornglmullt  33082  orngrmullt  33083  orngmullt  33084  ofldlt1  33088  isarchiofld  33092  dvdsruassoi  33149  nsgmgc  33184  drngidl  33211  qsdrngi  33268  deg1addlt  33340  ply1degltdimlem  33390  lbsdiflsp0  33394  fedgmul  33399  fldexttr  33420  fldextid  33421  irngnzply1lem  33438  irredminply  33454  algextdeglem8  33462  qtopt1  33506  reff  33510  locfinreflem  33511  metideq  33564  metider  33565  pstmxmet  33568  qqhval2lem  33652  qqhcn  33662  qqhucn  33663  pwsiga  33819  prsiga  33820  measle0  33897  mbfmcst  33949  1stmbfm  33950  2ndmbfm  33951  imambfm  33952  cnmbfm  33953  mbfmco  33954  mbfmco2  33955  0elcarsg  33997  carsgclctun  34011  sibfof  34030  oddpwdc  34044  eulerpartlemmf  34065  eulerpartlemgs2  34070  0rrv  34141  ballotlemfc0  34182  ballotlemfcc  34183  signstfveq0  34279  breprexplemc  34334  bnj1452  34753  usgrgt2cycl  34810  acycgr1v  34829  derangen  34852  subfacval3  34869  cvmseu  34956  cvmliftmolem2  34962  cvmliftlem7  34971  cvmliftlem15  34978  cvmlift2lem9a  34983  cvmlift2lem9  34991  cvmlift2lem10  34992  cvmlift2lem11  34993  cvmlift2lem12  34994  cvmlift3lem6  35004  cvmlift3lem8  35006  ex-sategoelel  35101  ex-sategoelelomsuc  35106  mclsppslem  35263  mclspps  35264  wsuclem  35491  fness  35903  fnetr  35905  fnessref  35911  refssfne  35912  neibastop1  35913  neibastop2  35915  tailfb  35931  filnetlem3  35934  bj-finsumval0  36834  bj-rvecvec  36848  dfgcd3  36873  lindsadd  37156  poimirlem13  37176  poimirlem15  37178  poimirlem24  37187  poimirlem28  37191  mblfinlem2  37201  ovoliunnfl  37205  volsupnfl  37208  mbfresfi  37209  iblabsnc  37227  iblmulc2nc  37228  ftc1cnnclem  37234  ftc1cnnc  37235  ftc1anc  37244  sdclem2  37285  metf1o  37298  ismtyhmeolem  37347  ismtyres  37351  heibor1lem  37352  bfplem2  37366  bfp  37367  rrncmslem  37375  iccbnd  37383  icccmpALT  37384  rngogrphom  37514  rngoisoco  37525  keridl  37575  lsmcv2  38570  lsatcv0  38572  lcvexchlem4  38578  lcvexchlem5  38579  l1cvpat  38595  lfl0f  38610  lfladdcl  38612  lflnegcl  38616  lkrlss  38636  eqlkr  38640  lkrlsp  38643  lkrlsp2  38644  lshpkrcl  38657  lkrin  38705  1cvrjat  39017  llni  39050  llnle  39060  lplni  39074  lplnle  39082  llncvrlpln2  39099  2atmat  39103  lvoli  39117  lplncvrlvol2  39157  elpaddri  39344  paddclN  39384  pclclN  39433  pclfinN  39442  0psubclN  39485  1psubclN  39486  atpsubclN  39487  pmapsubclN  39488  osumclN  39509  pexmidN  39511  pexmidlem6N  39517  lhp2lt  39543  lautcnv  39632  idlaut  39638  lautco  39639  idldil  39656  ldilcnv  39657  ldilco  39658  ltrncnv  39688  idltrn  39692  cdleme16d  39823  cdleme50laut  40089  cdleme50ldil  40090  cdleme50ltrn  40099  ltrnco  40261  dian0  40581  dia0eldmN  40582  dia1eldmN  40583  dialss  40588  diaintclN  40600  docaclN  40666  doca2N  40668  djajN  40679  dibintclN  40709  diblss  40712  dicvaddcl  40732  dicvscacl  40733  dicn0  40734  cdlemn11a  40749  dihord2cN  40763  dihord11b  40764  dihord6apre  40798  dihmeetlem1N  40832  dihglblem5apreN  40833  dihpN  40878  dihjatcclem4  40963  dochkr1  41020  islpoldN  41026  lcfrlem31  41115  mapdpglem18  41231  mapdheq2  41271  mapdheq4  41274  mapdh6aN  41277  hdmap1l6a  41351  hdmap14lem4a  41413  lcmineqlem4  41572  frlmfzoccat  41813  drnginvmuld  41831  psrbagres  41844  evlselvlem  41884  evlselv  41885  fsuppind  41888  fsuppssind  41891  prjspvs  42099  irrapxlem4  42310  pell1234qrdich  42346  pell1qr1  42356  pell14qrgap  42360  pellqrexplicit  42362  rmspecfund  42394  fzmaxdif  42467  acongeq  42469  jm2.23  42482  jm3.1  42506  lmhmlnmsplit  42576  hbt  42619  dgrsub2  42624  proot1ex  42689  cantnfub  42815  cantnfresb  42818  cantnf2  42819  tfsconcatfv2  42834  tfsconcatrn  42836  tfsconcatb0  42838  naddcnff  42856  naddcnffo  42858  naddcnfid1  42861  naddcnfid2  42862  clublem  43105  dftrcl3  43215  mnugrud  43786  hashnzfz2  43823  dvconstbi  43836  ubelsupr  44447  restopn3  44586  wessf1ornlem  44622  lefldiveq  44737  iccintsng  44971  climsuse  45059  mullimc  45067  limcdm0  45069  limccog  45071  mullimcf  45074  constlimc  45075  idlimc  45077  limcperiod  45079  limsupre  45092  limcleqr  45095  neglimc  45098  addlimc  45099  0ellimcdiv  45100  xlimliminflimsup  45313  cncfshift  45325  cncfperiod  45330  cncfuni  45337  icccncfext  45338  cncfiooicclem1  45344  fperdvper  45370  ioodvbdlimc1lem2  45383  ioodvbdlimc2lem  45385  mbfres2cn  45409  iblsplit  45417  stoweidlem7  45458  stoweidlem13  45464  stoweidlem26  45477  wallispilem3  45518  stirlinglem6  45530  stirlinglem10  45534  dirkercncf  45558  fourierdlem6  45564  fourierdlem11  45569  fourierdlem12  45570  fourierdlem15  45573  fourierdlem26  45584  fourierdlem42  45600  fourierdlem50  45607  fourierdlem51  45608  fourierdlem52  45609  fourierdlem54  45611  fourierdlem62  45619  fourierdlem79  45636  fourierdlem102  45659  fourierdlem114  45671  etransclem23  45708  zgeltp1eq  46752  setsnidel  46780  preimafvsnel  46782  iccpartres  46821  prpair  46904  fpprel2  47144  isubgrsubgr  47265  isuspgrim  47285  grimidvtxedg  47286  grimcnv  47289  isassintop  47384  rhmsubcALTV  47459  srhmsubcALTV  47499  fldhmsubcALTV  47507  rmfsupp  47550  mndpfsupp  47552  scmfsupp  47554  mptcfsupp  47556  lcoel0  47608  lincsumcl  47611  lincscmcl  47612  lcoss  47616  lindsrng01  47648  lincreslvec3  47662  lindssnlvec  47666  zgtp1leeq  47701  lubsscl  48091  glbsscl  48092  idmon  48134  idepi  48135  thinciso  48178
  Copyright terms: Public domain W3C validator