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

Theorem mpbir2and 930
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 534 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 235 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  fveqressseq  5972  fmptsng  6039  fmptsnd  6040  fnprb  6077  fdmfifsupp  7841  fczfsuppd  7849  fsuppmptif  7861  fsuppco2  7864  fsuppcor  7865  dffi3  7893  supmaxOLD  7931  suppr  7935  infpr  7967  ordtypelem7  7987  cantnf0  8127  cantnfp1lem1  8130  cantnfp1lem2  8131  cantnfp1lem3  8132  cantnflem1a  8137  cantnflem1d  8140  cantnflem1  8141  cantnf  8145  rankpwi  8241  carduni  8362  fin23lem32  8720  fpwwe2lem6  9006  fpwwe2lem9  9009  fpwwe2lem12  9012  fpwwe2lem13  9013  fpwwe2  9014  inttsk  9145  grutsk1  9192  add20  10072  supaddc  10520  supadd  10521  supmul  10525  suprzcl  10961  uzwo3  11205  rpnnen1lem5  11240  xrre  11410  xrre3  11412  xleadd1a  11485  xlemul1a  11520  supxrre  11559  infmxrreOLD  11572  ixxub  11602  ixxlbOLD  11604  elioc2  11643  elico2  11644  elicc2  11645  elfz1eq  11756  fznatpl1  11796  nn0fz0  11836  fzctr  11849  fzo1fzo0n0  11903  fzoaddel  11912  elincfzoext  11917  flid  11989  flval3  11995  fladdz  12003  fldiv  12032  modid  12066  seqf1olem1  12197  bcval5  12448  hashf1lem1  12561  eqs1  12691  wwlktovf1  12971  sqeqd  13168  sqrlem7  13251  max0add  13312  abs2difabs  13336  rddif  13342  fzomaxdiflem  13344  rexico  13355  limsupgre  13480  limsupgreOLD  13481  rlim3  13500  icco1  13542  rlimclim  13548  rlimuni  13552  rlimresb  13567  isercolllem2  13667  isercolllem3  13668  isercoll  13669  caucvgrlem  13674  caucvgrlemOLD  13675  caurcvgr  13676  caurcvgrOLD  13677  iseraltlem3  13688  fsum00  13796  o1fsum  13811  dvdseq  14290  bitsfzolem  14345  bitsfzolemOLD  14346  bitsfzo  14347  bitsmod  14348  bitscmp  14350  gcd0id  14425  gcdneg  14428  bezoutlem4OLD  14444  bezoutlem4  14447  nn0seqcvgd  14467  lcmneg  14506  prmind2  14573  isprm5  14589  qredeq  14601  hashdvds  14661  eulerthlem2  14668  pcpremul  14731  pcidlem  14759  pcgcd1  14764  pcadd2  14773  fldivp1  14780  pcfaclem  14781  prmreclem5  14802  4sqlem17OLD  14843  4sqlem17  14849  vdwlem1  14869  vdwlem6  14874  vdwlem12  14880  vdwlem13  14881  0ram  14916  ram0  14918  ramub1lem1  14922  invco  15614  sectmon  15625  monsect  15626  invid  15630  cicref  15644  ssctr  15668  ssceq  15669  0ssc  15680  0subcat  15681  catsubcat  15682  issubc3  15692  fullsubc  15693  funcinv  15716  fthmon  15770  fuccocl  15807  fucidcl  15808  invfuc  15817  2initoinv  15843  2termoinv  15850  elhomai  15866  setcmon  15920  setcepi  15921  catcisolem  15939  curf2cl  16054  yonedalem4c  16100  yonedalem3  16103  yoniso  16108  lublecl  16173  isacs3lem  16350  tsrdir  16422  mnd1  16515  mnd1OLD  16516  sgrp2nmndlem4  16600  sgrp2nmndlem5  16601  nmznsg  16799  ghmpreima  16842  ghmeql  16843  ghmnsgpreima  16845  cntzsubm  16927  cntzsubg  16928  cntzmhm  16930  symgextfo  17001  symgfixf1  17016  symgfixfolem1  17017  odlem2  17126  odlem2OLD  17142  gexlem2  17171  gexlem2OLD  17174  gexcl2  17179  sylow1lem5  17192  subgslw  17206  slwhash  17214  fislw  17215  sylow3lem1  17217  lsmsubg  17244  efgredlemd  17332  efgredlem  17335  efgcpbllemb  17343  frgpuplem  17360  cyggeninv  17456  iscygd  17460  iscygodd  17461  gsumzadd  17493  gsumconst  17505  gsumpt  17532  gsum2dlem2  17541  gsum2d  17542  gsum2d2lem  17543  dprdfcntz  17586  eldprdi  17589  subgdmdprd  17605  subgdprd  17606  dprdpr  17621  ablfac1c  17642  ablfac1eu  17644  ablfaclem3  17658  ring1  17768  kerf1hrm  17909  issubdrg  17971  rhmeql  17976  rhmima  17977  cntzsubr  17978  isabvd  17986  abvdiv  18003  lsslsp  18176  lmhmima  18208  lmhmpreima  18209  lmhmeql  18216  lsmcl  18244  lspfixed  18289  issubassa  18486  issubassa2  18507  snifpsrbag  18528  psrbaglesupp  18530  psrbaglecl  18531  psrbagaddcl  18532  psrbagcon  18533  mplsubglem  18596  mpllsslem  18597  mplassa  18616  subrgmpl  18622  mplcoe5  18630  mplbas2  18632  mplind  18663  evlslem3  18675  mpfind  18697  ply1assa  18730  coe1tmmul2  18807  coe1tmmul  18808  cply1coe0bi  18832  qsssubdrg  18965  gzrngunit  18971  evpmodpmf1o  19101  ocvpj  19217  dsmm0cl  19240  dsmmacl  19241  dsmmsubg  19243  dsmmlss  19244  frlmsplit2  19268  uvcff  19286  lindfrn  19316  f1lindf  19317  lindsss  19319  mat1rngiso  19448  dmatid  19457  dmatsubcl  19460  dmatscmcl  19465  scmatid  19476  scmataddcl  19478  scmatsubcl  19479  scmatmulcl  19480  smatvscl  19486  scmatrhmcl  19490  scmatrngiso  19498  mat0scmat  19500  mat1scmat  19501  mdet0pr  19554  m2cpmrngiso  19719  pm2mprngiso  19783  chmaidscmat  19809  fvmptnn04if  19810  distop  19948  indistopon  19953  ppttop  19959  epttop  19961  mretopd  20045  toponmre  20046  neiss  20062  opnneissb  20067  ssnei2  20069  innei  20078  neiptoptop  20084  ordtcld1  20150  ordtcld2  20151  lmconst  20214  cnpnei  20217  iscncl  20222  cnss1  20229  cnss2  20230  cncnpi  20231  cncnp  20233  cnconst2  20236  cnrest  20238  cnpresti  20241  cnpdis  20246  paste  20247  lmcnp  20257  cnhaus  20307  hauscmp  20359  2ndcomap  20410  1stcelcls  20413  1stccnp  20414  llyrest  20437  nllyrest  20438  llyidm  20440  nllyidm  20441  ssref  20464  reftr  20466  refun0  20467  dissnref  20480  kgentopon  20490  kgenidm  20499  kgencn3  20510  txcld  20555  neitx  20559  tx1cn  20561  tx2cn  20562  ptcld  20565  xkoccn  20571  txcnp  20572  ptcnp  20574  txcnmpt  20576  ptcn  20579  txdis1cn  20587  ptrescn  20591  txkgen  20604  xkoco1cn  20609  xkoco2cn  20610  xkococn  20612  xkoinjcn  20639  qtoptop2  20651  qtopuni  20654  qtopid  20657  qtopkgen  20662  basqtop  20663  tgqtop  20664  qtopss  20667  qtopeu  20668  qtoprest  20669  kqopn  20686  kqcld  20687  kqreglem2  20694  reghmph  20745  ordthmeolem  20753  qtopf1  20768  opnfbas  20794  isfil2  20808  fbasweak  20817  fsubbas  20819  filcon  20835  fbasrn  20836  rnelfmlem  20904  flimss2  20924  flimss1  20925  hausflim  20933  flimclslem  20936  flimsncls  20938  cnpflfi  20951  flfcnp2  20959  fclsfnflim  20979  cnextfvval  21017  cnextfres1  21020  symgtgp  21053  opnsubg  21059  ghmcnp  21066  qustgpopn  21071  qustgplem  21072  qustgphaus  21074  tsmsfbas  21079  ustfilxp  21164  utoptop  21186  utopbas  21187  restutopopn  21190  iducn  21235  cstucnd  21236  ucncn  21237  fmucnd  21244  cfilufg  21245  trcfilu  21246  cfiluweak  21247  neipcfilu  21248  psmetsym  21263  psmetres2  21267  isxmetd  21278  xmetsym  21299  xmetpsmet  21300  imasf1oxmet  21327  xblss2ps  21353  xblss2  21354  xblcntrps  21362  xblcntr  21363  blcld  21457  metustfbas  21509  cfilucfil  21511  restmetu  21522  ngptgp  21581  tngngpd  21598  tngnrg  21614  nlmvscn  21627  nrginvrcn  21631  nmo0  21693  nmoeq0  21694  nmoid  21700  nghmcn  21703  0nmhm  21713  blcvx  21753  zcld  21768  iccntr  21776  xrge0tsms  21789  xmetdcn2  21792  metdstri  21805  metdscn  21810  metdstriOLD  21820  metdscnOLD  21825  rescncf  21866  cncfco  21876  oprpiece1res2  21917  cnheibor  21920  cnllycmp  21921  bndth  21923  evth  21924  ishtpyd  21943  isphtpyd  21954  pcoval2  21984  nmhmcn  22071  ipcn  22154  lmnn  22170  cfilss  22177  iscfil3  22180  cfilfcls  22181  cmetcaulem  22195  iscmet3lem2  22199  cfilres  22203  lmcau  22219  flimcfil  22220  cncmet  22227  rlmbn  22265  minveclem3b  22307  minveclem3bOLD  22319  pjthlem1  22328  pjth2  22331  ivthlem3  22341  ovolssnul  22377  ovolctb  22380  ovolunnul  22390  ovoliunnul  22397  ovolsca  22405  ovolicc  22414  ovolicopnf  22415  voliunlem2  22441  voliunlem3  22442  volsup  22446  uniioovol  22473  uniiccvol  22474  dyadmaxlem  22492  vitalilem5  22507  ismbfd  22533  mbfres  22537  mbfss  22539  mbfmulc2re  22541  mbfadd  22554  mbfmulc2  22556  mbflimsupOLD  22561  mbflim  22563  i1faddlem  22588  i1fmullem  22589  mbfmul  22621  itg2itg1  22631  itg2seq  22637  itg2eqa  22640  itg2mulc  22642  itg2split  22644  itg2mono  22648  itg2cnlem1  22656  ibl0  22681  iblposlem  22686  itgreval  22691  iblneg  22697  iblss  22699  iblss2  22700  itgle  22704  iblconst  22712  iblabs  22723  iblabsr  22724  iblmulc2  22725  bddmulibl  22733  limciun  22786  limcun  22787  dvres2lem  22802  dvidlem  22807  dvcnp2  22811  dvcn  22812  cpnres  22828  dvaddbr  22829  dvmulbr  22830  dvcobr  22837  dvcjbr  22840  dvrec  22846  dvcnvlem  22865  dvferm  22877  dvlip2  22884  dveq0  22889  dv11cn  22890  dvivthlem1  22897  lhop1  22903  lhop2  22904  lhop  22905  dvcnvre  22908  dvfsumlem3  22917  dvfsumlem4  22918  dvfsumrlim  22920  dvfsum2  22923  ftc1a  22926  ftc1lem4  22928  ftc1lem6  22930  ftc1  22931  coe1mul3  22985  deg1addle2  22988  deg1add  22989  deg1sublt  22996  deg1mul2  23000  deg1tm  23004  fta1blem  23056  drnguc1p  23058  ig1prsp  23066  ig1prspOLD  23072  plyco0  23083  plyeq0lem  23101  dgrub  23125  dgreq  23135  dgradd2  23159  dgrmul  23161  dgrcolem2  23165  dgrco  23166  plycpn  23179  plydivlem4  23186  plydiveu  23188  vieta1lem2  23201  vieta1  23202  aalioulem2  23226  aalioulem3  23227  aaliou3lem7  23242  tayl0  23254  ulmcn  23291  ulmdvlem3  23294  psercn  23318  abelth  23333  pilem3  23346  pilem3OLD  23347  efif1olem1  23428  abslogimle  23460  argregt0  23496  argrege0  23497  logf1o2  23532  cxpsqrtlem  23584  cxpcn3  23625  abscxpbnd  23630  logreclem  23636  ang180lem2  23676  ang180lem3  23677  xrlimcnp  23831  harmonicbnd4  23873  fsumharmonic  23874  lgamgulmlem5  23895  lgambdd  23899  basellem3  23946  basellem4  23947  dvdsppwf1o  24052  dvdsflf1o  24053  fsumfldivdiaglem  24055  chpeq0  24073  chteq0  24074  chtub  24077  chpub  24085  dchrelbasd  24104  dchrmulcl  24114  dchrinv  24126  bcmono  24142  bposlem1  24149  bposlem2  24150  lgslem1  24161  lgsdirprm  24194  lgsqrlem2  24207  lgsqrlem3  24208  lgsdchr  24213  lgseisenlem1  24214  lgseisenlem2  24215  lgseisenlem3  24216  lgsquadlem1  24219  2sqlem8  24237  2sqblem  24242  chebbnd1lem1  24244  dchrisumlem1  24264  dchrisumlem2  24265  dchrisumlem3  24266  dchrisum0fno1  24286  pntrmax  24339  pntpbnd1a  24360  pntibndlem3  24367  pntlemn  24375  pntlemi  24379  pntlem3  24384  pntleml  24386  ostth1  24408  ostth2  24412  ostth3  24413  ercgrg  24499  motco  24522  cnvmot  24523  legso  24581  mirmot  24657  lmicom  24767  lmimid  24773  lmimot  24777  hypcgrlem1  24778  hypcgrlem2  24779  ttgcontlem1  24852  brbtwn2  24872  axlowdimlem3  24911  axlowdimlem16  24924  axcontlem8  24938  cusgra0v  25125  cusgraexi  25133  cusgrares  25137  uvtxnb  25162  1pthon  25258  constr2spth  25267  2pthon  25269  usgra2wlkspthlem2  25285  usgra2wlkspth  25286  constr3trllem3  25317  constr3cycl  25326  wlklniswwlkn1  25364  vfwlkniswwlkn  25371  usg2wlkeq2  25374  wwlknred  25388  wwlknredwwlkn0  25392  clwlkisclwwlklem2a1  25444  clwwlkel  25458  wwlkext2clwwlk  25468  clwwnisshclwwn  25474  clwlkf1clwwlk  25515  0egra0rgra  25601  0vgrargra  25602  eupares  25640  eupap1  25641  frgra0v  25658  frgra1v  25663  nvabs  26239  vacn  26267  nmcvcn  26268  nmblore  26364  0lno  26368  0blo  26370  nmlno0lem  26371  occl  26894  pjhthlem1  26981  pjpjpre  27009  nmopre  27460  nmlnop0iALT  27585  nmophmi  27621  leoprf2  27717  stlesi  27831  disjdifprg  28126  fpwrelmap  28263  fzspl  28313  2sqmod  28355  ogrpaddlt  28427  ogrpsublt  28431  pnfinf  28446  xrge0tsmsd  28495  ornglmullt  28517  orngrmullt  28518  orngmullt  28519  ofldlt1  28523  isarchiofld  28527  psgnfzto1stlem  28560  fzto1st1  28562  qtopt1  28609  reff  28613  locfinreflem  28614  metideq  28643  metider  28644  pstmxmet  28647  qqhval2lem  28732  qqhcn  28742  qqhucn  28743  pwsiga  28899  prsiga  28900  measle0  28977  mbfmcst  29028  1stmbfm  29029  2ndmbfm  29030  imambfm  29031  cnmbfm  29032  mbfmco  29033  mbfmco2  29034  carsgclctun  29100  sibfof  29120  oddpwdc  29134  eulerpartlemmf  29155  eulerpartlemgs2  29160  0rrv  29231  ballotlemfc0  29272  ballotlemfcc  29273  signstfveq0  29413  bnj1452  29808  derangen  29842  subfacval3  29859  cvmseu  29946  cvmliftmolem2  29952  cvmliftlem7  29961  cvmliftlem15  29968  cvmlift2lem9a  29973  cvmlift2lem9  29981  cvmlift2lem10  29982  cvmlift2lem11  29983  cvmlift2lem12  29984  cvmlift3lem6  29994  cvmlift3lem8  29996  mclsppslem  30168  mclspps  30169  wsuclem  30454  fness  30949  fnetr  30951  fnessref  30957  refssfne  30958  neibastop1  30959  neibastop2  30961  tailfb  30977  filnetlem3  30980  bj-finsumval0  31609  poimirlem13  31860  poimirlem15  31862  poimirlem17  31864  poimirlem24  31871  poimirlem28  31875  mblfinlem2  31885  ovoliunnfl  31889  volsupnfl  31892  mbfresfi  31894  dvtanlemOLD  31898  itg2addnclem2  31901  iblabsnc  31913  iblmulc2nc  31914  ftc1cnnclem  31922  ftc1cnnc  31923  ftc1anc  31932  fzadd2  31977  sdclem2  31978  metf1o  31991  ismtyhmeolem  32043  ismtyres  32047  heibor1lem  32048  bfplem2  32062  bfp  32063  rrncmslem  32071  iccbnd  32079  icccmpALT  32080  rngogrphom  32117  rngoisoco  32128  keridl  32172  lsmcv2  32507  lsatcv0  32509  lcvexchlem4  32515  lcvexchlem5  32516  l1cvpat  32532  lfl0f  32547  lfladdcl  32549  lflnegcl  32553  lkrlss  32573  eqlkr  32577  lkrlsp  32580  lkrlsp2  32581  lshpkrcl  32594  lkrin  32642  1cvrjat  32952  llni  32985  llnle  32995  lplni  33009  lplnle  33017  llncvrlpln2  33034  2atmat  33038  lvoli  33052  lplncvrlvol2  33092  elpaddri  33279  paddclN  33319  pclclN  33368  pclfinN  33377  0psubclN  33420  1psubclN  33421  atpsubclN  33422  pmapsubclN  33423  osumclN  33444  pexmidN  33446  pexmidlem6N  33452  lhp2lt  33478  lautcnv  33567  idlaut  33573  lautco  33574  idldil  33591  ldilcnv  33592  ldilco  33593  ltrncnv  33623  idltrn  33627  cdleme16d  33759  cdleme50laut  34026  cdleme50ldil  34027  cdleme50ltrn  34036  ltrnco  34198  dian0  34519  dia0eldmN  34520  dia1eldmN  34521  dialss  34526  diaintclN  34538  docaclN  34604  doca2N  34606  djajN  34617  dibintclN  34647  diblss  34650  dicvaddcl  34670  dicvscacl  34671  dicn0  34672  cdlemn11a  34687  dihord2cN  34701  dihord11b  34702  dihord6apre  34736  dihmeetlem1N  34770  dihglblem5apreN  34771  dihpN  34816  dihjatcclem4  34901  dochkr1  34958  islpoldN  34964  lcfrlem31  35053  mapdpglem18  35169  mapdheq2  35209  mapdheq4  35212  mapdh6aN  35215  hdmap1l6a  35290  hdmap1neglem1N  35308  hdmap14lem4a  35354  fzsplit1nn0  35508  icodiamlt  35577  irrapxlem3  35581  irrapxlem4  35582  pell1234qrdich  35620  pell1qr1  35630  pell14qrgap  35634  pellqrexplicit  35636  rmspecfund  35670  fzmaxdif  35744  acongeq  35746  jm2.23  35764  jm3.1  35788  lmhmlnmsplit  35858  hbt  35902  dgrsub2  35907  proot1ex  35991  clublem  36130  dftrcl3  36225  hashnzfz2  36583  dvconstbi  36596  ubelsupr  37257  lefldiveq  37403  iccintsng  37516  fmul01  37541  fmuldfeq  37544  climsuse  37570  mullimc  37579  limcdm0  37581  limccog  37583  mullimcf  37586  constlimc  37587  idlimc  37589  limcperiod  37591  limsupre  37604  limsupreOLD  37605  limcleqr  37608  neglimc  37611  addlimc  37612  0ellimcdiv  37613  cncfshift  37634  cncfperiod  37639  cncfuni  37647  icccncfext  37648  cncfiooicclem1  37654  fperdvper  37673  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  mbfres2cn  37718  iblsplit  37726  stoweidlem7  37750  stoweidlem13  37756  stoweidlem26  37769  wallispilem3  37812  stirlinglem6  37824  stirlinglem10  37828  dirkercncf  37852  fourierdlem6  37858  fourierdlem11  37863  fourierdlem12  37864  fourierdlem15  37867  fourierdlem26  37878  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem50  37903  fourierdlem51  37904  fourierdlem52  37905  fourierdlem54  37907  fourierdlem62  37915  fourierdlem79  37932  fourierdlem102  37955  fourierdlem114  37967  etransclem23  38005  zgeltp1eq  38530  iccpartres  38545  pfx2  38766  pfxccatin12d  38786  repswpfx  38790  fusgrfis  39132  nbgr2vtx1edg  39154  uvtxnbgrb  39204  cplgr1v  39225  rabsubmgmd  39382  submgmid  39384  subsubmgm  39388  mgmhmima  39393  mgmhmeql  39394  isassintop  39437  rnghmsscmap2  39566  rnghmsscmap  39567  rnghmsubcsetc  39570  zrzeroorngc  39595  rhmsscmap2  39612  rhmsscmap  39613  rhmsubcsetc  39616  rhmsscrnghm  39619  rhmsubcrngc  39622  srhmsubc  39669  fldhmsubc  39677  rhmsubc  39683  srhmsubcALTV  39688  fldhmsubcALTV  39696  rhmsubcALTV  39702  rmfsupp  39752  mndpfsupp  39754  scmfsupp  39756  mptcfsupp  39758  lcoel0  39814  lincsumcl  39817  lincscmcl  39818  lcoss  39822  lindsrng01  39854  lincreslvec3  39868  lindssnlvec  39872  zgtp1leeq  39912
  Copyright terms: Public domain W3C validator