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

Theorem mpbir2and 888
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 518 . 2  |-  ( ph  ->  ( ch  /\  th ) )
4 mpbir2and.3 . 2  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
53, 4mpbird 223 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  dffi3  7184  supmax  7216  suppr  7219  ordtypelem7  7239  cantnfle  7372  cantnf0  7376  cantnfp1lem1  7380  cantnfp1lem2  7381  cantnfp1lem3  7382  oemapvali  7386  cantnflem1a  7387  cantnflem1c  7389  cantnflem1d  7390  cantnflem1  7391  cantnf  7395  mapfien  7399  rankpwi  7495  carduni  7614  fin23lem32  7970  fpwwe2lem6  8257  fpwwe2lem9  8260  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  inttsk  8396  grutsk1  8443  add20  9286  supmul  9722  suprzcl  10091  uzwo3  10311  rpnnen1lem5  10346  xrre  10498  xrre3  10500  xleadd1a  10573  xlemul1a  10608  supxrre  10646  infmxrre  10654  ixxub  10677  ixxlb  10678  elioc2  10713  elico2  10714  elicc2  10715  elfz1eq  10807  fzctr  10854  fzoaddel  10906  flid  10939  flval3  10945  fladdz  10950  fldiv  10964  modid  10993  seqf1olem1  11085  bcval5  11330  hashf1lem1  11393  sqeqd  11651  sqrlem7  11734  max0add  11795  abs2difabs  11818  rddif  11824  fzomaxdiflem  11826  rexico  11837  limsupgre  11955  rlim3  11972  icco1  12014  rlimclim  12020  rlimuni  12024  rlimresb  12039  isercolllem2  12139  isercolllem3  12140  isercoll  12141  caucvgrlem  12145  caurcvgr  12146  iseraltlem3  12156  fsum00  12256  o1fsum  12271  dvdseq  12576  bitsfzolem  12625  bitsfzo  12626  bitsmod  12627  bitscmp  12629  gcd0id  12702  gcdneg  12705  bezoutlem4  12720  nn0seqcvgd  12740  prmind2  12769  qredeq  12785  isprm5  12791  hashdvds  12843  eulerthlem2  12850  pcpremul  12896  pcidlem  12924  pcgcd1  12929  pcadd2  12938  fldivp1  12945  pcfaclem  12946  prmreclem5  12967  4sqlem17  13008  vdwlem1  13028  vdwlem6  13033  vdwlem12  13039  vdwlem13  13040  0ram  13067  ram0  13069  ramub1lem1  13073  invco  13673  sectmon  13680  monsect  13681  ssctr  13702  ssceq  13703  issubc3  13723  fullsubc  13724  funcinv  13747  fthmon  13801  fuccocl  13838  fucidcl  13839  invfuc  13848  elhomai  13865  setcmon  13919  setcepi  13920  catcisolem  13938  curf2cl  14005  yonedalem4c  14051  yonedalem3  14054  yoniso  14059  isacs3lem  14269  tsrdir  14360  nmznsg  14661  ghmpreima  14704  ghmeql  14705  ghmnsgpreima  14707  cntzsubm  14811  cntzsubg  14812  cntzmhm  14814  odlem2  14854  gexlem2  14893  gexcl2  14900  sylow1lem5  14913  subgslw  14927  slwhash  14935  fislw  14936  sylow3lem1  14938  lsmsubg  14965  efgredlemd  15053  efgredlem  15056  efgcpbllemb  15064  frgpuplem  15081  cyggeninv  15170  iscygd  15174  iscygodd  15175  gsumconst  15209  gsumpt  15222  dprdfcntz  15250  eldprdi  15253  subgdmdprd  15269  subgdprd  15270  dprdpr  15285  ablfac1c  15306  ablfac1eu  15308  ablfaclem3  15322  issubdrg  15570  rhmeql  15575  rhmima  15576  cntzsubr  15577  isabvd  15585  abvdiv  15602  lsslsp  15772  lmhmima  15804  lmhmpreima  15805  lmhmeql  15812  lsmcl  15836  lspfixed  15881  issubassa  16064  issubassa2  16084  psrbaglesupp  16114  psrbaglecl  16115  psrbagaddcl  16116  psrbagcon  16117  psrbas  16124  psrlidm  16148  psrridm  16149  mvridlem  16164  mplsubglem  16179  mpllsslem  16180  mplassa  16198  subrgmpl  16204  mplcoe3  16210  mplcoe2  16211  mplbas2  16212  mplind  16243  ply1assa  16278  coe1tmmul2  16352  coe1tmmul  16353  qsssubdrg  16431  gzrngunit  16437  ocvpj  16617  distop  16733  indistopon  16738  ppttop  16744  epttop  16746  mretopd  16829  toponmre  16830  neiss  16846  opnneissb  16851  ssnei2  16853  innei  16862  ordtcld1  16927  ordtcld2  16928  lmconst  16991  cnpnei  16993  iscncl  16998  cnss1  17005  cnss2  17006  cncnpi  17007  cncnp  17009  cnconst2  17011  cnrest  17013  cnpresti  17016  cnpdis  17021  paste  17022  lmcnp  17032  cnhaus  17082  hauscmp  17134  2ndcomap  17184  1stcelcls  17187  1stccnp  17188  llyrest  17211  nllyrest  17212  llyidm  17214  nllyidm  17215  kgentopon  17233  kgenidm  17242  kgencn3  17253  txcld  17298  tx1cn  17303  tx2cn  17304  ptcld  17307  xkoccn  17313  txcnp  17314  ptcnp  17316  txcnmpt  17318  ptcn  17321  txdis1cn  17329  ptrescn  17333  txkgen  17346  xkoco1cn  17351  xkoco2cn  17352  xkococn  17354  xkoinjcn  17381  qtoptop2  17390  qtopuni  17393  qtopid  17396  qtopkgen  17401  basqtop  17402  tgqtop  17403  qtopss  17406  qtopeu  17407  qtoprest  17408  kqopn  17425  kqcld  17426  kqreglem2  17433  reghmph  17484  ordthmeolem  17492  qtopf1  17507  opnfbas  17537  isfil2  17551  fbasweak  17560  fsubbas  17562  filcon  17578  fbasrn  17579  rnelfmlem  17647  flimss2  17667  flimss1  17668  hausflim  17676  flimclslem  17679  flimsncls  17681  cnpflfi  17694  flfcnp2  17702  fclsfnflim  17722  symgtgp  17784  opnsubg  17790  ghmcnp  17797  divstgpopn  17802  divstgplem  17803  divstgphaus  17805  tsmsfbas  17810  isxmetd  17891  xmetsym  17912  imasdsf1olem  17937  imasf1oxmet  17939  xblss2  17958  xblcntr  17963  blcld  18051  ngptgp  18152  tngngpd  18169  tngnrg  18185  nlmvscn  18198  nrginvrcn  18202  nmo0  18244  nmoeq0  18245  nmoid  18251  nghmcn  18254  0nmhm  18264  blcvx  18304  zcld  18319  iccntr  18326  xrge0tsms  18339  xmetdcn2  18342  metdstri  18355  metdscn  18360  rescncf  18401  cncfco  18411  oprpiece1res2  18450  cnheibor  18453  cnllycmp  18454  bndth  18456  evth  18457  ishtpyd  18473  isphtpyd  18484  pcoval2  18514  nmhmcn  18601  ipcn  18673  lmnn  18689  cfilss  18696  iscfil3  18699  cfilfcls  18700  cmetcaulem  18714  iscmet3lem2  18718  cfilres  18722  lmcau  18738  flimcfil  18739  cncmet  18744  rlmbn  18778  minveclem3b  18792  pjthlem1  18801  pjth2  18804  ivthlem3  18813  ovolssnul  18846  ovolctb  18849  ovolunnul  18859  ovoliunnul  18866  ovolsca  18874  ovolicc  18882  ovolicopnf  18883  voliunlem2  18908  voliunlem3  18909  volsup  18913  uniioovol  18934  uniiccvol  18935  dyadmaxlem  18952  vitalilem5  18967  ismbfd  18995  mbfres  18999  mbfss  19001  mbfmulc2re  19003  mbfadd  19016  mbfmulc2  19018  mbflimsup  19021  mbflim  19023  i1faddlem  19048  i1fmullem  19049  mbfmul  19081  itg2itg1  19091  itg2seq  19097  itg2eqa  19100  itg2mulc  19102  itg2split  19104  itg2mono  19108  itg2cnlem1  19116  ibl0  19141  iblposlem  19146  itgreval  19151  iblneg  19157  iblss  19159  iblss2  19160  itgle  19164  iblconst  19172  iblabs  19183  iblabsr  19184  iblmulc2  19185  bddmulibl  19193  limciun  19244  limcun  19245  dvres2lem  19260  dvidlem  19265  dvcnp2  19269  dvcn  19270  cpnres  19286  dvaddbr  19287  dvmulbr  19288  dvcobr  19295  dvcjbr  19298  dvrec  19304  dvcnvlem  19323  dvferm  19335  dvlip2  19342  dveq0  19347  dv11cn  19348  dvivthlem1  19355  lhop1  19361  lhop2  19362  lhop  19363  dvcnvre  19366  dvfsumlem3  19375  dvfsumlem4  19376  dvfsumrlim  19378  dvfsum2  19381  ftc1a  19384  ftc1lem4  19386  ftc1lem6  19388  ftc1  19389  evlslem3  19398  mpfind  19428  coe1mul3  19485  deg1addle2  19488  deg1add  19489  deg1sublt  19496  deg1mul2  19500  deg1tm  19504  fta1blem  19554  drnguc1p  19556  ig1prsp  19563  plyco0  19574  plyeq0lem  19592  dgrub  19616  dgreq  19626  dgradd2  19649  dgrmul  19651  dgrcolem2  19655  dgrco  19656  plycpn  19669  plydivlem4  19676  plydiveu  19678  vieta1lem2  19691  vieta1  19692  aalioulem2  19713  aalioulem3  19714  aaliou3lem7  19729  tayl0  19741  ulmcn  19776  ulmdvlem3  19779  psercn  19802  abelth  19817  pilem3  19829  efif1olem1  19904  argregt0  19964  argrege0  19965  logf1o2  19997  cxpsqrlem  20049  cxpcn3  20088  abscxpbnd  20093  ang180lem2  20108  ang180lem3  20109  logreclem  20116  xrlimcnp  20263  harmonicbnd4  20304  fsumharmonic  20305  basellem3  20320  basellem4  20321  dvdsppwf1o  20426  dvdsflf1o  20427  fsumfldivdiaglem  20429  chpeq0  20447  chteq0  20448  chtub  20451  chpub  20459  dchrelbasd  20478  dchrmulcl  20488  dchrinv  20500  bcmono  20516  bposlem1  20523  bposlem2  20524  lgslem1  20535  lgsdirprm  20568  lgsqrlem2  20581  lgsqrlem3  20582  lgsdchr  20587  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem3  20590  lgsquadlem1  20593  2sqlem8  20611  2sqblem  20616  chebbnd1lem1  20618  dchrisumlem1  20638  dchrisumlem2  20639  dchrisumlem3  20640  dchrisum0fno1  20660  pntrmax  20713  pntpbnd1a  20734  pntibndlem3  20741  pntlemn  20749  pntlemi  20753  pntlem3  20758  pntleml  20760  ostth1  20782  ostth2  20786  ostth3  20787  nvabs  21239  vacn  21267  nmcvcn  21268  nmblore  21364  0lno  21368  0blo  21370  nmlno0lem  21371  occl  21883  pjhthlem1  21970  pjpjpre  21998  nmopre  22450  nmlnop0iALT  22575  nmophmi  22611  leoprf2  22707  stlesi  22821  xrre3FL  23251  xrge0tsmsd  23382  mbfmcst  23564  imambfm  23567  mbfmco  23569  0rrv  23654  derangen  23703  subfacval3  23720  cvmseu  23807  cvmliftmolem2  23813  cvmliftlem7  23822  cvmliftlem15  23829  cvmlift2lem9a  23834  cvmlift2lem9  23842  cvmlift2lem10  23843  cvmlift2lem11  23844  cvmlift2lem12  23845  cvmlift3lem6  23855  cvmlift3lem8  23857  eupares  23899  eupap1  23900  fznatpl1  24093  brbtwn2  24533  axlowdimlem3  24572  axlowdimlem16  24585  axcontlem8  24599  eqfnung2  25118  repfuntw  25160  prltub  25260  ubpar  25261  supaub  25273  geme2  25275  inttop2  25515  intopcoaconb  25540  intopcoaconc  25541  qusp  25542  prcnt  25551  cmptdst  25568  prdnei  25573  tcnvec  25690  aidm2  25750  dualalg  25782  idfisf  25841  idsubfun  25858  setiscat  25979  lppotos  26144  fness  26282  ssref  26283  fnetr  26286  reftr  26289  fnessref  26293  refssfne  26294  neibastop1  26308  neibastop2  26310  tailfb  26326  filnetlem3  26329  fzadd2  26444  sdclem2  26452  metf1o  26469  ismtyhmeolem  26528  ismtyres  26532  heibor1lem  26533  bfplem2  26547  bfp  26548  rrncmslem  26556  iccbnd  26564  icccmpALT  26565  rngogrphom  26602  rngoisoco  26613  keridl  26657  fzsplit1nn0  26833  icodiamlt  26905  irrapxlem3  26909  irrapxlem4  26910  pell1234qrdich  26946  pell1qr1  26956  pell14qrgap  26960  pellqrexplicit  26962  rmspecfund  26994  fzmaxdif  27068  acongeq  27070  jm2.23  27089  jm3.1  27113  lmhmlnmsplit  27185  dsmm0cl  27206  dsmmacl  27207  dsmmsubg  27209  dsmmlss  27210  uvcff  27240  frlmsplit2  27243  lindfrn  27291  f1lindf  27292  lindsss  27294  hbt  27334  dgrsub2  27339  proot1ex  27520  dvconstbi  27551  cusgra0v  28156  frgra0v  28174  frgra1v  28176  bnj1452  29082  lsmcv2  29219  lsatcv0  29221  lcvexchlem4  29227  lcvexchlem5  29228  l1cvpat  29244  lfl0f  29259  lfladdcl  29261  lflnegcl  29265  lkrlss  29285  eqlkr  29289  lkrlsp  29292  lkrlsp2  29293  lshpkrcl  29306  lkrin  29354  1cvrjat  29664  llni  29697  llnle  29707  lplni  29721  lplnle  29729  llncvrlpln2  29746  2atmat  29750  lvoli  29764  lplncvrlvol2  29804  elpaddri  29991  paddclN  30031  pclclN  30080  pclfinN  30089  0psubclN  30132  1psubclN  30133  atpsubclN  30134  pmapsubclN  30135  osumclN  30156  pexmidN  30158  pexmidlem6N  30164  lhp2lt  30190  lautcnv  30279  idlaut  30285  lautco  30286  idldil  30303  ldilcnv  30304  ldilco  30305  ltrncnv  30335  idltrn  30339  cdleme16d  30470  cdleme50laut  30736  cdleme50ldil  30737  cdleme50ltrn  30746  ltrnco  30908  dian0  31229  dia0eldmN  31230  dia1eldmN  31231  dialss  31236  diaintclN  31248  docaclN  31314  doca2N  31316  djajN  31327  dibintclN  31357  diblss  31360  dicvaddcl  31380  dicvscacl  31381  dicn0  31382  cdlemn11a  31397  dihord2cN  31411  dihord11b  31412  dihord6apre  31446  dihmeetlem1N  31480  dihglblem5apreN  31481  dihpN  31526  dihjatcclem4  31611  dochkr1  31668  islpoldN  31674  lcfrlem31  31763  mapdpglem18  31879  mapdheq2  31919  mapdheq4  31922  mapdh6aN  31925  hdmap1l6a  32000  hdmap1neglem1N  32018  hdmap14lem4a  32064
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 177  df-an 360
  Copyright terms: Public domain W3C validator