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

Theorem mpbir2and 922
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 532 . 2
4 mpbir2and.3 . 2
53, 4mpbird 232 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  fveqressseq  6027  fmptsng  6092  fmptsnd  6093  fnprb  6129  fnprOLD  6130  fdmfifsupp  7859  fczfsuppd  7867  fsuppmptif  7879  fsuppco2  7882  fsuppcor  7883  dffi3  7911  supmaxOLD  7946  suppr  7950  ordtypelem7  7970  cantnf0  8115  cantnfp1lem1  8118  cantnfp1lem2  8119  cantnfp1lem3  8120  cantnflem1a  8125  cantnflem1d  8128  cantnflem1  8129  cantnf  8133  cantnfleOLD  8141  cantnfp1lem1OLD  8144  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  cantnflem1aOLD  8148  cantnflem1cOLD  8150  cantnflem1dOLD  8151  cantnflem1OLD  8152  cantnfOLD  8155  mapfienOLD  8159  rankpwi  8262  carduni  8383  fin23lem32  8745  fpwwe2lem6  9034  fpwwe2lem9  9037  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  inttsk  9173  grutsk1  9220  add20  10089  supmul  10536  suprzcl  10967  uzwo3  11206  rpnnen1lem5  11241  xrre  11399  xrre3  11401  xleadd1a  11474  xlemul1a  11509  supxrre  11548  infmxrre  11556  ixxub  11579  ixxlb  11580  elioc2  11616  elico2  11617  elicc2  11618  elfz1eq  11726  fznatpl1  11763  nn0fz0  11803  fzctr  11816  fzo1fzo0n0  11864  fzoaddel  11873  flid  11945  flval3  11951  fladdz  11958  fldiv  11987  modid  12020  seqf1olem1  12146  bcval5  12396  hashf1lem1  12504  ccat2s1fvw  12642  wwlktovf1  12895  sqeqd  12999  sqrlem7  13082  max0add  13143  abs2difabs  13167  rddif  13173  fzomaxdiflem  13175  rexico  13186  limsupgre  13304  rlim3  13321  icco1  13363  rlimclim  13369  rlimuni  13373  rlimresb  13388  isercolllem2  13488  isercolllem3  13489  isercoll  13490  caucvgrlem  13495  caurcvgr  13496  iseraltlem3  13506  fsum00  13612  o1fsum  13627  dvdseq  14033  bitsfzolem  14084  bitsfzo  14085  bitsmod  14086  bitscmp  14088  gcd0id  14161  gcdneg  14164  bezoutlem4  14179  nn0seqcvgd  14199  prmind2  14228  qredeq  14247  isprm5  14253  hashdvds  14305  eulerthlem2  14312  pcpremul  14367  pcidlem  14395  pcgcd1  14400  pcadd2  14409  fldivp1  14416  pcfaclem  14417  prmreclem5  14438  4sqlem17  14479  vdwlem1  14499  vdwlem6  14504  vdwlem12  14510  vdwlem13  14511  0ram  14538  ram0  14540  ramub1lem1  14544  invco  15165  sectmon  15172  monsect  15173  ssctr  15194  ssceq  15195  0ssc  15206  0subcat  15207  catsubcat  15208  issubc3  15218  fullsubc  15219  funcinv  15242  fthmon  15296  fuccocl  15333  fucidcl  15334  invfuc  15343  elhomai  15360  setcmon  15414  setcepi  15415  catcisolem  15433  curf2cl  15500  yonedalem4c  15546  yonedalem3  15549  yoniso  15554  lublecl  15619  isacs3lem  15796  tsrdir  15868  mnd1  15961  mnd1OLD  15962  sgrp2nmndlem4  16046  sgrp2nmndlem5  16047  nmznsg  16245  ghmpreima  16288  ghmeql  16289  ghmnsgpreima  16291  cntzsubm  16373  cntzsubg  16374  cntzmhm  16376  symgextfo  16447  symgfixf1  16462  symgfixfolem1  16463  odlem2  16563  gexlem2  16602  gexcl2  16609  sylow1lem5  16622  subgslw  16636  slwhash  16644  fislw  16645  sylow3lem1  16647  lsmsubg  16674  efgredlemd  16762  efgredlem  16765  efgcpbllemb  16773  frgpuplem  16790  cyggeninv  16886  iscygd  16890  iscygodd  16891  gsumzadd  16935  gsumconst  16954  gsumpt  16988  gsumptOLD  16989  gsum2dlem2  16998  gsum2d  16999  gsum2d2lem  17001  dprdfcntz  17049  dprdfcntzOLD  17055  eldprdi  17058  eldprdiOLD  17065  subgdmdprd  17081  subgdprd  17082  dprdpr  17099  ablfac1c  17122  ablfac1eu  17124  ablfaclem3  17138  ring1  17248  kerf1hrm  17392  issubdrg  17454  rhmeql  17459  rhmima  17460  cntzsubr  17461  isabvd  17469  abvdiv  17486  lsslsp  17661  lmhmima  17693  lmhmpreima  17694  lmhmeql  17701  lsmcl  17729  lspfixed  17774  issubassa  17973  issubassa2  17994  snifpsrbag  18015  psrbaglesupp  18017  psrbaglesuppOLD  18018  psrbaglecl  18019  psrbagaddcl  18020  psrbagaddclOLD  18021  psrbagcon  18022  psrbasOLD  18031  psrlidmOLD  18057  psrridmOLD  18059  mvridlemOLD  18075  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  mplassa  18116  subrgmpl  18122  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  mplbas2  18134  mplbas2OLD  18135  mplind  18167  evlslem3  18183  mpfind  18205  ply1assa  18238  coe1tmmul2  18317  coe1tmmul  18318  cply1coe0bi  18342  qsssubdrg  18477  gzrngunit  18483  evpmodpmf1o  18632  ocvpj  18748  dsmm0cl  18771  dsmmacl  18772  dsmmsubg  18774  dsmmlss  18775  frlmsplit2  18803  uvcff  18822  lindfrn  18856  f1lindf  18857  lindsss  18859  mat1rngiso  18988  dmatid  18997  dmatsubcl  19000  dmatscmcl  19005  scmatid  19016  scmataddcl  19018  scmatsubcl  19019  scmatmulcl  19020  smatvscl  19026  scmatrhmcl  19030  scmatrngiso  19038  mat0scmat  19040  mat1scmat  19041  mdet0pr  19094  m2cpmrngiso  19259  pm2mprngiso  19323  chmaidscmat  19349  fvmptnn04if  19350  distop  19497  indistopon  19502  ppttop  19508  epttop  19510  mretopd  19593  toponmre  19594  neiss  19610  opnneissb  19615  ssnei2  19617  innei  19626  neiptoptop  19632  ordtcld1  19698  ordtcld2  19699  lmconst  19762  cnpnei  19765  iscncl  19770  cnss1  19777  cnss2  19778  cncnpi  19779  cncnp  19781  cnconst2  19784  cnrest  19786  cnpresti  19789  cnpdis  19794  paste  19795  lmcnp  19805  cnhaus  19855  hauscmp  19907  2ndcomap  19959  1stcelcls  19962  1stccnp  19963  llyrest  19986  nllyrest  19987  llyidm  19989  nllyidm  19990  ssref  20013  reftr  20015  refun0  20016  dissnref  20029  kgentopon  20039  kgenidm  20048  kgencn3  20059  txcld  20104  neitx  20108  tx1cn  20110  tx2cn  20111  ptcld  20114  xkoccn  20120  txcnp  20121  ptcnp  20123  txcnmpt  20125  ptcn  20128  txdis1cn  20136  ptrescn  20140  txkgen  20153  xkoco1cn  20158  xkoco2cn  20159  xkococn  20161  xkoinjcn  20188  qtoptop2  20200  qtopuni  20203  qtopid  20206  qtopkgen  20211  basqtop  20212  tgqtop  20213  qtopss  20216  qtopeu  20217  qtoprest  20218  kqopn  20235  kqcld  20236  kqreglem2  20243  reghmph  20294  ordthmeolem  20302  qtopf1  20317  opnfbas  20343  isfil2  20357  fbasweak  20366  fsubbas  20368  filcon  20384  fbasrn  20385  rnelfmlem  20453  flimss2  20473  flimss1  20474  hausflim  20482  flimclslem  20485  flimsncls  20487  cnpflfi  20500  flfcnp2  20508  fclsfnflim  20528  cnextfvval  20565  cnextfres  20568  symgtgp  20600  opnsubg  20606  ghmcnp  20613  qustgpopn  20618  qustgplem  20619  qustgphaus  20621  tsmsfbas  20626  ustfilxp  20715  utoptop  20737  utopbas  20738  restutopopn  20741  iducn  20786  cstucnd  20787  ucncn  20788  fmucnd  20795  cfilufg  20796  trcfilu  20797  cfiluweak  20798  neipcfilu  20799  psmetsym  20814  psmetres2  20818  isxmetd  20829  xmetsym  20850  xmetpsmet  20851  imasdsf1olem  20876  imasf1oxmet  20878  xblss2ps  20904  xblss2  20905  xblcntrps  20913  xblcntr  20914  blcld  21008  metustfbasOLD  21068  metustfbas  21069  cfilucfilOLD  21072  cfilucfil  21073  restmetu  21090  ngptgp  21150  tngngpd  21167  tngnrg  21183  nlmvscn  21196  nrginvrcn  21200  nmo0  21242  nmoeq0  21243  nmoid  21249  nghmcn  21252  0nmhm  21262  blcvx  21303  zcld  21318  iccntr  21326  xrge0tsms  21339  xmetdcn2  21342  metdstri  21355  metdscn  21360  rescncf  21401  cncfco  21411  oprpiece1res2  21452  cnheibor  21455  cnllycmp  21456  bndth  21458  evth  21459  ishtpyd  21475  isphtpyd  21486  pcoval2  21516  nmhmcn  21603  ipcn  21686  lmnn  21702  cfilss  21709  iscfil3  21712  cfilfcls  21713  cmetcaulem  21727  iscmet3lem2  21731  cfilres  21735  lmcau  21751  flimcfil  21752  cncmet  21761  rlmbn  21801  minveclem3b  21843  pjthlem1  21852  pjth2  21855  ivthlem3  21865  ovolssnul  21898  ovolctb  21901  ovolunnul  21911  ovoliunnul  21918  ovolsca  21926  ovolicc  21934  ovolicopnf  21935  voliunlem2  21961  voliunlem3  21962  volsup  21966  uniioovol  21988  uniiccvol  21989  dyadmaxlem  22006  vitalilem5  22021  ismbfd  22047  mbfres  22051  mbfss  22053  mbfmulc2re  22055  mbfadd  22068  mbfmulc2  22070  mbflimsup  22073  mbflim  22075  i1faddlem  22100  i1fmullem  22101  mbfmul  22133  itg2itg1  22143  itg2seq  22149  itg2eqa  22152  itg2mulc  22154  itg2split  22156  itg2mono  22160  itg2cnlem1  22168  ibl0  22193  iblposlem  22198  itgreval  22203  iblneg  22209  iblss  22211  iblss2  22212  itgle  22216  iblconst  22224  iblabs  22235  iblabsr  22236  iblmulc2  22237  bddmulibl  22245  limciun  22298  limcun  22299  dvres2lem  22314  dvidlem  22319  dvcnp2  22323  dvcn  22324  cpnres  22340  dvaddbr  22341  dvmulbr  22342  dvcobr  22349  dvcjbr  22352  dvrec  22358  dvcnvlem  22377  dvferm  22389  dvlip2  22396  dveq0  22401  dv11cn  22402  dvivthlem1  22409  lhop1  22415  lhop2  22416  lhop  22417  dvcnvre  22420  dvfsumlem3  22429  dvfsumlem4  22430  dvfsumrlim  22432  dvfsum2  22435  ftc1a  22438  ftc1lem4  22440  ftc1lem6  22442  ftc1  22443  coe1mul3  22500  deg1addle2  22503  deg1add  22504  deg1sublt  22511  deg1mul2  22515  deg1tm  22519  fta1blem  22569  drnguc1p  22571  ig1prsp  22578  plyco0  22589  plyeq0lem  22607  dgrub  22631  dgreq  22641  dgradd2  22665  dgrmul  22667  dgrcolem2  22671  dgrco  22672  plycpn  22685  plydivlem4  22692  plydiveu  22694  vieta1lem2  22707  vieta1  22708  aalioulem2  22729  aalioulem3  22730  aaliou3lem7  22745  tayl0  22757  ulmcn  22794  ulmdvlem3  22797  psercn  22821  abelth  22836  pilem3  22848  efif1olem1  22929  abslogimle  22961  argregt0  22995  argrege0  22996  logf1o2  23031  cxpsqrtlem  23083  cxpcn3  23122  abscxpbnd  23127  ang180lem2  23142  ang180lem3  23143  logreclem  23150  xrlimcnp  23298  harmonicbnd4  23340  fsumharmonic  23341  basellem3  23356  basellem4  23357  dvdsppwf1o  23462  dvdsflf1o  23463  fsumfldivdiaglem  23465  chpeq0  23483  chteq0  23484  chtub  23487  chpub  23495  dchrelbasd  23514  dchrmulcl  23524  dchrinv  23536  bcmono  23552  bposlem1  23559  bposlem2  23560  lgslem1  23571  lgsdirprm  23604  lgsqrlem2  23617  lgsqrlem3  23618  lgsdchr  23623  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem3  23626  lgsquadlem1  23629  2sqlem8  23647  2sqblem  23652  chebbnd1lem1  23654  dchrisumlem1  23674  dchrisumlem2  23675  dchrisumlem3  23676  dchrisum0fno1  23696  pntrmax  23749  pntpbnd1a  23770  pntibndlem3  23777  pntlemn  23785  pntlemi  23789  pntlem3  23794  pntleml  23796  ostth1  23818  ostth2  23822  ostth3  23823  ercgrg  23908  motco  23927  cnvmot  23928  legso  23985  mirmot  24055  lmicom  24154  lmimid  24159  lmimot  24163  hypcgrlem1  24164  hypcgrlem2  24165  ttgcontlem1  24188  brbtwn2  24208  axlowdimlem3  24247  axlowdimlem16  24260  axcontlem8  24274  cusgra0v  24460  cusgraexi  24468  cusgrares  24472  uvtxnb  24497  1pthon  24593  constr2spth  24602  2pthon  24604  usgra2wlkspthlem2  24620  usgra2wlkspth  24621  constr3trllem3  24652  constr3cycl  24661  wlklniswwlkn1  24699  vfwlkniswwlkn  24706  usg2wlkeq2  24709  wwlknred  24723  wwlknredwwlkn0  24727  clwlkisclwwlklem2a1  24779  clwwlkel  24793  wwlkext2clwwlk  24803  clwwnisshclwwn  24809  clwlkf1clwwlk  24850  0egra0rgra  24936  0vgrargra  24937  eupares  24975  eupap1  24976  frgra0v  24993  frgra1v  24998  nvabs  25576  vacn  25604  nmcvcn  25605  nmblore  25701  0lno  25705  0blo  25707  nmlno0lem  25708  occl  26222  pjhthlem1  26309  pjpjpre  26337  nmopre  26789  nmlnop0iALT  26914  nmophmi  26950  leoprf2  27046  stlesi  27160  disjdifprg  27436  fpwrelmap  27556  fzspl  27598  2sqmod  27636  ogrpaddlt  27708  ogrpsublt  27712  pnfinf  27727  xrge0tsmsd  27775  ornglmullt  27797  orngrmullt  27798  orngmullt  27799  ofldlt1  27803  isarchiofld  27807  qtopt1  27838  reff  27842  locfinreflem  27843  metideq  27872  metider  27873  pstmxmet  27876  qqhval2lem  27962  qqhcn  27972  qqhucn  27973  pwsiga  28130  prsiga  28131  measle0  28179  mbfmcst  28230  1stmbfm  28231  2ndmbfm  28232  imambfm  28233  cnmbfm  28234  mbfmco  28235  mbfmco2  28236  sibfof  28282  oddpwdc  28293  eulerpartlemmf  28314  eulerpartlemgs2  28319  0rrv  28390  ballotlemfc0  28431  ballotlemfcc  28432  signstfveq0  28534  lgamgulmlem5  28575  lgambdd  28579  derangen  28616  subfacval3  28633  cvmseu  28721  cvmliftmolem2  28727  cvmliftlem7  28736  cvmliftlem15  28743  cvmlift2lem9a  28748  cvmlift2lem9  28756  cvmlift2lem10  28757  cvmlift2lem11  28758  cvmlift2lem12  28759  cvmlift3lem6  28769  cvmlift3lem8  28771  mclsppslem  28943  mclspps  28944  wsuclem  29381  supaddc  30041  supadd  30042  mblfinlem2  30052  ovoliunnfl  30056  volsupnfl  30059  mbfresfi  30061  dvtanlem  30064  itg2addnclem2  30067  iblabsnc  30079  iblmulc2nc  30080  ftc1cnnclem  30088  ftc1cnnc  30089  ftc1anc  30098  fness  30167  fnetr  30169  fnessref  30175  refssfne  30176  neibastop1  30177  neibastop2  30179  tailfb  30195  filnetlem3  30198  fzadd2  30234  sdclem2  30235  metf1o  30248  ismtyhmeolem  30300  ismtyres  30304  heibor1lem  30305  bfplem2  30319  bfp  30320  rrncmslem  30328  iccbnd  30336  icccmpALT  30337  rngogrphom  30374  rngoisoco  30385  keridl  30429  fzsplit1nn0  30687  icodiamlt  30756  irrapxlem3  30760  irrapxlem4  30761  pell1234qrdich  30797  pell1qr1  30807  pell14qrgap  30811  pellqrexplicit  30813  rmspecfund  30845  fzmaxdif  30919  acongeq  30921  jm2.23  30938  jm3.1  30962  lmhmlnmsplit  31033  hbt  31079  dgrsub2  31084  proot1ex  31161  lcmneg  31209  hashnzfz2  31226  dvconstbi  31239  ubelsupr  31395  lefldiveq  31482  iccintsng  31563  fmul01  31574  fmuldfeq  31577  climsuse  31614  mullimc  31622  limcdm0  31624  limccog  31626  mullimcf  31629  constlimc  31630  idlimc  31632  limcperiod  31634  limsupre  31647  limcleqr  31650  neglimc  31653  addlimc  31654  0ellimcdiv  31655  cncfshift  31676  cncfperiod  31681  cncfuni  31689  icccncfext  31690  cncfiooicclem1  31696  fperdvper  31715  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  mbfres2cn  31757  iblsplit  31765  stoweidlem7  31789  stoweidlem13  31795  stoweidlem26  31808  wallispilem3  31849  stirlinglem6  31861  stirlinglem10  31865  dirkercncf  31889  fourierdlem6  31895  fourierdlem11  31900  fourierdlem12  31901  fourierdlem15  31904  fourierdlem26  31915  fourierdlem42  31931  fourierdlem50  31939  fourierdlem51  31940  fourierdlem52  31941  fourierdlem54  31943  fourierdlem62  31951  fourierdlem79  31968  fourierdlem102  31991  fourierdlem114  32003  etransclem23  32040  rabsubmgmd  32479  submgmid  32481  subsubmgm  32485  mgmhmima  32490  mgmhmeql  32491  isassintop  32534  invid  32571  cicref  32585  2initoinv  32616  2termoinv  32623  rnghmsscmap2  32781  rnghmsscmap  32782  rnghmsubcsetc  32785  zrzeroorngc  32810  rhmsscmap2  32827  rhmsscmap  32828  rhmsubcsetc  32831  rhmsscrnghm  32834  rhmsubcrngc  32837  srhmsubc  32884  fldhmsubc  32892  rhmsubc  32898  srhmsubcOLD  32903  fldhmsubcOLD  32911  rhmsubcOLD  32917  rmfsupp  32967  mndpfsupp  32969  scmfsupp  32971  mptcfsupp  32973  lcoel0  33029  lincsumcl  33032  lincscmcl  33033  lcoss  33037  lindsrng01  33069  lincreslvec3  33083  lindssnlvec  33087  bnj1452  34108  bj-finsumval0  34663  lsmcv2  34754  lsatcv0  34756  lcvexchlem4  34762  lcvexchlem5  34763  l1cvpat  34779  lfl0f  34794  lfladdcl  34796  lflnegcl  34800  lkrlss  34820  eqlkr  34824  lkrlsp  34827  lkrlsp2  34828  lshpkrcl  34841  lkrin  34889  1cvrjat  35199  llni  35232  llnle  35242  lplni  35256  lplnle  35264  llncvrlpln2  35281  2atmat  35285  lvoli  35299  lplncvrlvol2  35339  elpaddri  35526  paddclN  35566  pclclN  35615  pclfinN  35624  0psubclN  35667  1psubclN  35668  atpsubclN  35669  pmapsubclN  35670  osumclN  35691  pexmidN  35693  pexmidlem6N  35699  lhp2lt  35725  lautcnv  35814  idlaut  35820  lautco  35821  idldil  35838  ldilcnv  35839  ldilco  35840  ltrncnv  35870  idltrn  35874  cdleme16d  36006  cdleme50laut  36273  cdleme50ldil  36274  cdleme50ltrn  36283  ltrnco  36445  dian0  36766  dia0eldmN  36767  dia1eldmN  36768  dialss  36773  diaintclN  36785  docaclN  36851  doca2N  36853  djajN  36864  dibintclN  36894  diblss  36897  dicvaddcl  36917  dicvscacl  36918  dicn0  36919  cdlemn11a  36934  dihord2cN  36948  dihord11b  36949  dihord6apre  36983  dihmeetlem1N  37017  dihglblem5apreN  37018  dihpN  37063  dihjatcclem4  37148  dochkr1  37205  islpoldN  37211  lcfrlem31  37300  mapdpglem18  37416  mapdheq2  37456  mapdheq4  37459  mapdh6aN  37462  hdmap1l6a  37537  hdmap1neglem1N  37555  hdmap14lem4a  37601
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 185  df-an 371
  Copyright terms: Public domain W3C validator