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

Theorem mpbir2and 938
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  |-  ( ph  ->  ch )
mpbir2and.2  |-  ( ph  ->  th )
mpbir2and.3  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
Assertion
Ref Expression
mpbir2and  |-  ( ph  ->  ps )

Proof of Theorem mpbir2and
StepHypRef Expression
1 mpbir2and.1 . . 3  |-  ( ph  ->  ch )
2 mpbir2and.2 . . 3  |-  ( ph  ->  th )
31, 2jca 539 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 240 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  fveqressseq  6041  fmptsng  6109  fmptsnd  6110  fnprb  6147  fntpb  6148  fdmfifsupp  7919  fczfsuppd  7927  fsuppmptif  7939  fsuppco2  7942  fsuppcor  7943  dffi3  7971  supmaxOLD  8009  suppr  8013  infpr  8045  ordtypelem7  8065  cantnf0  8206  cantnfp1lem1  8209  cantnfp1lem2  8210  cantnfp1lem3  8211  cantnflem1a  8216  cantnflem1d  8219  cantnflem1  8220  cantnf  8224  rankpwi  8320  carduni  8441  fin23lem32  8800  fpwwe2lem6  9086  fpwwe2lem9  9089  fpwwe2lem12  9092  fpwwe2lem13  9093  fpwwe2  9094  inttsk  9225  grutsk1  9272  add20  10154  supaddc  10602  supadd  10603  supmul  10607  suprzcl  11044  uzwo3  11288  rpnnen1lem5  11323  xrre  11493  xrre3  11495  xleadd1a  11568  xlemul1a  11603  supxrre  11642  infmxrreOLD  11655  ixxub  11685  ixxlbOLD  11687  elioc2  11726  elico2  11727  elicc2  11728  elfz1eq  11839  fznatpl1  11879  nn0fz0  11919  fzctr  11933  fzo1fzo0n0  11988  fzoaddel  11998  elincfzoext  12003  flid  12076  flval3  12082  fladdz  12090  fldiv  12119  modid  12153  seqf1olem1  12284  bcval5  12535  hashf1lem1  12651  eqs1  12786  wwlktovf1  13081  sqeqd  13278  sqrlem7  13361  max0add  13422  abs2difabs  13446  rddif  13452  fzomaxdiflem  13454  rexico  13465  icodiamlt  13546  limsupgre  13591  limsupgreOLD  13592  rlim3  13611  icco1  13653  rlimclim  13659  rlimuni  13663  rlimresb  13678  isercolllem2  13778  isercolllem3  13779  isercoll  13780  caucvgrlem  13785  caucvgrlemOLD  13786  caurcvgr  13787  caurcvgrOLD  13788  iseraltlem3  13799  fsum00  13907  o1fsum  13922  dvdseq  14401  bitsfzolem  14456  bitsfzolemOLD  14457  bitsfzo  14458  bitsmod  14459  bitscmp  14461  gcd0id  14536  gcdneg  14539  bezoutlem4OLD  14555  bezoutlem4  14558  nn0seqcvgd  14578  lcmneg  14617  prmind2  14684  isprm5  14700  qredeq  14712  hashdvds  14772  eulerthlem2  14779  pcpremul  14842  pcidlem  14870  pcgcd1  14875  pcadd2  14884  fldivp1  14891  pcfaclem  14892  prmreclem5  14913  4sqlem17OLD  14954  4sqlem17  14960  vdwlem1  14980  vdwlem6  14985  vdwlem12  14991  vdwlem13  14992  0ram  15027  ram0  15029  ramub1lem1  15033  invco  15725  sectmon  15736  monsect  15737  invid  15741  cicref  15755  ssctr  15779  ssceq  15780  0ssc  15791  0subcat  15792  catsubcat  15793  issubc3  15803  fullsubc  15804  funcinv  15827  fthmon  15881  fuccocl  15918  fucidcl  15919  invfuc  15928  2initoinv  15954  2termoinv  15961  elhomai  15977  setcmon  16031  setcepi  16032  catcisolem  16050  curf2cl  16165  yonedalem4c  16211  yonedalem3  16214  yoniso  16219  lublecl  16284  isacs3lem  16461  tsrdir  16533  mnd1  16626  mnd1OLD  16627  sgrp2nmndlem4  16711  sgrp2nmndlem5  16712  nmznsg  16910  ghmpreima  16953  ghmeql  16954  ghmnsgpreima  16956  cntzsubm  17038  cntzsubg  17039  cntzmhm  17041  symgextfo  17112  symgfixf1  17127  symgfixfolem1  17128  odlem2  17237  odlem2OLD  17253  gexlem2  17282  gexlem2OLD  17285  gexcl2  17290  sylow1lem5  17303  subgslw  17317  slwhash  17325  fislw  17326  sylow3lem1  17328  lsmsubg  17355  efgredlemd  17443  efgredlem  17446  efgcpbllemb  17454  frgpuplem  17471  cyggeninv  17567  iscygd  17571  iscygodd  17572  gsumzadd  17604  gsumconst  17616  gsumpt  17643  gsum2dlem2  17652  gsum2d  17653  gsum2d2lem  17654  dprdfcntz  17697  eldprdi  17700  subgdmdprd  17716  subgdprd  17717  dprdpr  17732  ablfac1c  17753  ablfac1eu  17755  ablfaclem3  17769  ring1  17879  kerf1hrm  18020  issubdrg  18082  rhmeql  18087  rhmima  18088  cntzsubr  18089  isabvd  18097  abvdiv  18114  lsslsp  18287  lmhmima  18319  lmhmpreima  18320  lmhmeql  18327  lsmcl  18355  lspfixed  18400  issubassa  18597  issubassa2  18618  snifpsrbag  18639  psrbaglesupp  18641  psrbaglecl  18642  psrbagaddcl  18643  psrbagcon  18644  mplsubglem  18707  mpllsslem  18708  mplassa  18727  subrgmpl  18733  mplcoe5  18741  mplbas2  18743  mplind  18774  evlslem3  18786  mpfind  18808  ply1assa  18841  coe1tmmul2  18918  coe1tmmul  18919  cply1coe0bi  18943  qsssubdrg  19076  gzrngunit  19082  evpmodpmf1o  19213  ocvpj  19329  dsmm0cl  19352  dsmmacl  19353  dsmmsubg  19355  dsmmlss  19356  frlmsplit2  19380  uvcff  19398  lindfrn  19428  f1lindf  19429  lindsss  19431  mat1rngiso  19560  dmatid  19569  dmatsubcl  19572  dmatscmcl  19577  scmatid  19588  scmataddcl  19590  scmatsubcl  19591  scmatmulcl  19592  smatvscl  19598  scmatrhmcl  19602  scmatrngiso  19610  mat0scmat  19612  mat1scmat  19613  mdet0pr  19666  m2cpmrngiso  19831  pm2mprngiso  19895  chmaidscmat  19921  fvmptnn04if  19922  distop  20060  indistopon  20065  ppttop  20071  epttop  20073  mretopd  20157  toponmre  20158  neiss  20174  opnneissb  20179  ssnei2  20181  innei  20190  neiptoptop  20196  ordtcld1  20262  ordtcld2  20263  lmconst  20326  cnpnei  20329  iscncl  20334  cnss1  20341  cnss2  20342  cncnpi  20343  cncnp  20345  cnconst2  20348  cnrest  20350  cnpresti  20353  cnpdis  20358  paste  20359  lmcnp  20369  cnhaus  20419  hauscmp  20471  2ndcomap  20522  1stcelcls  20525  1stccnp  20526  llyrest  20549  nllyrest  20550  llyidm  20552  nllyidm  20553  ssref  20576  reftr  20578  refun0  20579  dissnref  20592  kgentopon  20602  kgenidm  20611  kgencn3  20622  txcld  20667  neitx  20671  tx1cn  20673  tx2cn  20674  ptcld  20677  xkoccn  20683  txcnp  20684  ptcnp  20686  txcnmpt  20688  ptcn  20691  txdis1cn  20699  ptrescn  20703  txkgen  20716  xkoco1cn  20721  xkoco2cn  20722  xkococn  20724  xkoinjcn  20751  qtoptop2  20763  qtopuni  20766  qtopid  20769  qtopkgen  20774  basqtop  20775  tgqtop  20776  qtopss  20779  qtopeu  20780  qtoprest  20781  kqopn  20798  kqcld  20799  kqreglem2  20806  reghmph  20857  ordthmeolem  20865  qtopf1  20880  opnfbas  20906  isfil2  20920  fbasweak  20929  fsubbas  20931  filcon  20947  fbasrn  20948  rnelfmlem  21016  flimss2  21036  flimss1  21037  hausflim  21045  flimclslem  21048  flimsncls  21050  cnpflfi  21063  flfcnp2  21071  fclsfnflim  21091  cnextfvval  21129  cnextfres1  21132  symgtgp  21165  opnsubg  21171  ghmcnp  21178  qustgpopn  21183  qustgplem  21184  qustgphaus  21186  tsmsfbas  21191  ustfilxp  21276  utoptop  21298  utopbas  21299  restutopopn  21302  iducn  21347  cstucnd  21348  ucncn  21349  fmucnd  21356  cfilufg  21357  trcfilu  21358  cfiluweak  21359  neipcfilu  21360  psmetsym  21375  psmetres2  21379  isxmetd  21390  xmetsym  21411  xmetpsmet  21412  imasf1oxmet  21439  xblss2ps  21465  xblss2  21466  xblcntrps  21474  xblcntr  21475  blcld  21569  metustfbas  21621  cfilucfil  21623  restmetu  21634  ngptgp  21693  tngngpd  21710  tngnrg  21726  nlmvscn  21739  nrginvrcn  21743  nmo0  21805  nmoeq0  21806  nmoid  21812  nghmcn  21815  0nmhm  21825  blcvx  21865  zcld  21880  iccntr  21888  xrge0tsms  21901  xmetdcn2  21904  metdstri  21917  metdscn  21922  metdstriOLD  21932  metdscnOLD  21937  rescncf  21978  cncfco  21988  oprpiece1res2  22029  cnheibor  22032  cnllycmp  22033  bndth  22035  evth  22036  ishtpyd  22055  isphtpyd  22066  pcoval2  22096  nmhmcn  22183  ipcn  22266  lmnn  22282  cfilss  22289  iscfil3  22292  cfilfcls  22293  cmetcaulem  22307  iscmet3lem2  22311  cfilres  22315  lmcau  22331  flimcfil  22332  cncmet  22339  rlmbn  22377  minveclem3b  22419  minveclem3bOLD  22431  pjthlem1  22440  pjth2  22443  ivthlem3  22453  ovolssnul  22489  ovolctb  22492  ovolunnul  22502  ovoliunnul  22509  ovolsca  22517  ovolicc  22526  ovolicopnf  22527  voliunlem2  22553  voliunlem3  22554  volsup  22558  uniioovol  22585  uniiccvol  22586  dyadmaxlem  22604  vitalilem5  22619  ismbfd  22645  mbfres  22649  mbfss  22651  mbfmulc2re  22653  mbfadd  22666  mbfmulc2  22668  mbflimsupOLD  22673  mbflim  22675  i1faddlem  22700  i1fmullem  22701  mbfmul  22733  itg2itg1  22743  itg2seq  22749  itg2eqa  22752  itg2mulc  22754  itg2split  22756  itg2mono  22760  itg2cnlem1  22768  ibl0  22793  iblposlem  22798  itgreval  22803  iblneg  22809  iblss  22811  iblss2  22812  itgle  22816  iblconst  22824  iblabs  22835  iblabsr  22836  iblmulc2  22837  bddmulibl  22845  limciun  22898  limcun  22899  dvres2lem  22914  dvidlem  22919  dvcnp2  22923  dvcn  22924  cpnres  22940  dvaddbr  22941  dvmulbr  22942  dvcobr  22949  dvcjbr  22952  dvrec  22958  dvcnvlem  22977  dvferm  22989  dvlip2  22996  dveq0  23001  dv11cn  23002  dvivthlem1  23009  lhop1  23015  lhop2  23016  lhop  23017  dvcnvre  23020  dvfsumlem3  23029  dvfsumlem4  23030  dvfsumrlim  23032  dvfsum2  23035  ftc1a  23038  ftc1lem4  23040  ftc1lem6  23042  ftc1  23043  coe1mul3  23097  deg1addle2  23100  deg1add  23101  deg1sublt  23108  deg1mul2  23112  deg1tm  23116  fta1blem  23168  drnguc1p  23170  ig1prsp  23178  ig1prspOLD  23184  plyco0  23195  plyeq0lem  23213  dgrub  23237  dgreq  23247  dgradd2  23271  dgrmul  23273  dgrcolem2  23277  dgrco  23278  plycpn  23291  plydivlem4  23298  plydiveu  23300  vieta1lem2  23313  vieta1  23314  aalioulem2  23338  aalioulem3  23339  aaliou3lem7  23354  tayl0  23366  ulmcn  23403  ulmdvlem3  23406  psercn  23430  abelth  23445  pilem3  23458  pilem3OLD  23459  efif1olem1  23540  abslogimle  23572  argregt0  23608  argrege0  23609  logf1o2  23644  cxpsqrtlem  23696  cxpcn3  23737  abscxpbnd  23742  logreclem  23748  ang180lem2  23788  ang180lem3  23789  xrlimcnp  23943  harmonicbnd4  23985  fsumharmonic  23986  lgamgulmlem5  24007  lgambdd  24011  basellem3  24058  basellem4  24059  dvdsppwf1o  24164  dvdsflf1o  24165  fsumfldivdiaglem  24167  chpeq0  24185  chteq0  24186  chtub  24189  chpub  24197  dchrelbasd  24216  dchrmulcl  24226  dchrinv  24238  bcmono  24254  bposlem1  24261  bposlem2  24262  lgslem1  24273  lgsdirprm  24306  lgsqrlem2  24319  lgsqrlem3  24320  lgsdchr  24325  lgseisenlem1  24326  lgseisenlem2  24327  lgseisenlem3  24328  lgsquadlem1  24331  2sqlem8  24349  2sqblem  24354  chebbnd1lem1  24356  dchrisumlem1  24376  dchrisumlem2  24377  dchrisumlem3  24378  dchrisum0fno1  24398  pntrmax  24451  pntpbnd1a  24472  pntibndlem3  24479  pntlemn  24487  pntlemi  24491  pntlem3  24496  pntleml  24498  ostth1  24520  ostth2  24524  ostth3  24525  ercgrg  24611  motco  24634  cnvmot  24635  legso  24693  mirmot  24769  lmicom  24879  lmimid  24885  lmimot  24889  hypcgrlem1  24890  hypcgrlem2  24891  ttgcontlem1  24964  brbtwn2  24984  axlowdimlem3  25023  axlowdimlem16  25036  axcontlem8  25050  cusgra0v  25237  cusgraexi  25245  cusgrares  25249  uvtxnb  25274  1pthon  25370  constr2spth  25379  2pthon  25381  usgra2wlkspthlem2  25397  usgra2wlkspth  25398  constr3trllem3  25429  constr3cycl  25438  wlklniswwlkn1  25476  vfwlkniswwlkn  25483  usg2wlkeq2  25486  wwlknred  25500  wwlknredwwlkn0  25504  clwlkisclwwlklem2a1  25556  clwwlkel  25570  wwlkext2clwwlk  25580  clwwnisshclwwn  25586  clwlkf1clwwlk  25627  0egra0rgra  25713  0vgrargra  25714  eupares  25752  eupap1  25753  frgra0v  25770  frgra1v  25775  nvabs  26351  vacn  26379  nmcvcn  26380  nmblore  26476  0lno  26480  0blo  26482  nmlno0lem  26483  occl  27006  pjhthlem1  27093  pjpjpre  27121  nmopre  27572  nmlnop0iALT  27697  nmophmi  27733  leoprf2  27829  stlesi  27943  disjdifprg  28234  fpwrelmap  28367  fzspl  28417  2sqmod  28458  ogrpaddlt  28530  ogrpsublt  28534  pnfinf  28549  xrge0tsmsd  28597  ornglmullt  28619  orngrmullt  28620  orngmullt  28621  ofldlt1  28625  isarchiofld  28629  psgnfzto1stlem  28662  fzto1st1  28664  qtopt1  28711  reff  28715  locfinreflem  28716  metideq  28745  metider  28746  pstmxmet  28749  qqhval2lem  28834  qqhcn  28844  qqhucn  28845  pwsiga  29001  prsiga  29002  measle0  29079  mbfmcst  29130  1stmbfm  29131  2ndmbfm  29132  imambfm  29133  cnmbfm  29134  mbfmco  29135  mbfmco2  29136  carsgclctun  29202  sibfof  29222  oddpwdc  29236  eulerpartlemmf  29257  eulerpartlemgs2  29262  0rrv  29333  ballotlemfc0  29374  ballotlemfcc  29375  signstfveq0  29515  bnj1452  29910  derangen  29944  subfacval3  29961  cvmseu  30048  cvmliftmolem2  30054  cvmliftlem7  30063  cvmliftlem15  30070  cvmlift2lem9a  30075  cvmlift2lem9  30083  cvmlift2lem10  30084  cvmlift2lem11  30085  cvmlift2lem12  30086  cvmlift3lem6  30096  cvmlift3lem8  30098  mclsppslem  30270  mclspps  30271  wsuclem  30557  nosepon  30605  fness  31054  fnetr  31056  fnessref  31062  refssfne  31063  neibastop1  31064  neibastop2  31066  tailfb  31082  filnetlem3  31085  bj-finsumval0  31747  poimirlem13  31998  poimirlem15  32000  poimirlem17  32002  poimirlem24  32009  poimirlem28  32013  mblfinlem2  32023  ovoliunnfl  32027  volsupnfl  32030  mbfresfi  32032  dvtanlemOLD  32036  itg2addnclem2  32039  iblabsnc  32051  iblmulc2nc  32052  ftc1cnnclem  32060  ftc1cnnc  32061  ftc1anc  32070  fzadd2  32115  sdclem2  32116  metf1o  32129  ismtyhmeolem  32181  ismtyres  32185  heibor1lem  32186  bfplem2  32200  bfp  32201  rrncmslem  32209  iccbnd  32217  icccmpALT  32218  rngogrphom  32255  rngoisoco  32266  keridl  32310  lsmcv2  32640  lsatcv0  32642  lcvexchlem4  32648  lcvexchlem5  32649  l1cvpat  32665  lfl0f  32680  lfladdcl  32682  lflnegcl  32686  lkrlss  32706  eqlkr  32710  lkrlsp  32713  lkrlsp2  32714  lshpkrcl  32727  lkrin  32775  1cvrjat  33085  llni  33118  llnle  33128  lplni  33142  lplnle  33150  llncvrlpln2  33167  2atmat  33171  lvoli  33185  lplncvrlvol2  33225  elpaddri  33412  paddclN  33452  pclclN  33501  pclfinN  33510  0psubclN  33553  1psubclN  33554  atpsubclN  33555  pmapsubclN  33556  osumclN  33577  pexmidN  33579  pexmidlem6N  33585  lhp2lt  33611  lautcnv  33700  idlaut  33706  lautco  33707  idldil  33724  ldilcnv  33725  ldilco  33726  ltrncnv  33756  idltrn  33760  cdleme16d  33892  cdleme50laut  34159  cdleme50ldil  34160  cdleme50ltrn  34169  ltrnco  34331  dian0  34652  dia0eldmN  34653  dia1eldmN  34654  dialss  34659  diaintclN  34671  docaclN  34737  doca2N  34739  djajN  34750  dibintclN  34780  diblss  34783  dicvaddcl  34803  dicvscacl  34804  dicn0  34805  cdlemn11a  34820  dihord2cN  34834  dihord11b  34835  dihord6apre  34869  dihmeetlem1N  34903  dihglblem5apreN  34904  dihpN  34949  dihjatcclem4  35034  dochkr1  35091  islpoldN  35097  lcfrlem31  35186  mapdpglem18  35302  mapdheq2  35342  mapdheq4  35345  mapdh6aN  35348  hdmap1l6a  35423  hdmap1neglem1N  35441  hdmap14lem4a  35487  fzsplit1nn0  35641  irrapxlem3  35713  irrapxlem4  35714  pell1234qrdich  35752  pell1qr1  35762  pell14qrgap  35766  pellqrexplicit  35768  rmspecfund  35802  fzmaxdif  35876  acongeq  35878  jm2.23  35896  jm3.1  35920  lmhmlnmsplit  35990  hbt  36034  dgrsub2  36039  proot1ex  36123  clublem  36262  dftrcl3  36357  hashnzfz2  36714  dvconstbi  36727  ubelsupr  37381  lefldiveq  37544  iccintsng  37662  fmul01  37696  fmuldfeq  37699  climsuse  37725  mullimc  37734  limcdm0  37736  limccog  37738  mullimcf  37741  constlimc  37742  idlimc  37744  limcperiod  37746  limsupre  37759  limsupreOLD  37760  limcleqr  37763  neglimc  37766  addlimc  37767  0ellimcdiv  37768  cncfshift  37789  cncfperiod  37794  cncfuni  37802  icccncfext  37803  cncfiooicclem1  37809  fperdvper  37828  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  mbfres2cn  37873  iblsplit  37881  stoweidlem7  37905  stoweidlem13  37911  stoweidlem26  37924  wallispilem3  37967  stirlinglem6  37979  stirlinglem10  37983  dirkercncf  38007  fourierdlem6  38013  fourierdlem11  38018  fourierdlem12  38019  fourierdlem15  38022  fourierdlem26  38033  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem50  38058  fourierdlem51  38059  fourierdlem52  38060  fourierdlem54  38062  fourierdlem62  38070  fourierdlem79  38087  fourierdlem102  38110  fourierdlem114  38122  etransclem23  38160  zgeltp1eq  38755  iccpartres  38770  pfx2  38993  pfxccatin12d  39013  repswpfx  39017  fusgrfis  39446  nbgr2vtx1edg  39468  uvtxnbgrb  39524  cplgr1v  39547  0vtxrgr  39642  0vtxrusgr  39643  ewlkle  39672  1wlk1ewlk  39698  trlOntrl  39746  pthOnpth  39780  uhgr1wlkspth  39787  usgr2wlkspth  39791  pthdlem2  39794  0TrlOn  39840  0pthon-av  39843  1trld  39857  1pthond  39859  lp1cycl  39867  2trld  39887  2trlond  39888  2spthd  39890  2pthond  39891  3trld  39913  3trlond  39914  3pthond  39916  3spthd  39917  3spthond  39918  3cycld  39919  rabsubmgmd  40064  submgmid  40066  subsubmgm  40070  mgmhmima  40075  mgmhmeql  40076  isassintop  40119  rnghmsscmap2  40248  rnghmsscmap  40249  rnghmsubcsetc  40252  zrzeroorngc  40277  rhmsscmap2  40294  rhmsscmap  40295  rhmsubcsetc  40298  rhmsscrnghm  40301  rhmsubcrngc  40304  srhmsubc  40351  fldhmsubc  40359  rhmsubc  40365  srhmsubcALTV  40370  fldhmsubcALTV  40378  rhmsubcALTV  40384  rmfsupp  40432  mndpfsupp  40434  scmfsupp  40436  mptcfsupp  40438  lcoel0  40494  lincsumcl  40497  lincscmcl  40498  lcoss  40502  lindsrng01  40534  lincreslvec3  40548  lindssnlvec  40552  zgtp1leeq  40592
  Copyright terms: Public domain W3C validator