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

Theorem mpbir2and 920
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 530 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 232 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  fveqressseq  5929  fmptsng  5994  fmptsnd  5995  fnprb  6032  fdmfifsupp  7754  fczfsuppd  7762  fsuppmptif  7774  fsuppco2  7777  fsuppcor  7778  dffi3  7806  supmaxOLD  7840  suppr  7844  ordtypelem7  7864  cantnf0  8007  cantnfp1lem1  8010  cantnfp1lem2  8011  cantnfp1lem3  8012  cantnflem1a  8017  cantnflem1d  8020  cantnflem1  8021  cantnf  8025  cantnfleOLD  8033  cantnfp1lem1OLD  8036  cantnfp1lem2OLD  8037  cantnfp1lem3OLD  8038  cantnflem1aOLD  8040  cantnflem1cOLD  8042  cantnflem1dOLD  8043  cantnflem1OLD  8044  cantnfOLD  8047  mapfienOLD  8051  rankpwi  8154  carduni  8275  fin23lem32  8637  fpwwe2lem6  8924  fpwwe2lem9  8927  fpwwe2lem12  8930  fpwwe2lem13  8931  fpwwe2  8932  inttsk  9063  grutsk1  9110  add20  9982  supmul  10427  suprzcl  10859  uzwo3  11096  rpnnen1lem5  11131  xrre  11291  xrre3  11293  xleadd1a  11366  xlemul1a  11401  supxrre  11440  infmxrre  11448  ixxub  11471  ixxlb  11472  elioc2  11508  elico2  11509  elicc2  11510  elfz1eq  11618  fznatpl1  11656  nn0fz0  11696  fzctr  11709  fzo1fzo0n0  11759  fzoaddel  11768  elincfzoext  11773  flid  11844  flval3  11850  fladdz  11858  fldiv  11887  modid  11921  seqf1olem1  12049  bcval5  12298  hashf1lem1  12408  eqs1  12530  wwlktovf1  12806  sqeqd  13001  sqrlem7  13084  max0add  13145  abs2difabs  13169  rddif  13175  fzomaxdiflem  13177  rexico  13188  limsupgre  13306  rlim3  13323  icco1  13365  rlimclim  13371  rlimuni  13375  rlimresb  13390  isercolllem2  13490  isercolllem3  13491  isercoll  13492  caucvgrlem  13497  caurcvgr  13498  iseraltlem3  13508  fsum00  13614  o1fsum  13629  dvdseq  14035  bitsfzolem  14086  bitsfzo  14087  bitsmod  14088  bitscmp  14090  gcd0id  14163  gcdneg  14166  bezoutlem4  14181  nn0seqcvgd  14201  prmind2  14230  qredeq  14249  isprm5  14255  hashdvds  14307  eulerthlem2  14314  pcpremul  14369  pcidlem  14397  pcgcd1  14402  pcadd2  14411  fldivp1  14418  pcfaclem  14419  prmreclem5  14440  4sqlem17  14481  vdwlem1  14501  vdwlem6  14506  vdwlem12  14512  vdwlem13  14513  0ram  14540  ram0  14542  ramub1lem1  14546  invco  15177  sectmon  15188  monsect  15189  invid  15193  cicref  15207  ssctr  15231  ssceq  15232  0ssc  15243  0subcat  15244  catsubcat  15245  issubc3  15255  fullsubc  15256  funcinv  15279  fthmon  15333  fuccocl  15370  fucidcl  15371  invfuc  15380  2initoinv  15406  2termoinv  15413  elhomai  15429  setcmon  15483  setcepi  15484  catcisolem  15502  curf2cl  15617  yonedalem4c  15663  yonedalem3  15666  yoniso  15671  lublecl  15736  isacs3lem  15913  tsrdir  15985  mnd1  16078  mnd1OLD  16079  sgrp2nmndlem4  16163  sgrp2nmndlem5  16164  nmznsg  16362  ghmpreima  16405  ghmeql  16406  ghmnsgpreima  16408  cntzsubm  16490  cntzsubg  16491  cntzmhm  16493  symgextfo  16564  symgfixf1  16579  symgfixfolem1  16580  odlem2  16680  gexlem2  16719  gexcl2  16726  sylow1lem5  16739  subgslw  16753  slwhash  16761  fislw  16762  sylow3lem1  16764  lsmsubg  16791  efgredlemd  16879  efgredlem  16882  efgcpbllemb  16890  frgpuplem  16907  cyggeninv  17003  iscygd  17007  iscygodd  17008  gsumzadd  17052  gsumconst  17070  gsumpt  17102  gsumptOLD  17103  gsum2dlem2  17112  gsum2d  17113  gsum2d2lem  17115  dprdfcntz  17162  dprdfcntzOLD  17168  eldprdi  17171  eldprdiOLD  17178  subgdmdprd  17194  subgdprd  17195  dprdpr  17212  ablfac1c  17235  ablfac1eu  17237  ablfaclem3  17251  ring1  17361  kerf1hrm  17505  issubdrg  17567  rhmeql  17572  rhmima  17573  cntzsubr  17574  isabvd  17582  abvdiv  17599  lsslsp  17774  lmhmima  17806  lmhmpreima  17807  lmhmeql  17814  lsmcl  17842  lspfixed  17887  issubassa  18086  issubassa2  18107  snifpsrbag  18128  psrbaglesupp  18130  psrbaglesuppOLD  18131  psrbaglecl  18132  psrbagaddcl  18133  psrbagaddclOLD  18134  psrbagcon  18135  psrbasOLD  18144  psrlidmOLD  18170  psrridmOLD  18172  mvridlemOLD  18188  mplsubglem  18206  mpllsslem  18207  mplsubglemOLD  18208  mpllsslemOLD  18209  mplassa  18229  subrgmpl  18235  mplcoe3OLD  18242  mplcoe5  18244  mplcoe2OLD  18246  mplbas2  18247  mplbas2OLD  18248  mplind  18280  evlslem3  18296  mpfind  18318  ply1assa  18351  coe1tmmul2  18430  coe1tmmul  18431  cply1coe0bi  18455  qsssubdrg  18590  gzrngunit  18596  evpmodpmf1o  18723  ocvpj  18839  dsmm0cl  18862  dsmmacl  18863  dsmmsubg  18865  dsmmlss  18866  frlmsplit2  18892  uvcff  18911  lindfrn  18941  f1lindf  18942  lindsss  18944  mat1rngiso  19073  dmatid  19082  dmatsubcl  19085  dmatscmcl  19090  scmatid  19101  scmataddcl  19103  scmatsubcl  19104  scmatmulcl  19105  smatvscl  19111  scmatrhmcl  19115  scmatrngiso  19123  mat0scmat  19125  mat1scmat  19126  mdet0pr  19179  m2cpmrngiso  19344  pm2mprngiso  19408  chmaidscmat  19434  fvmptnn04if  19435  distop  19582  indistopon  19587  ppttop  19593  epttop  19595  mretopd  19679  toponmre  19680  neiss  19696  opnneissb  19701  ssnei2  19703  innei  19712  neiptoptop  19718  ordtcld1  19784  ordtcld2  19785  lmconst  19848  cnpnei  19851  iscncl  19856  cnss1  19863  cnss2  19864  cncnpi  19865  cncnp  19867  cnconst2  19870  cnrest  19872  cnpresti  19875  cnpdis  19880  paste  19881  lmcnp  19891  cnhaus  19941  hauscmp  19993  2ndcomap  20044  1stcelcls  20047  1stccnp  20048  llyrest  20071  nllyrest  20072  llyidm  20074  nllyidm  20075  ssref  20098  reftr  20100  refun0  20101  dissnref  20114  kgentopon  20124  kgenidm  20133  kgencn3  20144  txcld  20189  neitx  20193  tx1cn  20195  tx2cn  20196  ptcld  20199  xkoccn  20205  txcnp  20206  ptcnp  20208  txcnmpt  20210  ptcn  20213  txdis1cn  20221  ptrescn  20225  txkgen  20238  xkoco1cn  20243  xkoco2cn  20244  xkococn  20246  xkoinjcn  20273  qtoptop2  20285  qtopuni  20288  qtopid  20291  qtopkgen  20296  basqtop  20297  tgqtop  20298  qtopss  20301  qtopeu  20302  qtoprest  20303  kqopn  20320  kqcld  20321  kqreglem2  20328  reghmph  20379  ordthmeolem  20387  qtopf1  20402  opnfbas  20428  isfil2  20442  fbasweak  20451  fsubbas  20453  filcon  20469  fbasrn  20470  rnelfmlem  20538  flimss2  20558  flimss1  20559  hausflim  20567  flimclslem  20570  flimsncls  20572  cnpflfi  20585  flfcnp2  20593  fclsfnflim  20613  cnextfvval  20650  cnextfres  20653  symgtgp  20685  opnsubg  20691  ghmcnp  20698  qustgpopn  20703  qustgplem  20704  qustgphaus  20706  tsmsfbas  20711  ustfilxp  20800  utoptop  20822  utopbas  20823  restutopopn  20826  iducn  20871  cstucnd  20872  ucncn  20873  fmucnd  20880  cfilufg  20881  trcfilu  20882  cfiluweak  20883  neipcfilu  20884  psmetsym  20899  psmetres2  20903  isxmetd  20914  xmetsym  20935  xmetpsmet  20936  imasdsf1olem  20961  imasf1oxmet  20963  xblss2ps  20989  xblss2  20990  xblcntrps  20998  xblcntr  20999  blcld  21093  metustfbasOLD  21153  metustfbas  21154  cfilucfilOLD  21157  cfilucfil  21158  restmetu  21175  ngptgp  21235  tngngpd  21252  tngnrg  21268  nlmvscn  21281  nrginvrcn  21285  nmo0  21327  nmoeq0  21328  nmoid  21334  nghmcn  21337  0nmhm  21347  blcvx  21388  zcld  21403  iccntr  21411  xrge0tsms  21424  xmetdcn2  21427  metdstri  21440  metdscn  21445  rescncf  21486  cncfco  21496  oprpiece1res2  21537  cnheibor  21540  cnllycmp  21541  bndth  21543  evth  21544  ishtpyd  21560  isphtpyd  21571  pcoval2  21601  nmhmcn  21688  ipcn  21771  lmnn  21787  cfilss  21794  iscfil3  21797  cfilfcls  21798  cmetcaulem  21812  iscmet3lem2  21816  cfilres  21820  lmcau  21836  flimcfil  21837  cncmet  21846  rlmbn  21886  minveclem3b  21928  pjthlem1  21937  pjth2  21940  ivthlem3  21950  ovolssnul  21983  ovolctb  21986  ovolunnul  21996  ovoliunnul  22003  ovolsca  22011  ovolicc  22019  ovolicopnf  22020  voliunlem2  22046  voliunlem3  22047  volsup  22051  uniioovol  22073  uniiccvol  22074  dyadmaxlem  22091  vitalilem5  22106  ismbfd  22132  mbfres  22136  mbfss  22138  mbfmulc2re  22140  mbfadd  22153  mbfmulc2  22155  mbflimsup  22158  mbflim  22160  i1faddlem  22185  i1fmullem  22186  mbfmul  22218  itg2itg1  22228  itg2seq  22234  itg2eqa  22237  itg2mulc  22239  itg2split  22241  itg2mono  22245  itg2cnlem1  22253  ibl0  22278  iblposlem  22283  itgreval  22288  iblneg  22294  iblss  22296  iblss2  22297  itgle  22301  iblconst  22309  iblabs  22320  iblabsr  22321  iblmulc2  22322  bddmulibl  22330  limciun  22383  limcun  22384  dvres2lem  22399  dvidlem  22404  dvcnp2  22408  dvcn  22409  cpnres  22425  dvaddbr  22426  dvmulbr  22427  dvcobr  22434  dvcjbr  22437  dvrec  22443  dvcnvlem  22462  dvferm  22474  dvlip2  22481  dveq0  22486  dv11cn  22487  dvivthlem1  22494  lhop1  22500  lhop2  22501  lhop  22502  dvcnvre  22505  dvfsumlem3  22514  dvfsumlem4  22515  dvfsumrlim  22517  dvfsum2  22520  ftc1a  22523  ftc1lem4  22525  ftc1lem6  22527  ftc1  22528  coe1mul3  22585  deg1addle2  22588  deg1add  22589  deg1sublt  22596  deg1mul2  22600  deg1tm  22604  fta1blem  22654  drnguc1p  22656  ig1prsp  22663  plyco0  22674  plyeq0lem  22692  dgrub  22716  dgreq  22726  dgradd2  22750  dgrmul  22752  dgrcolem2  22756  dgrco  22757  plycpn  22770  plydivlem4  22777  plydiveu  22779  vieta1lem2  22792  vieta1  22793  aalioulem2  22814  aalioulem3  22815  aaliou3lem7  22830  tayl0  22842  ulmcn  22879  ulmdvlem3  22882  psercn  22906  abelth  22921  pilem3  22933  efif1olem1  23014  abslogimle  23046  argregt0  23082  argrege0  23083  logf1o2  23118  cxpsqrtlem  23170  cxpcn3  23209  abscxpbnd  23214  logreclem  23220  ang180lem2  23260  ang180lem3  23261  xrlimcnp  23415  harmonicbnd4  23457  fsumharmonic  23458  basellem3  23473  basellem4  23474  dvdsppwf1o  23579  dvdsflf1o  23580  fsumfldivdiaglem  23582  chpeq0  23600  chteq0  23601  chtub  23604  chpub  23612  dchrelbasd  23631  dchrmulcl  23641  dchrinv  23653  bcmono  23669  bposlem1  23676  bposlem2  23677  lgslem1  23688  lgsdirprm  23721  lgsqrlem2  23734  lgsqrlem3  23735  lgsdchr  23740  lgseisenlem1  23741  lgseisenlem2  23742  lgseisenlem3  23743  lgsquadlem1  23746  2sqlem8  23764  2sqblem  23769  chebbnd1lem1  23771  dchrisumlem1  23791  dchrisumlem2  23792  dchrisumlem3  23793  dchrisum0fno1  23813  pntrmax  23866  pntpbnd1a  23887  pntibndlem3  23894  pntlemn  23902  pntlemi  23906  pntlem3  23911  pntleml  23913  ostth1  23935  ostth2  23939  ostth3  23940  ercgrg  24028  motco  24047  cnvmot  24048  legso  24105  mirmot  24175  lmicom  24274  lmimid  24279  lmimot  24283  hypcgrlem1  24284  hypcgrlem2  24285  ttgcontlem1  24309  brbtwn2  24329  axlowdimlem3  24368  axlowdimlem16  24381  axcontlem8  24395  cusgra0v  24581  cusgraexi  24589  cusgrares  24593  uvtxnb  24618  1pthon  24714  constr2spth  24723  2pthon  24725  usgra2wlkspthlem2  24741  usgra2wlkspth  24742  constr3trllem3  24773  constr3cycl  24782  wlklniswwlkn1  24820  vfwlkniswwlkn  24827  usg2wlkeq2  24830  wwlknred  24844  wwlknredwwlkn0  24848  clwlkisclwwlklem2a1  24900  clwwlkel  24914  wwlkext2clwwlk  24924  clwwnisshclwwn  24930  clwlkf1clwwlk  24971  0egra0rgra  25057  0vgrargra  25058  eupares  25096  eupap1  25097  frgra0v  25114  frgra1v  25119  nvabs  25693  vacn  25721  nmcvcn  25722  nmblore  25818  0lno  25822  0blo  25824  nmlno0lem  25825  occl  26339  pjhthlem1  26426  pjpjpre  26454  nmopre  26905  nmlnop0iALT  27030  nmophmi  27066  leoprf2  27162  stlesi  27276  disjdifprg  27565  fpwrelmap  27706  fzspl  27751  2sqmod  27789  ogrpaddlt  27861  ogrpsublt  27865  pnfinf  27880  xrge0tsmsd  27929  ornglmullt  27951  orngrmullt  27952  orngmullt  27953  ofldlt1  27957  isarchiofld  27961  qtopt1  27992  reff  27996  locfinreflem  27997  metideq  28026  metider  28027  pstmxmet  28030  qqhval2lem  28115  qqhcn  28125  qqhucn  28126  pwsiga  28279  prsiga  28280  measle0  28335  mbfmcst  28386  1stmbfm  28387  2ndmbfm  28388  imambfm  28389  cnmbfm  28390  mbfmco  28391  mbfmco2  28392  carsgclctun  28448  sibfof  28465  oddpwdc  28476  eulerpartlemmf  28497  eulerpartlemgs2  28502  0rrv  28573  ballotlemfc0  28614  ballotlemfcc  28615  signstfveq0  28717  lgamgulmlem5  28764  lgambdd  28768  derangen  28805  subfacval3  28822  cvmseu  28910  cvmliftmolem2  28916  cvmliftlem7  28925  cvmliftlem15  28932  cvmlift2lem9a  28937  cvmlift2lem9  28945  cvmlift2lem10  28946  cvmlift2lem11  28947  cvmlift2lem12  28948  cvmlift3lem6  28958  cvmlift3lem8  28960  mclsppslem  29132  mclspps  29133  wsuclem  29546  supaddc  30206  supadd  30207  mblfinlem2  30217  ovoliunnfl  30221  volsupnfl  30224  mbfresfi  30226  dvtanlemOLD  30230  itg2addnclem2  30233  iblabsnc  30245  iblmulc2nc  30246  ftc1cnnclem  30254  ftc1cnnc  30255  ftc1anc  30264  fness  30333  fnetr  30335  fnessref  30341  refssfne  30342  neibastop1  30343  neibastop2  30345  tailfb  30361  filnetlem3  30364  fzadd2  30400  sdclem2  30401  metf1o  30414  ismtyhmeolem  30466  ismtyres  30470  heibor1lem  30471  bfplem2  30485  bfp  30486  rrncmslem  30494  iccbnd  30502  icccmpALT  30503  rngogrphom  30540  rngoisoco  30551  keridl  30595  fzsplit1nn0  30852  icodiamlt  30921  irrapxlem3  30925  irrapxlem4  30926  pell1234qrdich  30962  pell1qr1  30972  pell14qrgap  30976  pellqrexplicit  30978  rmspecfund  31010  fzmaxdif  31084  acongeq  31086  jm2.23  31104  jm3.1  31128  lmhmlnmsplit  31199  hbt  31247  dgrsub2  31252  proot1ex  31329  lcmneg  31377  hashnzfz2  31394  dvconstbi  31407  ubelsupr  31562  lefldiveq  31649  iccintsng  31729  fmul01  31740  fmuldfeq  31743  climsuse  31780  mullimc  31788  limcdm0  31790  limccog  31792  mullimcf  31795  constlimc  31796  idlimc  31798  limcperiod  31800  limsupre  31813  limcleqr  31816  neglimc  31819  addlimc  31820  0ellimcdiv  31821  cncfshift  31842  cncfperiod  31847  cncfuni  31855  icccncfext  31856  cncfiooicclem1  31862  fperdvper  31881  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  mbfres2cn  31923  iblsplit  31931  stoweidlem7  31955  stoweidlem13  31961  stoweidlem26  31974  wallispilem3  32015  stirlinglem6  32027  stirlinglem10  32031  dirkercncf  32055  fourierdlem6  32061  fourierdlem11  32066  fourierdlem12  32067  fourierdlem15  32070  fourierdlem26  32081  fourierdlem42  32097  fourierdlem50  32105  fourierdlem51  32106  fourierdlem52  32107  fourierdlem54  32109  fourierdlem62  32117  fourierdlem79  32134  fourierdlem102  32157  fourierdlem114  32169  etransclem23  32206  pfx2  32587  pfxccatin12d  32607  repswpfx  32611  rabsubmgmd  32797  submgmid  32799  subsubmgm  32803  mgmhmima  32808  mgmhmeql  32809  isassintop  32852  rnghmsscmap2  32981  rnghmsscmap  32982  rnghmsubcsetc  32985  zrzeroorngc  33010  rhmsscmap2  33027  rhmsscmap  33028  rhmsubcsetc  33031  rhmsscrnghm  33034  rhmsubcrngc  33037  srhmsubc  33084  fldhmsubc  33092  rhmsubc  33098  srhmsubcALTV  33103  fldhmsubcALTV  33111  rhmsubcALTV  33117  rmfsupp  33167  mndpfsupp  33169  scmfsupp  33171  mptcfsupp  33173  lcoel0  33229  lincsumcl  33232  lincscmcl  33233  lcoss  33237  lindsrng01  33269  lincreslvec3  33283  lindssnlvec  33287  zgeltp1eq  33328  zgtp1leeq  33329  bnj1452  34455  bj-finsumval0  35010  lsmcv2  35167  lsatcv0  35169  lcvexchlem4  35175  lcvexchlem5  35176  l1cvpat  35192  lfl0f  35207  lfladdcl  35209  lflnegcl  35213  lkrlss  35233  eqlkr  35237  lkrlsp  35240  lkrlsp2  35241  lshpkrcl  35254  lkrin  35302  1cvrjat  35612  llni  35645  llnle  35655  lplni  35669  lplnle  35677  llncvrlpln2  35694  2atmat  35698  lvoli  35712  lplncvrlvol2  35752  elpaddri  35939  paddclN  35979  pclclN  36028  pclfinN  36037  0psubclN  36080  1psubclN  36081  atpsubclN  36082  pmapsubclN  36083  osumclN  36104  pexmidN  36106  pexmidlem6N  36112  lhp2lt  36138  lautcnv  36227  idlaut  36233  lautco  36234  idldil  36251  ldilcnv  36252  ldilco  36253  ltrncnv  36283  idltrn  36287  cdleme16d  36419  cdleme50laut  36686  cdleme50ldil  36687  cdleme50ltrn  36696  ltrnco  36858  dian0  37179  dia0eldmN  37180  dia1eldmN  37181  dialss  37186  diaintclN  37198  docaclN  37264  doca2N  37266  djajN  37277  dibintclN  37307  diblss  37310  dicvaddcl  37330  dicvscacl  37331  dicn0  37332  cdlemn11a  37347  dihord2cN  37361  dihord11b  37362  dihord6apre  37396  dihmeetlem1N  37430  dihglblem5apreN  37431  dihpN  37476  dihjatcclem4  37561  dochkr1  37618  islpoldN  37624  lcfrlem31  37713  mapdpglem18  37829  mapdheq2  37869  mapdheq4  37872  mapdh6aN  37875  hdmap1l6a  37950  hdmap1neglem1N  37968  hdmap14lem4a  38014  dftrcl3  38231
  Copyright terms: Public domain W3C validator