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

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

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 398

This theorem is referenced by:  elpreimad  7061  fveqressseq  7082  fmptsng  7166  fmptsnd  7167  fnprb  7210  fntpb  7211  fpr3g  8270  frrlem4  8274  1ellim  8498  isfsuppd  9366  fdmfifsupp  9373  fczfsuppd  9381  fsuppmptif  9394  fsuppco2  9398  fsuppcor  9399  dffi3  9426  suppr  9466  infpr  9498  ordtypelem7  9519  cantnf0  9670  cantnfp1lem1  9673  cantnfp1lem2  9674  cantnfp1lem3  9675  cantnflem1a  9680  cantnflem1d  9683  cantnflem1  9684  cantnf  9688  rankpwi  9818  carduni  9976  fin23lem32  10339  fpwwe2lem5  10630  fpwwe2lem11  10636  fpwwe2lem12  10637  fpwwe2  10638  inttsk  10769  grutsk1  10816  add20  11726  supaddc  12181  supadd  12182  supmul  12186  suprzcl  12642  uzid  12837  uzwo3  12927  rpnnen1lem5  12965  xrletrid  13134  xrre  13148  xrre3  13150  xleadd1a  13232  xlemul1a  13267  elioc2  13387  elico2  13388  elicc2  13389  elfz1eq  13512  fzadd2  13536  fznatpl1  13555  elfz1uz  13571  nn0fz0  13599  fzctr  13613  fzo1fzo0n0  13683  fzoaddel  13685  elincfzoext  13690  flid  13773  flval3  13780  fladdz  13790  fldiv  13825  modid  13861  hashf1lem1  14415  hashf1lem1OLD  14416  pfxccatin12d  14695  repswpfx  14735  2cshw  14763  pfx2  14898  wwlktovf1  14908  sqeqd  15113  01sqrexlem7  15195  max0add  15257  abs2difabs  15281  rddif  15287  fzomaxdiflem  15289  rexico  15300  icodiamlt  15382  limsupgre  15425  rlim3  15442  icco1  15484  rlimclim  15490  rlimuni  15494  rlimresb  15509  isercolllem2  15612  isercolllem3  15613  isercoll  15614  caucvgrlem  15619  caurcvgr  15620  iseraltlem3  15630  fsum00  15744  o1fsum  15759  bitsfzolem  16375  bitsfzo  16376  bitsmod  16377  bitscmp  16379  gcd0id  16460  gcdneg  16463  bezoutlem4  16484  nn0seqcvgd  16507  lcmneg  16540  lcmfunsnlem2lem2  16576  qredeq  16594  prmind2  16622  eulerthlem2  16715  pcpremul  16776  pcidlem  16805  pcgcd1  16810  fldivp1  16830  pcfaclem  16831  4sqlem17  16894  vdwlem1  16914  vdwlem6  16919  vdwlem12  16925  vdwlem13  16926  0ram  16953  ram0  16955  ramub1lem1  16959  invco  17718  sectmon  17729  monsect  17730  invid  17734  ssctr  17772  ssceq  17773  0ssc  17787  0subcat  17788  catsubcat  17789  issubc3  17799  fullsubc  17800  funcinv  17823  fthmon  17878  fuccocl  17917  fucidcl  17918  invfuc  17927  2initoinv  17960  2termoinv  17967  elhomai  17983  setcmon  18037  setcepi  18038  catcisolem  18060  curf2cl  18184  yonedalem4c  18230  yonedalem3  18233  yoniso  18238  lublecl  18314  isacs3lem  18495  tsrdir  18557  mnd1  18667  sgrp2nmndlem4  18809  sgrp2nmndlem5  18810  0subg  19031  nmznsg  19048  ghmpreima  19114  ghmeql  19115  ghmnsgpreima  19117  cntzsgrpcl  19198  cntzsubm  19202  cntzsubg  19203  cntzmhm  19205  symgextfo  19290  symgfixf1  19305  symgfixfolem1  19306  odlem2  19407  finodsubmsubg  19435  gexlem2  19450  gexcl2  19457  sylow1lem5  19470  subgslw  19484  slwhash  19492  fislw  19493  sylow3lem1  19495  lsmsubg  19522  efgredlemd  19612  efgredlem  19615  efgcpbllemb  19623  frgpuplem  19640  cyggeninv  19751  iscygd  19755  iscygodd  19756  gsumzadd  19790  gsumconst  19802  gsumpt  19830  gsum2dlem2  19839  gsum2d  19840  gsum2d2lem  19841  dprdfcntz  19885  eldprdi  19888  subgdmdprd  19904  subgdprd  19905  dprdpr  19920  ablfac1c  19941  ablfac1eu  19943  ablfaclem3  19957  ring1  20122  kerf1ghm  20282  rhmeql  20350  rhmima  20351  cntzsubr  20353  issubdrg  20401  imadrhmcl  20413  isabvd  20428  abvdiv  20445  lsslsp  20626  lmhmima  20658  lmhmpreima  20659  lmhmeql  20666  lsmcl  20694  lspfixed  20741  qsssubdrg  21004  gzrngunit  21011  evpmodpmf1o  21149  ocvpj  21272  dsmm0cl  21295  dsmmacl  21296  dsmmsubg  21298  dsmmlss  21299  frlmsplit2  21328  uvcff  21346  lindfrn  21376  f1lindf  21377  lindsss  21379  issubassa  21421  issubassa2  21446  snifpsrbag  21475  psrbaglesupp  21477  psrbaglesuppOLD  21478  psrbaglecl  21479  psrbagleclOLD  21480  psrbagaddcl  21481  psrbagaddclOLD  21482  psrbagcon  21483  psrbagconOLD  21484  mplsubglem  21558  mpllsslem  21559  mplassa  21581  subrgmpl  21587  mplcoe5  21595  mplbas2  21597  mplind  21631  mpfind  21670  ismhp2  21685  mhpmulcl  21692  mhplss  21698  ply1assa  21723  coe1tmmul2  21798  coe1tmmul  21799  cply1coe0bi  21824  dmatid  21997  dmatsubcl  22000  dmatscmcl  22005  scmatid  22016  scmataddcl  22018  scmatsubcl  22019  scmatmulcl  22020  smatvscl  22026  scmatrhmcl  22030  mat0scmat  22040  mat1scmat  22041  mdet0pr  22094  chmaidscmat  22350  distop  22498  indistopon  22504  ppttop  22510  epttop  22512  mretopd  22596  toponmre  22597  neiss  22613  opnneissb  22618  ssnei2  22620  innei  22629  neiptoptop  22635  ordtcld1  22701  ordtcld2  22702  lmconst  22765  cnpnei  22768  iscncl  22773  cnss1  22780  cnss2  22781  cncnpi  22782  cncnp  22784  cnconst2  22787  cnrest  22789  cnpresti  22792  cnpdis  22797  paste  22798  lmcnp  22808  cnhaus  22858  hauscmp  22911  2ndcomap  22962  1stcelcls  22965  1stccnp  22966  llyrest  22989  nllyrest  22990  llyidm  22992  nllyidm  22993  ssref  23016  reftr  23018  refun0  23019  dissnref  23032  kgentopon  23042  kgenidm  23051  kgencn3  23062  txcld  23107  neitx  23111  tx1cn  23113  tx2cn  23114  ptcld  23117  xkoccn  23123  txcnp  23124  ptcnp  23126  txcnmpt  23128  ptcn  23131  txdis1cn  23139  ptrescn  23143  txkgen  23156  xkoco1cn  23161  xkoco2cn  23162  xkococn  23164  xkoinjcn  23191  qtoptop2  23203  qtopuni  23206  qtopid  23209  qtopkgen  23214  basqtop  23215  tgqtop  23216  qtopss  23219  qtopeu  23220  qtoprest  23221  kqopn  23238  kqcld  23239  kqreglem2  23246  reghmph  23297  ordthmeolem  23305  qtopf1  23320  opnfbas  23346  isfil2  23360  fbasweak  23369  fsubbas  23371  filconn  23387  fbasrn  23388  rnelfmlem  23456  flimss2  23476  flimss1  23477  hausflim  23485  flimclslem  23488  flimsncls  23490  cnpflfi  23503  flfcnp2  23511  fclsfnflim  23531  cnextfvval  23569  cnextfres1  23572  symgtgp  23610  opnsubg  23612  ghmcnp  23619  qustgpopn  23624  qustgplem  23625  qustgphaus  23627  tsmsfbas  23632  ustfilxp  23717  utoptop  23739  utopbas  23740  restutopopn  23743  iducn  23788  cstucnd  23789  ucncn  23790  fmucnd  23797  cfilufg  23798  trcfilu  23799  cfiluweak  23800  neipcfilu  23801  psmetres2  23820  isxmetd  23832  xmetpsmet  23854  imasf1oxmet  23881  xblss2ps  23907  xblss2  23908  xblcntrps  23916  xblcntr  23917  blcld  24014  metustfbas  24066  cfilucfil  24068  restmetu  24079  ngptgp  24145  tngngpd  24170  nrmtngnrm  24175  tngnrg  24191  nlmvscn  24204  nrginvrcn  24209  nmo0  24252  nmoeq0  24253  nmoid  24259  nghmcn  24262  0nmhm  24272  blcvx  24314  iccntr  24337  xrge0tsms  24350  xmetdcn2  24353  metdstri  24367  metdscn  24372  rescncf  24413  cncfco  24423  oprpiece1res2  24468  cnheibor  24471  cnllycmp  24472  bndth  24474  ishtpyd  24491  isphtpyd  24502  pcoval2  24532  nmhmcn  24636  ipcn  24763  lmnn  24780  cfilss  24787  iscfil3  24790  cfilfcls  24791  cmetcaulem  24805  iscmet3lem2  24809  cfilres  24813  lmcau  24830  flimcfil  24831  cncmet  24839  rlmbn  24878  minveclem3b  24945  pjthlem1  24954  pjth2  24957  ivthlem3  24970  ovolssnul  25004  ovolctb  25007  ovoliunnul  25024  ovolsca  25032  ovolicopnf  25041  voliunlem2  25068  volsup  25073  dyadmaxlem  25114  vitalilem5  25129  mbfres  25161  mbfss  25163  mbfmulc2re  25165  mbfadd  25178  mbfmulc2  25180  mbflim  25185  i1faddlem  25210  i1fmullem  25211  mbfmul  25244  itg2mulc  25265  itg2cnlem1  25279  ibl0  25304  iblposlem  25309  itgreval  25314  iblneg  25320  iblss  25322  iblss2  25323  itgle  25327  iblconst  25335  iblabs  25346  iblabsr  25347  iblmulc2  25348  bddmulibl  25356  limciun  25411  limcun  25412  dvres2lem  25427  dvidlem  25432  dvcnp2  25437  dvcn  25438  cpnres  25454  dvaddbr  25455  dvmulbr  25456  dvcobr  25463  dvcjbr  25466  dvrec  25472  dvcnvlem  25493  dvferm  25505  dvlip2  25512  dveq0  25517  dv11cn  25518  dvivthlem1  25525  lhop1  25531  lhop2  25532  lhop  25533  dvcnvre  25536  dvfsumlem3  25545  dvfsumlem4  25546  dvfsumrlim  25548  dvfsum2  25551  ftc1a  25554  ftc1lem4  25556  ftc1lem6  25558  ftc1  25559  coe1mul3  25617  deg1addle2  25620  deg1sublt  25628  fta1blem  25686  drnguc1p  25688  ig1prsp  25695  plyco0  25706  plyeq0lem  25724  dgrub  25748  dgreq  25758  dgradd2  25782  dgrmul  25784  dgrcolem2  25788  dgrco  25789  plycpn  25802  plydivlem4  25809  plydiveu  25811  vieta1lem2  25824  vieta1  25825  aalioulem2  25846  aalioulem3  25847  aaliou3lem7  25862  tayl0  25874  ulmcn  25911  ulmdvlem3  25914  psercn  25938  abelth  25953  pilem3  25965  efif1olem1  26051  abslogimle  26082  argregt0  26118  argrege0  26119  logf1o2  26158  cxpsqrtlem  26210  cxpcn3  26256  abscxpbnd  26261  logreclem  26267  ang180lem2  26315  ang180lem3  26316  xrlimcnp  26473  harmonicbnd4  26515  fsumharmonic  26516  lgamgulmlem5  26537  lgambdd  26541  basellem4  26588  dvdsppwf1o  26690  dvdsflf1o  26691  fsumfldivdiaglem  26693  chpeq0  26711  chteq0  26712  chtub  26715  chpub  26723  dchrelbasd  26742  dchrmulcl  26752  dchrinv  26764  bposlem1  26787  bposlem2  26788  lgsdirprm  26834  lgsqrlem2  26850  lgsqrlem3  26851  lgsdchr  26858  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgsquadlem1  26883  2sqlem8  26929  2sqblem  26934  2sqmod  26939  chebbnd1lem1  26972  dchrisumlem1  26992  dchrisumlem2  26993  dchrisumlem3  26994  dchrisum0fno1  27014  pntrmax  27067  pntpbnd1a  27088  pntibndlem3  27095  pntlemn  27103  pntlemi  27107  pntlem3  27112  pntleml  27114  ostth1  27136  ostth2  27140  ostth3  27141  nosepon  27168  nolesgn2ores  27175  nogesgn1ores  27177  nosupres  27210  nosupbnd1lem2  27212  nosupbnd2lem1  27218  noinfres  27225  noinfbnd1lem2  27227  noinfbnd2lem1  27233  cofcutrtime  27414  ercgrg  27768  motco  27791  cnvmot  27792  legso  27850  mirmot  27926  colopp  28020  hphl  28022  lmicom  28039  lmimid  28045  lmimot  28049  hypcgrlem1  28050  hypcgrlem2  28051  trgcopyeulem  28056  inagswap  28092  inaghl  28096  cgrg3col4  28104  brbtwn2  28163  axlowdimlem3  28202  axlowdimlem16  28215  axcontlem8  28229  fusgrfis  28587  nbgr2vtx1edg  28607  0vtxrgr  28833  0vtxrusgr  28834  ewlkle  28862  wlk1ewlk  28897  uspgr2wlkeq2  28904  wlkp1lem8  28937  trlontrl  28968  pthonpth  29005  pthdlem2  29025  wlklnwwlkln1  29122  wlknewwlksn  29141  wwlksnred  29146  wwlksnredwwlkn0  29150  2trlond  29193  2pthond  29196  elwwlks2ons3im  29208  clwlkclwwlklem2a1  29245  clwlkclwwlkf1  29263  clwwlkel  29299  clwwlkwwlksb  29307  wwlksext2clwwlk  29310  1ewlk  29368  0trlon  29377  0pthon  29380  1pthond  29397  3trlond  29426  3pthond  29428  3spthond  29430  eupthres  29468  2clwwlk2clwwlk  29603  numclwwlk1lem2foa  29607  numclwwlk1lem2f1  29610  nvabs  29925  vacn  29947  nmcvcn  29948  nmblore  30039  0lno  30043  0blo  30045  nmlno0lem  30046  occl  30557  pjhthlem1  30644  pjpjpre  30672  nmopre  31123  nmlnop0iALT  31248  nmophmi  31284  leoprf2  31380  stlesi  31494  disjdifprg  31806  disjun0  31826  fsuppcurry1  31950  fsuppcurry2  31951  fpwrelmap  31958  fzspl  32001  dfmgc2lem  32165  pwrssmgc  32170  xrge0tsmsd  32209  ogrpaddlt  32235  ogrpsublt  32239  psgnfzto1stlem  32259  fzto1st1  32261  evpmid  32307  pnfinf  32329  rmfsupp2  32387  ornglmullt  32425  orngrmullt  32426  orngmullt  32427  ofldlt1  32431  isarchiofld  32435  dvdsruassoi  32489  nsgmgc  32523  drngidl  32551  qsdrngi  32609  ply1degltdimlem  32707  lbsdiflsp0  32711  fedgmul  32716  fldexttr  32737  fldextid  32738  irngnzply1lem  32754  qtopt1  32815  reff  32819  locfinreflem  32820  metideq  32873  metider  32874  pstmxmet  32877  qqhval2lem  32961  qqhcn  32971  qqhucn  32972  pwsiga  33128  prsiga  33129  measle0  33206  mbfmcst  33258  1stmbfm  33259  2ndmbfm  33260  imambfm  33261  cnmbfm  33262  mbfmco  33263  mbfmco2  33264  0elcarsg  33306  carsgclctun  33320  sibfof  33339  oddpwdc  33353  eulerpartlemmf  33374  eulerpartlemgs2  33379  0rrv  33450  ballotlemfc0  33491  ballotlemfcc  33492  signstfveq0  33588  breprexplemc  33644  bnj1452  34063  usgrgt2cycl  34121  acycgr1v  34140  derangen  34163  subfacval3  34180  cvmseu  34267  cvmliftmolem2  34273  cvmliftlem7  34282  cvmliftlem15  34289  cvmlift2lem9a  34294  cvmlift2lem9  34302  cvmlift2lem10  34303  cvmlift2lem11  34304  cvmlift2lem12  34305  cvmlift3lem6  34315  cvmlift3lem8  34317  ex-sategoelel  34412  ex-sategoelelomsuc  34417  mclsppslem  34574  mclspps  34575  wsuclem  34797  gg-dvcnp2  35174  gg-dvmulbr  35175  gg-dvcobr  35176  fness  35234  fnetr  35236  fnessref  35242  refssfne  35243  neibastop1  35244  neibastop2  35246  tailfb  35262  filnetlem3  35265  bj-finsumval0  36166  bj-rvecvec  36180  dfgcd3  36205  lindsadd  36481  poimirlem13  36501  poimirlem15  36503  poimirlem24  36512  poimirlem28  36516  mblfinlem2  36526  ovoliunnfl  36530  volsupnfl  36533  mbfresfi  36534  iblabsnc  36552  iblmulc2nc  36553  ftc1cnnclem  36559  ftc1cnnc  36560  ftc1anc  36569  sdclem2  36610  metf1o  36623  ismtyhmeolem  36672  ismtyres  36676  heibor1lem  36677  bfplem2  36691  bfp  36692  rrncmslem  36700  iccbnd  36708  icccmpALT  36709  rngogrphom  36839  rngoisoco  36850  keridl  36900  lsmcv2  37899  lsatcv0  37901  lcvexchlem4  37907  lcvexchlem5  37908  l1cvpat  37924  lfl0f  37939  lfladdcl  37941  lflnegcl  37945  lkrlss  37965  eqlkr  37969  lkrlsp  37972  lkrlsp2  37973  lshpkrcl  37986  lkrin  38034  1cvrjat  38346  llni  38379  llnle  38389  lplni  38403  lplnle  38411  llncvrlpln2  38428  2atmat  38432  lvoli  38446  lplncvrlvol2  38486  elpaddri  38673  paddclN  38713  pclclN  38762  pclfinN  38771  0psubclN  38814  1psubclN  38815  atpsubclN  38816  pmapsubclN  38817  osumclN  38838  pexmidN  38840  pexmidlem6N  38846  lhp2lt  38872  lautcnv  38961  idlaut  38967  lautco  38968  idldil  38985  ldilcnv  38986  ldilco  38987  ltrncnv  39017  idltrn  39021  cdleme16d  39152  cdleme50laut  39418  cdleme50ldil  39419  cdleme50ltrn  39428  ltrnco  39590  dian0  39910  dia0eldmN  39911  dia1eldmN  39912  dialss  39917  diaintclN  39929  docaclN  39995  doca2N  39997  djajN  40008  dibintclN  40038  diblss  40041  dicvaddcl  40061  dicvscacl  40062  dicn0  40063  cdlemn11a  40078  dihord2cN  40092  dihord11b  40093  dihord6apre  40127  dihmeetlem1N  40161  dihglblem5apreN  40162  dihpN  40207  dihjatcclem4  40292  dochkr1  40349  islpoldN  40355  lcfrlem31  40444  mapdpglem18  40560  mapdheq2  40600  mapdheq4  40603  mapdh6aN  40606  hdmap1l6a  40680  hdmap14lem4a  40742  lcmineqlem4  40897  frlmfzoccat  41079  drnginvmuld  41101  psrbagres  41115  evlselvlem  41158  evlselv  41159  fsuppind  41162  fsuppssind  41165  prjspvs  41352  irrapxlem4  41563  pell1234qrdich  41599  pell1qr1  41609  pell14qrgap  41613  pellqrexplicit  41615  rmspecfund  41647  fzmaxdif  41720  acongeq  41722  jm2.23  41735  jm3.1  41759  lmhmlnmsplit  41829  hbt  41872  dgrsub2  41877  proot1ex  41943  cantnfub  42071  cantnfresb  42074  cantnf2  42075  tfsconcatfv2  42090  tfsconcatrn  42092  tfsconcatb0  42094  naddcnff  42112  naddcnffo  42114  naddcnfid1  42117  naddcnfid2  42118  clublem  42361  dftrcl3  42471  mnugrud  43043  hashnzfz2  43080  dvconstbi  43093  ubelsupr  43704  restopn3  43845  wessf1ornlem  43882  lefldiveq  44002  iccintsng  44236  climsuse  44324  mullimc  44332  limcdm0  44334  limccog  44336  mullimcf  44339  constlimc  44340  idlimc  44342  limcperiod  44344  limsupre  44357  limcleqr  44360  neglimc  44363  addlimc  44364  0ellimcdiv  44365  xlimliminflimsup  44578  cncfshift  44590  cncfperiod  44595  cncfuni  44602  icccncfext  44603  cncfiooicclem1  44609  fperdvper  44635  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  mbfres2cn  44674  iblsplit  44682  stoweidlem7  44723  stoweidlem13  44729  stoweidlem26  44742  wallispilem3  44783  stirlinglem6  44795  stirlinglem10  44799  dirkercncf  44823  fourierdlem6  44829  fourierdlem11  44834  fourierdlem12  44835  fourierdlem15  44838  fourierdlem26  44849  fourierdlem42  44865  fourierdlem50  44872  fourierdlem51  44873  fourierdlem52  44874  fourierdlem54  44876  fourierdlem62  44884  fourierdlem79  44901  fourierdlem102  44924  fourierdlem114  44936  etransclem23  44973  zgeltp1eq  46017  setsnidel  46045  preimafvsnel  46047  iccpartres  46086  prpair  46169  fpprel2  46409  rabsubmgmd  46561  submgmid  46563  subsubmgm  46567  mgmhmima  46572  mgmhmeql  46573  isassintop  46620  subrngint  46739  rhmimasubrng  46745  cntzsubrng  46746  rnglidlrng  46758  rngqiprngim  46789  rng2idl1cntr  46790  pzriprnglem8  46812  rnghmsscmap2  46871  rnghmsscmap  46872  rnghmsubcsetc  46875  zrzeroorngc  46900  rhmsscmap2  46917  rhmsscmap  46918  rhmsubcsetc  46921  rhmsscrnghm  46924  rhmsubcrngc  46927  srhmsubc  46974  fldhmsubc  46982  rhmsubc  46988  srhmsubcALTV  46992  fldhmsubcALTV  47000  rhmsubcALTV  47006  rmfsupp  47050  mndpfsupp  47052  scmfsupp  47054  mptcfsupp  47056  lcoel0  47109  lincsumcl  47112  lincscmcl  47113  lcoss  47117  lindsrng01  47149  lincreslvec3  47163  lindssnlvec  47167  zgtp1leeq  47202  lubsscl  47593  glbsscl  47594  idmon  47636  idepi  47637  thinciso  47680