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

Theorem mpbir2an 887
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 885 . 2  |-  ( ph  <->  ch )
51, 4mpbir 201 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  3pm3.2i  1132  ax12olem4OLD  2014  euequ1  2368  eqssi  3356  dtru  4382  opnzi  4425  so0  4528  we0  4569  ord0  4625  ordon  4755  omssnlim  4851  funi  5475  funcnvsn  5488  fnresi  5554  fn0  5556  f0  5619  fconst  5621  f10  5701  f1o0  5704  f1oi  5705  f1osn  5707  isoid  6041  fo1st  6358  fo2nd  6359  difxp  6372  porpss  6518  iordsmo  6611  tfrlem7  6636  tfr1  6650  frfnom  6684  seqomlem2  6700  oawordeulem  6789  mapsnf1o2  7053  canth2  7252  unfilem2  7364  cantnfvalf  7612  cnfcom3clem  7654  tc2  7673  r111  7693  rankf  7712  cardf2  7822  harcard  7857  r0weon  7886  infxpenc  7891  infxpenc2lem1  7892  alephon  7942  alephf1  7958  alephiso  7971  alephsmo  7975  alephf1ALT  7976  alephfplem4  7980  ackbij1lem17  8108  ackbij1  8110  ackbij2  8115  isfin1-3  8258  fin1a2lem2  8273  fin1a2lem4  8275  axcc2lem  8308  iunfo  8406  smobeth  8453  0tsk  8622  1pi  8752  nqerf  8799  axaddf  9012  axmulf  9013  axicn  9017  mulnzcnopr  9660  negiso  9976  dfnn2  10005  nnind  10010  0z  10285  dfuzi  10352  cnref1o  10599  elrpii  10607  injresinj  11192  om2uzf1oi  11285  om2uzisoi  11286  uzrdgfni  11290  expcl2lem  11385  expclzlem  11397  expge0  11408  expge1  11409  faclbnd4lem1  11576  hashkf  11612  sqrf  12159  fclim  12339  fsumge0  12566  eff2  12692  reeff1  12713  ef01bndlem  12777  sin01bnd  12778  cos01bnd  12779  sin01gt0  12783  egt2lt3  12797  qnnen  12805  ruc  12834  divalglem2  12907  divalglem9  12913  bitsf1  12950  sadaddlem  12970  2prm  13087  3prm  13088  1arith  13287  prmlem1a  13421  setsnid  13501  xpsff1o  13785  dmaf  14196  cdaf  14197  coapm  14218  isdrs2  14388  0pos  14403  isposi  14405  islati  14473  isclati  14534  fpwipodrs  14582  letsr  14664  frmdplusg  14791  odf  15167  efgsfo  15363  efgrelexlemb  15374  isabli  15418  mgpf  15667  prdscrngd  15711  xrs1cmn  16730  xrge0subm  16731  rege0subm  16747  zrngunit  16757  zlpir  16763  zzngim  16825  pjpm  16927  istpsi  17001  0cmp  17449  cmpfi  17463  indiscon  17473  kqf  17771  ptcmpfi  17837  fbssfi  17861  zfbas  17920  alexsubALTlem2  18071  alexsubALTlem4  18073  ptcmplem2  18076  ptcmp  18081  prdstmdd  18145  tsmsfbas  18149  ismeti  18347  prdsxmslem2  18551  retpsOLD  18790  cnfldms  18802  cnnrg  18807  tgqioo  18823  xrtgioo  18829  recld2  18837  xrge0gsumle  18856  xrge0tsms  18857  addcnlem  18886  divcn  18890  abscncf  18923  recncf  18924  imcncf  18925  cjcncf  18926  icopnfhmeo  18960  xrhmeo  18963  cnllycmp  18973  cncms  19301  ovolf  19370  ovolicc1  19404  ovolre  19413  ioorf  19457  opnmblALT  19487  itg2const2  19625  itg2splitlem  19632  itg2split  19633  itg2gt0  19644  itg2cnlem1  19645  itg2cnlem2  19646  itg2cn  19647  iblss  19688  itgle  19693  itgeqa  19697  ibladdlem  19703  itgaddlem1  19706  iblabslem  19711  iblabs  19712  iblabsr  19713  iblmulc2  19714  itgmulc2lem1  19715  bddmulibl  19722  itggt0  19725  itgcn  19726  dveflem  19855  mdegxrf  19983  iaa  20234  ulmdm  20301  dvradcnv  20329  reeff1o  20355  reefiso  20356  reefgim  20358  recosf1o  20429  efifo  20441  logcn  20530  cxpcn3  20624  resqrcn  20625  ressatans  20766  efrlim  20800  efnnfsumcl  20877  efchtdvds  20934  ppiub  20980  lgslem2  21073  lgsfcl2  21078  lgsne0  21109  padicabvf  21317  usgraexvlem  21406  wlkntrllem2  21552  umgrabi  21697  konigsberg  21701  ex-pss  21728  ex-fl  21747  isgrpoi  21778  grporn  21792  isabloi  21868  issubgoi  21890  ablomul  21935  mulid  21936  cnrngo  21983  smcnlem  22185  lnocoi  22250  cncph  22312  cnbn  22363  cnchl  22410  norm3adifii  22642  hhph  22672  hhhl  22698  hlim0  22730  hlimf  22732  helch  22738  hsn0elch  22742  hhssnv  22756  hhshsslem2  22760  hhssbn  22772  hhsshl  22773  shscli  22811  shintcli  22823  chintcli  22825  shsval2i  22881  pjhthlem2  22886  lejdii  23032  nonbooli  23145  pjrni  23196  pjfoi  23197  pjfi  23198  pjmf1  23210  df0op2  23247  idunop  23473  0cnop  23474  0cnfn  23475  idcnop  23476  idhmop  23477  0hmop  23478  0lnfn  23480  0bdop  23488  lnophsi  23496  lnopcoi  23498  lnopunii  23507  lnophmi  23513  nmcopex  23524  nmcoplb  23525  nmcfnex  23548  nmcfnlb  23549  imaelshi  23553  nlelshi  23555  nlelchi  23556  riesz4i  23558  riesz4  23559  riesz1  23560  cnlnadjlem6  23567  cnlnadjlem9  23570  cnlnadjeui  23572  cnlnadjeu  23573  nmopadji  23585  bdophsi  23591  bdopcoi  23593  nmopcoadji  23596  pjhmopi  23641  pjbdlni  23644  hmopidmchi  23646  mdslj1i  23814  rinvf1o  24034  xrstos  24193  xrsclat  24194  xrge00  24200  xrge0tsmsd  24215  retos  24270  refld  24271  xrge0iifmhm  24317  xrge0pluscn  24318  qqhval2lem  24357  rnlogblem  24391  logb1  24395  esum0  24436  esumcst  24447  esumpcvgval  24460  esumcvg  24468  dmvlsiga  24504  measdivcstOLD  24570  coinfliprv  24732  ballotlem2  24738  ballotlemfc0  24742  ballotlemfcc  24743  lgamcvg2  24831  lgam1  24840  gam1  24841  indispcon  24913  cnllyscon  24924  rellyscon  24930  ghomsn  25091  soseq  25521  wfrlem11  25540  wfr1  25546  frrlem5c  25580  bdayfo  25622  bdayfn  25626  brbigcup  25735  fobigcup  25737  brsingle  25754  fnsingle  25756  brimage  25763  funimage  25765  fnimage  25766  imageval  25767  brcart  25769  brapply  25775  brcup  25776  brcap  25777  funpartfun  25780  brub  25791  axlowdimlem16  25888  axlowdimlem17  25889  onsucconi  26179  onsucsuccmpi  26185  mblfinlem  26234  itg2gt0cn  26250  ibladdnclem  26251  itgaddnclem1  26253  iblabsnclem  26258  iblabsnc  26259  iblmulc2nc  26260  itgmulc2nclem1  26261  bddiblnc  26265  itggt0cn  26267  ftc1anclem7  26276  ftc1anclem8  26277  areacirc  26288  comppfsc  26378  0totbnd  26473  heiborlem6  26516  mzpclall  26775  jm2.20nn  27059  dfacbasgrp  27241  dgraaf  27320  cnmsgngrp  27404  iso0  27504  dvsid  27516  abnotbtaxb  27851  bnj906  29238  ax12olem4wAUX7  29395  ax12olem4OLD7  29644  isopiN  29916  isolatiN  29951  isomliN  29974  ishlatiN  30090
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