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

Theorem mpbir2an 886
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
Hypotheses
Ref Expression
mpbir2an.1  |-  ps
mpbir2an.2  |-  ch
mpbiran2an.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
mpbir2an  |-  ph

Proof of Theorem mpbir2an
StepHypRef Expression
1 mpbir2an.2 . 2  |-  ch
2 mpbir2an.1 . . 3  |-  ps
3 mpbiran2an.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
42, 3mpbiran 884 . 2  |-  ( ph  <->  ch )
51, 4mpbir 200 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  3pm3.2i  1130  ax12olem4  1871  euequ1  2231  eqssi  3195  dtru  4201  opnzi  4243  so0  4347  we0  4388  ord0  4444  ordon  4574  omssnlim  4670  funi  5284  funcnvsn  5297  fnresi  5361  fn0  5363  f0  5425  fconst  5427  f10  5507  f1o0  5510  f1oi  5511  f1osn  5513  isoid  5826  fo1st  6139  fo2nd  6140  difxp  6153  porpss  6281  iordsmo  6374  tfrlem7  6399  tfr1  6413  frfnom  6447  seqomlem2  6463  oawordeulem  6552  mapsnf1o2  6815  canth2  7014  unfilem2  7122  cantnfvalf  7366  cnfcom3clem  7408  tc2  7427  r111  7447  rankf  7466  cardf2  7576  harcard  7611  r0weon  7640  infxpenc  7645  infxpenc2lem1  7646  alephon  7696  alephf1  7712  alephiso  7725  alephsmo  7729  alephf1ALT  7730  alephfplem4  7734  ackbij1lem17  7862  ackbij1  7864  ackbij2  7869  isfin1-3  8012  fin1a2lem2  8027  fin1a2lem4  8029  axcc2lem  8062  iunfo  8161  smobeth  8208  0tsk  8377  1pi  8507  nqerf  8554  axaddf  8767  axmulf  8768  axicn  8772  mulnzcnopr  9414  negiso  9730  dfnn2  9759  nnind  9764  0z  10035  dfuzi  10102  cnref1o  10349  elrpii  10357  om2uzf1oi  11016  om2uzisoi  11017  uzrdgfni  11021  expcl2lem  11115  expclzlem  11127  expge0  11138  expge1  11139  faclbnd4lem1  11306  hashkf  11339  sqrf  11847  fclim  12027  fsumge0  12253  eff2  12379  reeff1  12400  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  sin01gt0  12470  egt2lt3  12484  qnnen  12492  ruc  12521  divalglem2  12594  divalglem9  12600  bitsf1  12637  sadaddlem  12657  2prm  12774  3prm  12775  1arith  12974  prmlem1a  13108  setsnid  13188  xpsff1o  13470  dmaf  13881  cdaf  13882  coapm  13903  isdrs2  14073  0pos  14088  isposi  14090  islati  14158  isclati  14219  fpwipodrs  14267  letsr  14349  frmdplusg  14476  odf  14852  efgsfo  15048  efgrelexlemb  15059  isabli  15103  mgpf  15352  prdscrngd  15396  xrs1cmn  16411  xrge0subm  16412  rege0subm  16428  zrngunit  16438  zlpir  16444  zzngim  16506  pjpm  16608  istpsi  16682  0cmp  17121  cmpfi  17135  indiscon  17144  kqf  17438  ptcmpfi  17504  fbssfi  17532  zfbas  17591  alexsubALTlem2  17742  alexsubALTlem4  17744  ptcmplem2  17747  ptcmp  17752  prdstmdd  17806  tsmsfbas  17810  ismeti  17890  prdsxmslem2  18075  retpsOLD  18273  cnfldms  18285  cnnrg  18290  tgqioo  18306  xrtgioo  18312  recld2  18320  xrge0gsumle  18338  xrge0tsms  18339  addcnlem  18368  divcn  18372  abscncf  18405  recncf  18406  imcncf  18407  cjcncf  18408  icopnfhmeo  18441  xrhmeo  18444  cnllycmp  18454  cncms  18774  ovolf  18841  ovolicc1  18875  ovolre  18884  ioorf  18928  opnmblALT  18958  itg2const2  19096  itg2splitlem  19103  itg2split  19104  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  itg2cn  19118  iblss  19159  itgle  19164  itgeqa  19168  ibladdlem  19174  itgaddlem1  19177  iblabslem  19182  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgmulc2lem1  19186  bddmulibl  19193  itggt0  19196  itgcn  19197  dveflem  19326  mdegxrf  19454  iaa  19705  dvradcnv  19797  reeff1o  19823  reefiso  19824  reefgim  19826  recosf1o  19897  efifo  19909  logcn  19994  cxpcn3  20088  resqrcn  20089  ressatans  20230  efrlim  20264  efnnfsumcl  20340  efchtdvds  20397  ppiub  20443  lgslem2  20536  lgsfcl2  20541  lgsne0  20572  padicabvf  20780  ex-pss  20815  ex-fl  20834  isgrpoi  20865  grporn  20879  isabloi  20955  issubgoi  20977  ablomul  21022  mulid  21023  cnrngo  21070  smcnlem  21270  lnocoi  21335  cncph  21397  cnbn  21448  cnchl  21495  norm3adifii  21727  hhph  21757  hhhl  21783  hlim0  21815  hlimf  21817  helch  21823  hsn0elch  21827  hhssnv  21841  hhshsslem2  21845  hhssbn  21857  hhsshl  21858  shscli  21896  shintcli  21908  chintcli  21910  shsval2i  21966  pjhthlem2  21971  lejdii  22117  nonbooli  22230  pjrni  22281  pjfoi  22282  pjfi  22283  pjmf1  22295  df0op2  22332  idunop  22558  0cnop  22559  0cnfn  22560  idcnop  22561  idhmop  22562  0hmop  22563  0lnfn  22565  0bdop  22573  lnophsi  22581  lnopcoi  22583  lnopunii  22592  lnophmi  22598  nmcopex  22609  nmcoplb  22610  nmcfnex  22633  nmcfnlb  22634  imaelshi  22638  nlelshi  22640  nlelchi  22641  riesz4i  22643  riesz4  22644  riesz1  22645  cnlnadjlem6  22652  cnlnadjlem9  22655  cnlnadjeui  22657  cnlnadjeu  22658  nmopadji  22670  bdophsi  22676  bdopcoi  22678  nmopcoadji  22681  pjhmopi  22726  pjbdlni  22729  hmopidmchi  22731  mdslj1i  22899  xrge00  23311  xrge0pluscn  23322  xrge0tsmsd  23382  rnlogblem  23401  logb1  23405  esum0  23428  esumpcvgval  23446  esumcvg  23454  measdivcstOLD  23551  measdivcst  23552  indf1ofs  23609  coinfliprv  23683  indispcon  23765  cnllyscon  23776  rellyscon  23782  umgrabi  23907  konigsberg  23911  ghomsn  23995  soseq  24254  wfrlem11  24266  wfr1  24272  frrlem5c  24287  bdayfo  24329  bdayfn  24333  brbigcup  24438  fobigcup  24440  brsingle  24456  fnsingle  24458  brimage  24465  funimage  24467  fnimage  24468  imageval  24469  brcart  24471  brapply  24477  brcup  24478  brcap  24479  funpartfun  24481  axlowdimlem16  24585  axlowdimlem17  24586  onsucconi  24876  onsucsuccmpi  24882  areacirc  24931  vxveqv  25054  zintdom  25438  indcomp  25589  1alg  25722  1ded  25738  0alg  25756  0ded  25757  0catOLD  25758  1cat  25759  pgapspf  26052  comppfsc  26307  0totbnd  26497  heiborlem6  26540  mzpclall  26805  jm2.20nn  27090  dfacbasgrp  27273  dgraaf  27352  cnmsgngrp  27436  iso0  27536  dvsid  27548  usgraexvlem  28127  bnj906  28962  isopiN  29371  isolatiN  29406  isomliN  29429  ishlatiN  29545
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