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

Theorem mpbir2and 889
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 519 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 224 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  fnpr  5950  fnprOLD  5951  dffi3  7436  supmax  7470  suppr  7473  ordtypelem7  7493  cantnfle  7626  cantnf0  7630  cantnfp1lem1  7634  cantnfp1lem2  7635  cantnfp1lem3  7636  oemapvali  7640  cantnflem1a  7641  cantnflem1c  7643  cantnflem1d  7644  cantnflem1  7645  cantnf  7649  mapfien  7653  rankpwi  7749  carduni  7868  fin23lem32  8224  fpwwe2lem6  8510  fpwwe2lem9  8513  fpwwe2lem12  8516  fpwwe2lem13  8517  fpwwe2  8518  inttsk  8649  grutsk1  8696  add20  9540  supmul  9976  suprzcl  10349  uzwo3  10569  rpnnen1lem5  10604  xrre  10757  xrre3  10759  xleadd1a  10832  xlemul1a  10867  supxrre  10906  infmxrre  10914  ixxub  10937  ixxlb  10938  elioc2  10973  elico2  10974  elicc2  10975  elfz1eq  11068  nn0fz0  11114  fzctr  11117  fzoaddel  11175  flid  11216  flval3  11222  fladdz  11227  fldiv  11241  modid  11270  seqf1olem1  11362  bcval5  11609  hashf1lem1  11704  sqeqd  11971  sqrlem7  12054  max0add  12115  abs2difabs  12138  rddif  12144  fzomaxdiflem  12146  rexico  12157  limsupgre  12275  rlim3  12292  icco1  12334  rlimclim  12340  rlimuni  12344  rlimresb  12359  isercolllem2  12459  isercolllem3  12460  isercoll  12461  caucvgrlem  12466  caurcvgr  12467  iseraltlem3  12477  fsum00  12577  o1fsum  12592  dvdseq  12897  bitsfzolem  12946  bitsfzo  12947  bitsmod  12948  bitscmp  12950  gcd0id  13023  gcdneg  13026  bezoutlem4  13041  nn0seqcvgd  13061  prmind2  13090  qredeq  13106  isprm5  13112  hashdvds  13164  eulerthlem2  13171  pcpremul  13217  pcidlem  13245  pcgcd1  13250  pcadd2  13259  fldivp1  13266  pcfaclem  13267  prmreclem5  13288  4sqlem17  13329  vdwlem1  13349  vdwlem6  13354  vdwlem12  13360  vdwlem13  13361  0ram  13388  ram0  13390  ramub1lem1  13394  invco  13996  sectmon  14003  monsect  14004  ssctr  14025  ssceq  14026  issubc3  14046  fullsubc  14047  funcinv  14070  fthmon  14124  fuccocl  14161  fucidcl  14162  invfuc  14171  elhomai  14188  setcmon  14242  setcepi  14243  catcisolem  14261  curf2cl  14328  yonedalem4c  14374  yonedalem3  14377  yoniso  14382  isacs3lem  14592  tsrdir  14683  nmznsg  14984  ghmpreima  15027  ghmeql  15028  ghmnsgpreima  15030  cntzsubm  15134  cntzsubg  15135  cntzmhm  15137  odlem2  15177  gexlem2  15216  gexcl2  15223  sylow1lem5  15236  subgslw  15250  slwhash  15258  fislw  15259  sylow3lem1  15261  lsmsubg  15288  efgredlemd  15376  efgredlem  15379  efgcpbllemb  15387  frgpuplem  15404  cyggeninv  15493  iscygd  15497  iscygodd  15498  gsumconst  15532  gsumpt  15545  dprdfcntz  15573  eldprdi  15576  subgdmdprd  15592  subgdprd  15593  dprdpr  15608  ablfac1c  15629  ablfac1eu  15631  ablfaclem3  15645  issubdrg  15893  rhmeql  15898  rhmima  15899  cntzsubr  15900  isabvd  15908  abvdiv  15925  lsslsp  16091  lmhmima  16123  lmhmpreima  16124  lmhmeql  16131  lsmcl  16155  lspfixed  16200  issubassa  16383  issubassa2  16403  psrbaglesupp  16433  psrbaglecl  16434  psrbagaddcl  16435  psrbagcon  16436  psrbas  16443  psrlidm  16467  psrridm  16468  mvridlem  16483  mplsubglem  16498  mpllsslem  16499  mplassa  16517  subrgmpl  16523  mplcoe3  16529  mplcoe2  16530  mplbas2  16531  mplind  16562  ply1assa  16597  coe1tmmul2  16668  coe1tmmul  16669  qsssubdrg  16758  gzrngunit  16764  ocvpj  16944  distop  17060  indistopon  17065  ppttop  17071  epttop  17073  mretopd  17156  toponmre  17157  neiss  17173  opnneissb  17178  ssnei2  17180  innei  17189  neiptoptop  17195  ordtcld1  17261  ordtcld2  17262  lmconst  17325  cnpnei  17328  iscncl  17333  cnss1  17340  cnss2  17341  cncnpi  17342  cncnp  17344  cnconst2  17347  cnrest  17349  cnpresti  17352  cnpdis  17357  paste  17358  lmcnp  17368  cnhaus  17418  hauscmp  17470  2ndcomap  17521  1stcelcls  17524  1stccnp  17525  llyrest  17548  nllyrest  17549  llyidm  17551  nllyidm  17552  kgentopon  17570  kgenidm  17579  kgencn3  17590  txcld  17635  neitx  17639  tx1cn  17641  tx2cn  17642  ptcld  17645  xkoccn  17651  txcnp  17652  ptcnp  17654  txcnmpt  17656  ptcn  17659  txdis1cn  17667  ptrescn  17671  txkgen  17684  xkoco1cn  17689  xkoco2cn  17690  xkococn  17692  xkoinjcn  17719  qtoptop2  17731  qtopuni  17734  qtopid  17737  qtopkgen  17742  basqtop  17743  tgqtop  17744  qtopss  17747  qtopeu  17748  qtoprest  17749  kqopn  17766  kqcld  17767  kqreglem2  17774  reghmph  17825  ordthmeolem  17833  qtopf1  17848  opnfbas  17874  isfil2  17888  fbasweak  17897  fsubbas  17899  filcon  17915  fbasrn  17916  rnelfmlem  17984  flimss2  18004  flimss1  18005  hausflim  18013  flimclslem  18016  flimsncls  18018  cnpflfi  18031  flfcnp2  18039  fclsfnflim  18059  cnextfvval  18096  cnextfres  18099  symgtgp  18131  opnsubg  18137  ghmcnp  18144  divstgpopn  18149  divstgplem  18150  divstgphaus  18152  tsmsfbas  18157  ustfilxp  18242  utoptop  18264  utopbas  18265  restutopopn  18268  iducn  18313  cstucnd  18314  ucncn  18315  fmucnd  18322  cfilufg  18323  trcfilu  18324  cfiluweak  18325  neipcfilu  18326  psmetsym  18341  isxmetd  18356  xmetsym  18377  imasdsf1olem  18403  imasf1oxmet  18405  xblss2ps  18431  xblss2  18432  xblcntrps  18440  xblcntr  18441  blcld  18535  metustfbasOLD  18595  metustfbas  18596  cfilucfilOLD  18599  cfilucfil  18600  restmetu  18617  ngptgp  18677  tngngpd  18694  tngnrg  18710  nlmvscn  18723  nrginvrcn  18727  nmo0  18769  nmoeq0  18770  nmoid  18776  nghmcn  18779  0nmhm  18789  blcvx  18829  zcld  18844  iccntr  18852  xrge0tsms  18865  xmetdcn2  18868  metdstri  18881  metdscn  18886  rescncf  18927  cncfco  18937  oprpiece1res2  18977  cnheibor  18980  cnllycmp  18981  bndth  18983  evth  18984  ishtpyd  19000  isphtpyd  19011  pcoval2  19041  nmhmcn  19128  ipcn  19200  lmnn  19216  cfilss  19223  iscfil3  19226  cfilfcls  19227  cmetcaulem  19241  iscmet3lem2  19245  cfilres  19249  lmcau  19265  flimcfil  19266  cncmet  19275  rlmbn  19315  minveclem3b  19329  pjthlem1  19338  pjth2  19341  ivthlem3  19350  ovolssnul  19383  ovolctb  19386  ovolunnul  19396  ovoliunnul  19403  ovolsca  19411  ovolicc  19419  ovolicopnf  19420  voliunlem2  19445  voliunlem3  19446  volsup  19450  uniioovol  19471  uniiccvol  19472  dyadmaxlem  19489  vitalilem5  19504  ismbfd  19532  mbfres  19536  mbfss  19538  mbfmulc2re  19540  mbfadd  19553  mbfmulc2  19555  mbflimsup  19558  mbflim  19560  i1faddlem  19585  i1fmullem  19586  mbfmul  19618  itg2itg1  19628  itg2seq  19634  itg2eqa  19637  itg2mulc  19639  itg2split  19641  itg2mono  19645  itg2cnlem1  19653  ibl0  19678  iblposlem  19683  itgreval  19688  iblneg  19694  iblss  19696  iblss2  19697  itgle  19701  iblconst  19709  iblabs  19720  iblabsr  19721  iblmulc2  19722  bddmulibl  19730  limciun  19781  limcun  19782  dvres2lem  19797  dvidlem  19802  dvcnp2  19806  dvcn  19807  cpnres  19823  dvaddbr  19824  dvmulbr  19825  dvcobr  19832  dvcjbr  19835  dvrec  19841  dvcnvlem  19860  dvferm  19872  dvlip2  19879  dveq0  19884  dv11cn  19885  dvivthlem1  19892  lhop1  19898  lhop2  19899  lhop  19900  dvcnvre  19903  dvfsumlem3  19912  dvfsumlem4  19913  dvfsumrlim  19915  dvfsum2  19918  ftc1a  19921  ftc1lem4  19923  ftc1lem6  19925  ftc1  19926  evlslem3  19935  mpfind  19965  coe1mul3  20022  deg1addle2  20025  deg1add  20026  deg1sublt  20033  deg1mul2  20037  deg1tm  20041  fta1blem  20091  drnguc1p  20093  ig1prsp  20100  plyco0  20111  plyeq0lem  20129  dgrub  20153  dgreq  20163  dgradd2  20186  dgrmul  20188  dgrcolem2  20192  dgrco  20193  plycpn  20206  plydivlem4  20213  plydiveu  20215  vieta1lem2  20228  vieta1  20229  aalioulem2  20250  aalioulem3  20251  aaliou3lem7  20266  tayl0  20278  ulmcn  20315  ulmdvlem3  20318  psercn  20342  abelth  20357  pilem3  20369  efif1olem1  20444  abslogimle  20471  argregt0  20505  argrege0  20506  logf1o2  20541  cxpsqrlem  20593  cxpcn3  20632  abscxpbnd  20637  ang180lem2  20652  ang180lem3  20653  logreclem  20660  xrlimcnp  20807  harmonicbnd4  20849  fsumharmonic  20850  basellem3  20865  basellem4  20866  dvdsppwf1o  20971  dvdsflf1o  20972  fsumfldivdiaglem  20974  chpeq0  20992  chteq0  20993  chtub  20996  chpub  21004  dchrelbasd  21023  dchrmulcl  21033  dchrinv  21045  bcmono  21061  bposlem1  21068  bposlem2  21069  lgslem1  21080  lgsdirprm  21113  lgsqrlem2  21126  lgsqrlem3  21127  lgsdchr  21132  lgseisenlem1  21133  lgseisenlem2  21134  lgseisenlem3  21135  lgsquadlem1  21138  2sqlem8  21156  2sqblem  21161  chebbnd1lem1  21163  dchrisumlem1  21183  dchrisumlem2  21184  dchrisumlem3  21185  dchrisum0fno1  21205  pntrmax  21258  pntpbnd1a  21279  pntibndlem3  21286  pntlemn  21294  pntlemi  21298  pntlem3  21303  pntleml  21305  ostth1  21327  ostth2  21331  ostth3  21332  cusgra0v  21469  cusgraexi  21477  cusgrares  21481  1pthon  21591  constr2spth  21600  2pthon  21602  constr3trllem3  21639  constr3cycl  21648  eupares  21697  eupap1  21698  nvabs  22162  vacn  22190  nmcvcn  22191  nmblore  22287  0lno  22291  0blo  22293  nmlno0lem  22294  occl  22806  pjhthlem1  22893  pjpjpre  22921  nmopre  23373  nmlnop0iALT  23498  nmophmi  23534  leoprf2  23630  stlesi  23744  disjdifprg  24017  fzspl  24149  xrge0tsmsd  24223  ofldaddlt  24241  ofldlt1  24243  kerf1hrm  24262  metider  24289  qqhval2lem  24365  qqhcn  24375  pwsiga  24513  prsiga  24514  measle0  24562  mbfmcst  24609  1stmbfm  24610  2ndmbfm  24611  imambfm  24612  cnmbfm  24613  mbfmco  24614  mbfmco2  24615  0rrv  24709  ballotlemfc0  24750  ballotlemfcc  24751  lgamgulmlem5  24817  lgambdd  24821  derangen  24858  subfacval3  24875  cvmseu  24963  cvmliftmolem2  24969  cvmliftlem7  24978  cvmliftlem15  24985  cvmlift2lem9a  24990  cvmlift2lem9  24998  cvmlift2lem10  24999  cvmlift2lem11  25000  cvmlift2lem12  25001  cvmlift3lem6  25011  cvmlift3lem8  25013  fznatpl1  25198  wsuclem  25576  brbtwn2  25844  axlowdimlem3  25883  axlowdimlem16  25896  axcontlem8  25910  supaddc  26237  supadd  26238  mblfinlem2  26244  ovoliunnfl  26248  volsupnfl  26251  mbfresfi  26253  itg2addnclem2  26257  iblabsnc  26269  iblmulc2nc  26270  ftc1cnnclem  26278  ftc1cnnc  26279  ftc1anc  26288  fness  26362  ssref  26363  fnetr  26366  reftr  26369  fnessref  26373  refssfne  26374  neibastop1  26388  neibastop2  26390  tailfb  26406  filnetlem3  26409  fzadd2  26445  sdclem2  26446  metf1o  26461  ismtyhmeolem  26513  ismtyres  26517  heibor1lem  26518  bfplem2  26532  bfp  26533  rrncmslem  26541  iccbnd  26549  icccmpALT  26550  rngogrphom  26587  rngoisoco  26598  keridl  26642  fzsplit1nn0  26812  icodiamlt  26883  irrapxlem3  26887  irrapxlem4  26888  pell1234qrdich  26924  pell1qr1  26934  pell14qrgap  26938  pellqrexplicit  26940  rmspecfund  26972  fzmaxdif  27046  acongeq  27048  jm2.23  27067  jm3.1  27091  lmhmlnmsplit  27162  dsmm0cl  27183  dsmmacl  27184  dsmmsubg  27186  dsmmlss  27187  uvcff  27217  frlmsplit2  27220  lindfrn  27268  f1lindf  27269  lindsss  27271  hbt  27311  dgrsub2  27316  proot1ex  27497  dvconstbi  27528  ubelsupr  27667  fmul01  27686  fmuldfeq  27689  climsuse  27710  stoweidlem7  27732  stoweidlem13  27738  stoweidlem26  27751  wallispilem3  27792  stirlinglem6  27804  stirlinglem10  27808  ubmelfzo  28126  fzo1fzo0n0  28128  cshwlen  28241  2cshw1lem1  28248  3cshw  28269  cshwssizelem1  28280  usgra2wlkspth  28308  0egra0rgra  28375  0vgrargra  28376  frgra0v  28383  frgra1v  28388  bnj1452  29421  lsmcv2  29827  lsatcv0  29829  lcvexchlem4  29835  lcvexchlem5  29836  l1cvpat  29852  lfl0f  29867  lfladdcl  29869  lflnegcl  29873  lkrlss  29893  eqlkr  29897  lkrlsp  29900  lkrlsp2  29901  lshpkrcl  29914  lkrin  29962  1cvrjat  30272  llni  30305  llnle  30315  lplni  30329  lplnle  30337  llncvrlpln2  30354  2atmat  30358  lvoli  30372  lplncvrlvol2  30412  elpaddri  30599  paddclN  30639  pclclN  30688  pclfinN  30697  0psubclN  30740  1psubclN  30741  atpsubclN  30742  pmapsubclN  30743  osumclN  30764  pexmidN  30766  pexmidlem6N  30772  lhp2lt  30798  lautcnv  30887  idlaut  30893  lautco  30894  idldil  30911  ldilcnv  30912  ldilco  30913  ltrncnv  30943  idltrn  30947  cdleme16d  31078  cdleme50laut  31344  cdleme50ldil  31345  cdleme50ltrn  31354  ltrnco  31516  dian0  31837  dia0eldmN  31838  dia1eldmN  31839  dialss  31844  diaintclN  31856  docaclN  31922  doca2N  31924  djajN  31935  dibintclN  31965  diblss  31968  dicvaddcl  31988  dicvscacl  31989  dicn0  31990  cdlemn11a  32005  dihord2cN  32019  dihord11b  32020  dihord6apre  32054  dihmeetlem1N  32088  dihglblem5apreN  32089  dihpN  32134  dihjatcclem4  32219  dochkr1  32276  islpoldN  32282  lcfrlem31  32371  mapdpglem18  32487  mapdheq2  32527  mapdheq4  32530  mapdh6aN  32533  hdmap1l6a  32608  hdmap1neglem1N  32626  hdmap14lem4a  32672
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator