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

Theorem mpbir2and 906
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 529 . 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 369
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
This theorem is referenced by:  fmptsng  5887  fnprb  5923  fnprOLD  5924  fdmfifsupp  7618  fczfsuppd  7626  fsuppmptif  7637  fsuppco2  7640  fsuppcor  7641  dffi3  7669  supmax  7703  suppr  7706  ordtypelem7  7726  cantnf0  7871  cantnfp1lem1  7874  cantnfp1lem2  7875  cantnfp1lem3  7876  cantnflem1a  7881  cantnflem1d  7884  cantnflem1  7885  cantnf  7889  cantnfleOLD  7897  cantnfp1lem1OLD  7900  cantnfp1lem2OLD  7901  cantnfp1lem3OLD  7902  cantnflem1aOLD  7904  cantnflem1cOLD  7906  cantnflem1dOLD  7907  cantnflem1OLD  7908  cantnfOLD  7911  mapfienOLD  7915  rankpwi  8018  carduni  8139  fin23lem32  8501  fpwwe2lem6  8790  fpwwe2lem9  8793  fpwwe2lem12  8796  fpwwe2lem13  8797  fpwwe2  8798  inttsk  8929  grutsk1  8976  add20  9839  supmul  10286  suprzcl  10709  uzwo3  10936  rpnnen1lem5  10971  xrre  11129  xrre3  11131  xleadd1a  11204  xlemul1a  11239  supxrre  11278  infmxrre  11286  ixxub  11309  ixxlb  11310  elioc2  11346  elico2  11347  elicc2  11348  elfz1eq  11449  fznatpl1  11495  nn0fz0  11509  fzctr  11513  fzo1fzo0n0  11572  fzoaddel  11581  flid  11641  flval3  11647  fladdz  11654  fldiv  11683  modid  11716  seqf1olem1  11829  bcval5  12078  hashf1lem1  12192  sqeqd  12639  sqrlem7  12722  max0add  12783  abs2difabs  12806  rddif  12812  fzomaxdiflem  12814  rexico  12825  limsupgre  12943  rlim3  12960  icco1  13002  rlimclim  13008  rlimuni  13012  rlimresb  13027  isercolllem2  13127  isercolllem3  13128  isercoll  13129  caucvgrlem  13134  caurcvgr  13135  iseraltlem3  13145  fsum00  13244  o1fsum  13259  dvdseq  13563  bitsfzolem  13613  bitsfzo  13614  bitsmod  13615  bitscmp  13617  gcd0id  13690  gcdneg  13693  bezoutlem4  13708  nn0seqcvgd  13728  prmind2  13757  qredeq  13775  isprm5  13781  hashdvds  13833  eulerthlem2  13840  pcpremul  13893  pcidlem  13921  pcgcd1  13926  pcadd2  13935  fldivp1  13942  pcfaclem  13943  prmreclem5  13964  4sqlem17  14005  vdwlem1  14025  vdwlem6  14030  vdwlem12  14036  vdwlem13  14037  0ram  14064  ram0  14066  ramub1lem1  14070  invco  14692  sectmon  14699  monsect  14700  ssctr  14721  ssceq  14722  issubc3  14742  fullsubc  14743  funcinv  14766  fthmon  14820  fuccocl  14857  fucidcl  14858  invfuc  14867  elhomai  14884  setcmon  14938  setcepi  14939  catcisolem  14957  curf2cl  15024  yonedalem4c  15070  yonedalem3  15073  yoniso  15078  lublecl  15142  isacs3lem  15319  tsrdir  15391  nmznsg  15705  ghmpreima  15748  ghmeql  15749  ghmnsgpreima  15751  cntzsubm  15833  cntzsubg  15834  cntzmhm  15836  symgextfo  15907  symgfixf1  15923  symgfixfolem1  15924  odlem2  16022  gexlem2  16061  gexcl2  16068  sylow1lem5  16081  subgslw  16095  slwhash  16103  fislw  16104  sylow3lem1  16106  lsmsubg  16133  efgredlemd  16221  efgredlem  16224  efgcpbllemb  16232  frgpuplem  16249  cyggeninv  16340  iscygd  16344  iscygodd  16345  gsumzadd  16389  gsumconst  16406  gsumpt  16429  gsumptOLD  16430  gsum2dlem2  16436  gsum2d  16437  gsum2d2lem  16439  dprdfcntz  16473  dprdfcntzOLD  16479  eldprdi  16482  eldprdiOLD  16489  subgdmdprd  16505  subgdprd  16506  dprdpr  16523  ablfac1c  16546  ablfac1eu  16548  ablfaclem3  16562  issubdrg  16814  rhmeql  16819  rhmima  16820  cntzsubr  16821  isabvd  16829  abvdiv  16846  lsslsp  17018  lmhmima  17050  lmhmpreima  17051  lmhmeql  17058  lsmcl  17086  lspfixed  17131  issubassa  17317  issubassa2  17337  snifpsrbag  17367  psrbaglesupp  17369  psrbaglesuppOLD  17370  psrbaglecl  17371  psrbagaddcl  17372  psrbagaddclOLD  17373  psrbagcon  17374  psrbasOLD  17383  psrlidmOLD  17409  psrridmOLD  17411  mvridlemOLD  17426  mplsubglem  17444  mpllsslem  17445  mplsubglemOLD  17446  mpllsslemOLD  17447  mplassa  17467  subrgmpl  17473  mplcoe3OLD  17480  mplcoe2  17481  mplcoe2OLD  17482  mplbas2  17483  mplbas2OLD  17484  mplind  17516  ply1assa  17554  coe1tmmul2  17627  coe1tmmul  17628  qsssubdrg  17716  gzrngunit  17722  evpmodpmf1o  17868  ocvpj  17984  dsmm0cl  18007  dsmmacl  18008  dsmmsubg  18010  dsmmlss  18011  frlmsplit2  18039  uvcff  18058  lindfrn  18092  f1lindf  18093  lindsss  18095  mdet0pr  18245  distop  18442  indistopon  18447  ppttop  18453  epttop  18455  mretopd  18538  toponmre  18539  neiss  18555  opnneissb  18560  ssnei2  18562  innei  18571  neiptoptop  18577  ordtcld1  18643  ordtcld2  18644  lmconst  18707  cnpnei  18710  iscncl  18715  cnss1  18722  cnss2  18723  cncnpi  18724  cncnp  18726  cnconst2  18729  cnrest  18731  cnpresti  18734  cnpdis  18739  paste  18740  lmcnp  18750  cnhaus  18800  hauscmp  18852  2ndcomap  18904  1stcelcls  18907  1stccnp  18908  llyrest  18931  nllyrest  18932  llyidm  18934  nllyidm  18935  kgentopon  18953  kgenidm  18962  kgencn3  18973  txcld  19018  neitx  19022  tx1cn  19024  tx2cn  19025  ptcld  19028  xkoccn  19034  txcnp  19035  ptcnp  19037  txcnmpt  19039  ptcn  19042  txdis1cn  19050  ptrescn  19054  txkgen  19067  xkoco1cn  19072  xkoco2cn  19073  xkococn  19075  xkoinjcn  19102  qtoptop2  19114  qtopuni  19117  qtopid  19120  qtopkgen  19125  basqtop  19126  tgqtop  19127  qtopss  19130  qtopeu  19131  qtoprest  19132  kqopn  19149  kqcld  19150  kqreglem2  19157  reghmph  19208  ordthmeolem  19216  qtopf1  19231  opnfbas  19257  isfil2  19271  fbasweak  19280  fsubbas  19282  filcon  19298  fbasrn  19299  rnelfmlem  19367  flimss2  19387  flimss1  19388  hausflim  19396  flimclslem  19399  flimsncls  19401  cnpflfi  19414  flfcnp2  19422  fclsfnflim  19442  cnextfvval  19479  cnextfres  19482  symgtgp  19514  opnsubg  19520  ghmcnp  19527  divstgpopn  19532  divstgplem  19533  divstgphaus  19535  tsmsfbas  19540  ustfilxp  19629  utoptop  19651  utopbas  19652  restutopopn  19655  iducn  19700  cstucnd  19701  ucncn  19702  fmucnd  19709  cfilufg  19710  trcfilu  19711  cfiluweak  19712  neipcfilu  19713  psmetsym  19728  isxmetd  19743  xmetsym  19764  imasdsf1olem  19790  imasf1oxmet  19792  xblss2ps  19818  xblss2  19819  xblcntrps  19827  xblcntr  19828  blcld  19922  metustfbasOLD  19982  metustfbas  19983  cfilucfilOLD  19986  cfilucfil  19987  restmetu  20004  ngptgp  20064  tngngpd  20081  tngnrg  20097  nlmvscn  20110  nrginvrcn  20114  nmo0  20156  nmoeq0  20157  nmoid  20163  nghmcn  20166  0nmhm  20176  blcvx  20217  zcld  20232  iccntr  20240  xrge0tsms  20253  xmetdcn2  20256  metdstri  20269  metdscn  20274  rescncf  20315  cncfco  20325  oprpiece1res2  20366  cnheibor  20369  cnllycmp  20370  bndth  20372  evth  20373  ishtpyd  20389  isphtpyd  20400  pcoval2  20430  nmhmcn  20517  ipcn  20600  lmnn  20616  cfilss  20623  iscfil3  20626  cfilfcls  20627  cmetcaulem  20641  iscmet3lem2  20645  cfilres  20649  lmcau  20665  flimcfil  20666  cncmet  20675  rlmbn  20715  minveclem3b  20757  pjthlem1  20766  pjth2  20769  ivthlem3  20779  ovolssnul  20812  ovolctb  20815  ovolunnul  20825  ovoliunnul  20832  ovolsca  20840  ovolicc  20848  ovolicopnf  20849  voliunlem2  20874  voliunlem3  20875  volsup  20879  uniioovol  20901  uniiccvol  20902  dyadmaxlem  20919  vitalilem5  20934  ismbfd  20960  mbfres  20964  mbfss  20966  mbfmulc2re  20968  mbfadd  20981  mbfmulc2  20983  mbflimsup  20986  mbflim  20988  i1faddlem  21013  i1fmullem  21014  mbfmul  21046  itg2itg1  21056  itg2seq  21062  itg2eqa  21065  itg2mulc  21067  itg2split  21069  itg2mono  21073  itg2cnlem1  21081  ibl0  21106  iblposlem  21111  itgreval  21116  iblneg  21122  iblss  21124  iblss2  21125  itgle  21129  iblconst  21137  iblabs  21148  iblabsr  21149  iblmulc2  21150  bddmulibl  21158  limciun  21211  limcun  21212  dvres2lem  21227  dvidlem  21232  dvcnp2  21236  dvcn  21237  cpnres  21253  dvaddbr  21254  dvmulbr  21255  dvcobr  21262  dvcjbr  21265  dvrec  21271  dvcnvlem  21290  dvferm  21302  dvlip2  21309  dveq0  21314  dv11cn  21315  dvivthlem1  21322  lhop1  21328  lhop2  21329  lhop  21330  dvcnvre  21333  dvfsumlem3  21342  dvfsumlem4  21343  dvfsumrlim  21345  dvfsum2  21348  ftc1a  21351  ftc1lem4  21353  ftc1lem6  21355  ftc1  21356  evlslem3  21366  mpfind  21396  coe1mul3  21456  deg1addle2  21459  deg1add  21460  deg1sublt  21467  deg1mul2  21471  deg1tm  21475  fta1blem  21525  drnguc1p  21527  ig1prsp  21534  plyco0  21545  plyeq0lem  21563  dgrub  21587  dgreq  21597  dgradd2  21620  dgrmul  21622  dgrcolem2  21626  dgrco  21627  plycpn  21640  plydivlem4  21647  plydiveu  21649  vieta1lem2  21662  vieta1  21663  aalioulem2  21684  aalioulem3  21685  aaliou3lem7  21700  tayl0  21712  ulmcn  21749  ulmdvlem3  21752  psercn  21776  abelth  21791  pilem3  21803  efif1olem1  21883  abslogimle  21910  argregt0  21944  argrege0  21945  logf1o2  21980  cxpsqrlem  22032  cxpcn3  22071  abscxpbnd  22076  ang180lem2  22091  ang180lem3  22092  logreclem  22099  xrlimcnp  22247  harmonicbnd4  22289  fsumharmonic  22290  basellem3  22305  basellem4  22306  dvdsppwf1o  22411  dvdsflf1o  22412  fsumfldivdiaglem  22414  chpeq0  22432  chteq0  22433  chtub  22436  chpub  22444  dchrelbasd  22463  dchrmulcl  22473  dchrinv  22485  bcmono  22501  bposlem1  22508  bposlem2  22509  lgslem1  22520  lgsdirprm  22553  lgsqrlem2  22566  lgsqrlem3  22567  lgsdchr  22572  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem3  22575  lgsquadlem1  22578  2sqlem8  22596  2sqblem  22601  chebbnd1lem1  22603  dchrisumlem1  22623  dchrisumlem2  22624  dchrisumlem3  22625  dchrisum0fno1  22645  pntrmax  22698  pntpbnd1a  22719  pntibndlem3  22726  pntlemn  22734  pntlemi  22738  pntlem3  22743  pntleml  22745  ostth1  22767  ostth2  22771  ostth3  22772  ttgcontlem1  22954  brbtwn2  22974  axlowdimlem3  23013  axlowdimlem16  23026  axcontlem8  23040  cusgra0v  23191  cusgraexi  23199  cusgrares  23203  1pthon  23313  constr2spth  23322  2pthon  23324  constr3trllem3  23361  constr3cycl  23370  eupares  23419  eupap1  23420  nvabs  23884  vacn  23912  nmcvcn  23913  nmblore  24009  0lno  24013  0blo  24015  nmlno0lem  24016  occl  24530  pjhthlem1  24617  pjpjpre  24645  nmopre  25097  nmlnop0iALT  25222  nmophmi  25258  leoprf2  25354  stlesi  25468  disjdifprg  25743  fpwrelmap  25858  xrge0tsmsd  26106  ornglmullt  26128  orngrmullt  26129  ofldlt1  26134  isarchiofld  26138  kerf1hrm  26145  metider  26175  qqhval2lem  26264  qqhcn  26274  pwsiga  26427  prsiga  26428  measle0  26476  mbfmcst  26528  1stmbfm  26529  2ndmbfm  26530  imambfm  26531  cnmbfm  26532  mbfmco  26533  mbfmco2  26534  oddpwdc  26585  eulerpartlemgs2  26611  0rrv  26682  ballotlemfc0  26723  ballotlemfcc  26724  lgamgulmlem5  26867  lgambdd  26871  derangen  26908  subfacval3  26925  cvmseu  27013  cvmliftmolem2  27019  cvmliftlem7  27028  cvmliftlem15  27035  cvmlift2lem9a  27040  cvmlift2lem9  27048  cvmlift2lem10  27049  cvmlift2lem11  27050  cvmlift2lem12  27051  cvmlift3lem6  27061  cvmlift3lem8  27063  wsuclem  27609  supaddc  28261  supadd  28262  mblfinlem2  28273  ovoliunnfl  28277  volsupnfl  28280  mbfresfi  28282  dvtanlem  28285  itg2addnclem2  28288  iblabsnc  28300  iblmulc2nc  28301  ftc1cnnclem  28309  ftc1cnnc  28310  ftc1anc  28319  fness  28398  ssref  28399  fnetr  28402  reftr  28405  fnessref  28409  refssfne  28410  neibastop1  28424  neibastop2  28426  tailfb  28442  filnetlem3  28445  fzadd2  28481  sdclem2  28482  metf1o  28495  ismtyhmeolem  28547  ismtyres  28551  heibor1lem  28552  bfplem2  28566  bfp  28567  rrncmslem  28575  iccbnd  28583  icccmpALT  28584  rngogrphom  28621  rngoisoco  28632  keridl  28676  fzsplit1nn0  28937  icodiamlt  29006  irrapxlem3  29010  irrapxlem4  29011  pell1234qrdich  29047  pell1qr1  29057  pell14qrgap  29061  pellqrexplicit  29063  rmspecfund  29095  fzmaxdif  29169  acongeq  29171  jm2.23  29190  jm3.1  29214  lmhmlnmsplit  29285  hbt  29331  dgrsub2  29336  proot1ex  29414  dvconstbi  29453  ubelsupr  29587  fmul01  29606  fmuldfeq  29609  climsuse  29627  stoweidlem7  29648  stoweidlem13  29654  stoweidlem26  29667  wallispilem3  29708  stirlinglem6  29720  stirlinglem10  29724  wwlktovf1  30098  uvtxnb  30124  usgra2wlkspth  30144  wlklniswwlkn1  30179  vfwlkniswwlkn  30186  usg2wlkeq2  30187  wwlknred  30201  wwlknredwwlkn0  30205  clwwlkel  30301  wwlkext2clwwlk  30311  clwwnisshclwwn  30319  clwlkf1clwwlk  30369  0egra0rgra  30395  0vgrargra  30396  frgra0v  30431  frgra1v  30436  fmptsnd  30567  rmfsupp  30618  mndpfsupp  30620  scmfsupp  30622  mptcfsupp  30624  lcoel0  30671  lincsumcl  30674  lincscmcl  30675  lcoss  30679  lindsrng01  30711  lincreslvec3  30725  lindssnlvec  30729  mnd1  30730  bnj1452  31745  bj-finsumval0  32159  lsmcv2  32247  lsatcv0  32249  lcvexchlem4  32255  lcvexchlem5  32256  l1cvpat  32272  lfl0f  32287  lfladdcl  32289  lflnegcl  32293  lkrlss  32313  eqlkr  32317  lkrlsp  32320  lkrlsp2  32321  lshpkrcl  32334  lkrin  32382  1cvrjat  32692  llni  32725  llnle  32735  lplni  32749  lplnle  32757  llncvrlpln2  32774  2atmat  32778  lvoli  32792  lplncvrlvol2  32832  elpaddri  33019  paddclN  33059  pclclN  33108  pclfinN  33117  0psubclN  33160  1psubclN  33161  atpsubclN  33162  pmapsubclN  33163  osumclN  33184  pexmidN  33186  pexmidlem6N  33192  lhp2lt  33218  lautcnv  33307  idlaut  33313  lautco  33314  idldil  33331  ldilcnv  33332  ldilco  33333  ltrncnv  33363  idltrn  33367  cdleme16d  33498  cdleme50laut  33764  cdleme50ldil  33765  cdleme50ltrn  33774  ltrnco  33936  dian0  34257  dia0eldmN  34258  dia1eldmN  34259  dialss  34264  diaintclN  34276  docaclN  34342  doca2N  34344  djajN  34355  dibintclN  34385  diblss  34388  dicvaddcl  34408  dicvscacl  34409  dicn0  34410  cdlemn11a  34425  dihord2cN  34439  dihord11b  34440  dihord6apre  34474  dihmeetlem1N  34508  dihglblem5apreN  34509  dihpN  34554  dihjatcclem4  34639  dochkr1  34696  islpoldN  34702  lcfrlem31  34791  mapdpglem18  34907  mapdheq2  34947  mapdheq4  34950  mapdh6aN  34953  hdmap1l6a  35028  hdmap1neglem1N  35046  hdmap14lem4a  35092
  Copyright terms: Public domain W3C validator