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

Theorem mpbir2an 888
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 886 . 2  |-  ( ph  <->  ch )
51, 4mpbir 202 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  3pm3.2i  1133  ax12olem4OLD  2015  euequ1  2371  eqssi  3366  dtru  4393  opnzi  4436  so0  4539  we0  4580  ord0  4636  ordon  4766  omssnlim  4862  funi  5486  funcnvsn  5499  fnresi  5565  fn0  5567  f0  5630  fconst  5632  f10  5712  f1o0  5715  f1oi  5716  f1osn  5718  isoid  6052  fo1st  6369  fo2nd  6370  difxp  6383  porpss  6529  iordsmo  6622  tfrlem7  6647  tfr1  6661  frfnom  6695  seqomlem2  6711  oawordeulem  6800  mapsnf1o2  7064  canth2  7263  unfilem2  7375  cantnfvalf  7623  cnfcom3clem  7665  tc2  7684  r111  7704  rankf  7723  cardf2  7835  harcard  7870  r0weon  7899  infxpenc  7904  infxpenc2lem1  7905  alephon  7955  alephf1  7971  alephiso  7984  alephsmo  7988  alephf1ALT  7989  alephfplem4  7993  ackbij1lem17  8121  ackbij1  8123  ackbij2  8128  isfin1-3  8271  fin1a2lem2  8286  fin1a2lem4  8288  axcc2lem  8321  iunfo  8419  smobeth  8466  0tsk  8635  1pi  8765  nqerf  8812  axaddf  9025  axmulf  9026  axicn  9030  mulnzcnopr  9673  negiso  9989  dfnn2  10018  nnind  10023  0z  10298  dfuzi  10365  cnref1o  10612  elrpii  10620  injresinj  11205  om2uzf1oi  11298  om2uzisoi  11299  uzrdgfni  11303  expcl2lem  11398  expclzlem  11410  expge0  11421  expge1  11422  faclbnd4lem1  11589  hashkf  11625  sqrf  12172  fclim  12352  fsumge0  12579  eff2  12705  reeff1  12726  ef01bndlem  12790  sin01bnd  12791  cos01bnd  12792  sin01gt0  12796  egt2lt3  12810  qnnen  12818  ruc  12847  divalglem2  12920  divalglem9  12926  bitsf1  12963  sadaddlem  12983  2prm  13100  3prm  13101  1arith  13300  prmlem1a  13434  setsnid  13514  xpsff1o  13798  dmaf  14209  cdaf  14210  coapm  14231  isdrs2  14401  0pos  14416  isposi  14418  islati  14486  isclati  14547  fpwipodrs  14595  letsr  14677  frmdplusg  14804  odf  15180  efgsfo  15376  efgrelexlemb  15387  isabli  15431  mgpf  15680  prdscrngd  15724  xrs1cmn  16743  xrge0subm  16744  rege0subm  16760  zrngunit  16770  zlpir  16776  zzngim  16838  pjpm  16940  istpsi  17014  0cmp  17462  cmpfi  17476  indiscon  17486  kqf  17784  ptcmpfi  17850  fbssfi  17874  zfbas  17933  alexsubALTlem2  18084  alexsubALTlem4  18086  ptcmplem2  18089  ptcmp  18094  prdstmdd  18158  tsmsfbas  18162  ismeti  18360  prdsxmslem2  18564  retpsOLD  18803  cnfldms  18815  cnnrg  18820  tgqioo  18836  xrtgioo  18842  recld2  18850  xrge0gsumle  18869  xrge0tsms  18870  addcnlem  18899  divcn  18903  abscncf  18936  recncf  18937  imcncf  18938  cjcncf  18939  icopnfhmeo  18973  xrhmeo  18976  cnllycmp  18986  cncms  19314  ovolf  19383  ovolicc1  19417  ovolre  19426  ioorf  19470  opnmblALT  19500  itg2const2  19636  itg2splitlem  19643  itg2split  19644  itg2gt0  19655  itg2cnlem1  19656  itg2cnlem2  19657  itg2cn  19658  iblss  19699  itgle  19704  itgeqa  19708  ibladdlem  19714  itgaddlem1  19717  iblabslem  19722  iblabs  19723  iblabsr  19724  iblmulc2  19725  itgmulc2lem1  19726  bddmulibl  19733  itggt0  19736  itgcn  19737  dveflem  19868  mdegxrf  19996  iaa  20247  ulmdm  20314  dvradcnv  20342  reeff1o  20368  reefiso  20369  reefgim  20371  recosf1o  20442  efifo  20454  logcn  20543  cxpcn3  20637  resqrcn  20638  ressatans  20779  efrlim  20813  efnnfsumcl  20890  efchtdvds  20947  ppiub  20993  lgslem2  21086  lgsfcl2  21091  lgsne0  21122  padicabvf  21330  usgraexvlem  21419  wlkntrllem2  21565  umgrabi  21710  konigsberg  21714  ex-pss  21741  ex-fl  21760  isgrpoi  21791  grporn  21805  isabloi  21881  issubgoi  21903  ablomul  21948  mulid  21949  cnrngo  21996  smcnlem  22198  lnocoi  22263  cncph  22325  cnbn  22376  cnchl  22423  norm3adifii  22655  hhph  22685  hhhl  22711  hlim0  22743  hlimf  22745  helch  22751  hsn0elch  22755  hhssnv  22769  hhshsslem2  22773  hhssbn  22785  hhsshl  22786  shscli  22824  shintcli  22836  chintcli  22838  shsval2i  22894  pjhthlem2  22899  lejdii  23045  nonbooli  23158  pjrni  23209  pjfoi  23210  pjfi  23211  pjmf1  23223  df0op2  23260  idunop  23486  0cnop  23487  0cnfn  23488  idcnop  23489  idhmop  23490  0hmop  23491  0lnfn  23493  0bdop  23501  lnophsi  23509  lnopcoi  23511  lnopunii  23520  lnophmi  23526  nmcopex  23537  nmcoplb  23538  nmcfnex  23561  nmcfnlb  23562  imaelshi  23566  nlelshi  23568  nlelchi  23569  riesz4i  23571  riesz4  23572  riesz1  23573  cnlnadjlem6  23580  cnlnadjlem9  23583  cnlnadjeui  23585  cnlnadjeu  23586  nmopadji  23598  bdophsi  23604  bdopcoi  23606  nmopcoadji  23609  pjhmopi  23654  pjbdlni  23657  hmopidmchi  23659  mdslj1i  23827  rinvf1o  24047  xrstos  24206  xrsclat  24207  xrge00  24213  xrge0tsmsd  24228  retos  24283  refld  24284  xrge0iifmhm  24330  xrge0pluscn  24331  qqhval2lem  24370  rnlogblem  24404  logb1  24408  esum0  24449  esumcst  24460  esumpcvgval  24473  esumcvg  24481  dmvlsiga  24517  measdivcstOLD  24583  coinfliprv  24745  ballotlem2  24751  ballotlemfc0  24755  ballotlemfcc  24756  lgamcvg2  24844  lgam1  24853  gam1  24854  indispcon  24926  cnllyscon  24937  rellyscon  24943  ghomsn  25104  soseq  25534  wfrlem11  25553  wfr1  25559  frrlem5c  25593  bdayfo  25635  bdayfn  25639  brbigcup  25748  fobigcup  25750  brsingle  25767  fnsingle  25769  brimage  25776  funimage  25778  fnimage  25779  imageval  25780  brcart  25782  brapply  25788  brcup  25789  brcap  25790  funpartfun  25793  brub  25804  axlowdimlem16  25901  axlowdimlem17  25902  onsucconi  26192  onsucsuccmpi  26198  mblfinlem2  26256  itg2gt0cn  26274  ibladdnclem  26275  itgaddnclem1  26277  iblabsnclem  26282  iblabsnc  26283  iblmulc2nc  26284  itgmulc2nclem1  26285  bddiblnc  26289  itggt0cn  26291  ftc1anclem7  26300  ftc1anclem8  26301  areacirc  26311  comppfsc  26401  0totbnd  26496  heiborlem6  26539  mzpclall  26798  jm2.20nn  27082  dfacbasgrp  27264  dgraaf  27343  cnmsgngrp  27427  iso0  27527  dvsid  27539  abnotbtaxb  27874  bnj906  29375  ax12olem4wAUX7  29532  ax12olem4OLD7  29781  isopiN  30053  isolatiN  30088  isomliN  30111  ishlatiN  30227
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 179  df-an 362
  Copyright terms: Public domain W3C validator