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  1935  euequ1  2297  eqssi  3271  dtru  4282  opnzi  4325  so0  4429  we0  4470  ord0  4526  ordon  4656  omssnlim  4752  funi  5366  funcnvsn  5379  fnresi  5443  fn0  5445  f0  5508  fconst  5510  f10  5590  f1o0  5593  f1oi  5594  f1osn  5596  isoid  5913  fo1st  6226  fo2nd  6227  difxp  6240  porpss  6368  iordsmo  6461  tfrlem7  6486  tfr1  6500  frfnom  6534  seqomlem2  6550  oawordeulem  6639  mapsnf1o2  6903  canth2  7102  unfilem2  7212  cantnfvalf  7456  cnfcom3clem  7498  tc2  7517  r111  7537  rankf  7556  cardf2  7666  harcard  7701  r0weon  7730  infxpenc  7735  infxpenc2lem1  7736  alephon  7786  alephf1  7802  alephiso  7815  alephsmo  7819  alephf1ALT  7820  alephfplem4  7824  ackbij1lem17  7952  ackbij1  7954  ackbij2  7959  isfin1-3  8102  fin1a2lem2  8117  fin1a2lem4  8119  axcc2lem  8152  iunfo  8251  smobeth  8298  0tsk  8467  1pi  8597  nqerf  8644  axaddf  8857  axmulf  8858  axicn  8862  mulnzcnopr  9504  negiso  9820  dfnn2  9849  nnind  9854  0z  10127  dfuzi  10194  cnref1o  10441  elrpii  10449  om2uzf1oi  11108  om2uzisoi  11109  uzrdgfni  11113  expcl2lem  11208  expclzlem  11220  expge0  11231  expge1  11232  faclbnd4lem1  11399  hashkf  11432  sqrf  11943  fclim  12123  fsumge0  12350  eff2  12476  reeff1  12497  ef01bndlem  12561  sin01bnd  12562  cos01bnd  12563  sin01gt0  12567  egt2lt3  12581  qnnen  12589  ruc  12618  divalglem2  12691  divalglem9  12697  bitsf1  12734  sadaddlem  12754  2prm  12871  3prm  12872  1arith  13071  prmlem1a  13205  setsnid  13285  xpsff1o  13569  dmaf  13980  cdaf  13981  coapm  14002  isdrs2  14172  0pos  14187  isposi  14189  islati  14257  isclati  14318  fpwipodrs  14366  letsr  14448  frmdplusg  14575  odf  14951  efgsfo  15147  efgrelexlemb  15158  isabli  15202  mgpf  15451  prdscrngd  15495  xrs1cmn  16517  xrge0subm  16518  rege0subm  16534  zrngunit  16544  zlpir  16550  zzngim  16612  pjpm  16714  istpsi  16788  0cmp  17227  cmpfi  17241  indiscon  17250  kqf  17544  ptcmpfi  17610  fbssfi  17634  zfbas  17693  alexsubALTlem2  17844  alexsubALTlem4  17846  ptcmplem2  17849  ptcmp  17854  prdstmdd  17908  tsmsfbas  17912  ismeti  17992  prdsxmslem2  18177  retpsOLD  18375  cnfldms  18387  cnnrg  18392  tgqioo  18408  xrtgioo  18414  recld2  18422  xrge0gsumle  18441  xrge0tsms  18442  addcnlem  18471  divcn  18475  abscncf  18508  recncf  18509  imcncf  18510  cjcncf  18511  icopnfhmeo  18545  xrhmeo  18548  cnllycmp  18558  cncms  18878  ovolf  18945  ovolicc1  18979  ovolre  18988  ioorf  19032  opnmblALT  19062  itg2const2  19200  itg2splitlem  19207  itg2split  19208  itg2gt0  19219  itg2cnlem1  19220  itg2cnlem2  19221  itg2cn  19222  iblss  19263  itgle  19268  itgeqa  19272  ibladdlem  19278  itgaddlem1  19281  iblabslem  19286  iblabs  19287  iblabsr  19288  iblmulc2  19289  itgmulc2lem1  19290  bddmulibl  19297  itggt0  19300  itgcn  19301  dveflem  19430  mdegxrf  19558  iaa  19809  ulmdm  19876  dvradcnv  19904  reeff1o  19930  reefiso  19931  reefgim  19933  recosf1o  20004  efifo  20016  logcn  20105  cxpcn3  20199  resqrcn  20200  ressatans  20341  efrlim  20375  efnnfsumcl  20452  efchtdvds  20509  ppiub  20555  lgslem2  20648  lgsfcl2  20653  lgsne0  20684  padicabvf  20892  ex-pss  20927  ex-fl  20946  isgrpoi  20977  grporn  20991  isabloi  21067  issubgoi  21089  ablomul  21134  mulid  21135  cnrngo  21182  smcnlem  21384  lnocoi  21449  cncph  21511  cnbn  21562  cnchl  21609  norm3adifii  21841  hhph  21871  hhhl  21897  hlim0  21929  hlimf  21931  helch  21937  hsn0elch  21941  hhssnv  21955  hhshsslem2  21959  hhssbn  21971  hhsshl  21972  shscli  22010  shintcli  22022  chintcli  22024  shsval2i  22080  pjhthlem2  22085  lejdii  22231  nonbooli  22344  pjrni  22395  pjfoi  22396  pjfi  22397  pjmf1  22409  df0op2  22446  idunop  22672  0cnop  22673  0cnfn  22674  idcnop  22675  idhmop  22676  0hmop  22677  0lnfn  22679  0bdop  22687  lnophsi  22695  lnopcoi  22697  lnopunii  22706  lnophmi  22712  nmcopex  22723  nmcoplb  22724  nmcfnex  22747  nmcfnlb  22748  imaelshi  22752  nlelshi  22754  nlelchi  22755  riesz4i  22757  riesz4  22758  riesz1  22759  cnlnadjlem6  22766  cnlnadjlem9  22769  cnlnadjeui  22771  cnlnadjeu  22772  nmopadji  22784  bdophsi  22790  bdopcoi  22792  nmopcoadji  22795  pjhmopi  22840  pjbdlni  22843  hmopidmchi  22845  mdslj1i  23013  xrge00  23400  xrge0tsmsd  23415  refld  23441  xrge0pluscn  23482  qqhval2lem  23638  rnlogblem  23665  logb1  23669  indf1ofs  23689  esum0  23710  esumpcvgval  23734  esumcvg  23742  measdivcstOLD  23842  measdivcst  23843  coinfliprv  23989  lgamcvg2  24088  lgam1  24097  gam1  24098  indispcon  24169  cnllyscon  24180  rellyscon  24186  umgrabi  24311  konigsberg  24315  ghomsn  24399  gamma1  24645  soseq  24812  wfrlem11  24824  wfr1  24830  frrlem5c  24845  bdayfo  24887  bdayfn  24891  brbigcup  24996  fobigcup  24998  brsingle  25014  fnsingle  25016  brimage  25023  funimage  25025  fnimage  25026  imageval  25027  brcart  25029  brapply  25035  brcup  25036  brcap  25037  funpartfun  25040  axlowdimlem16  25144  axlowdimlem17  25145  onsucconi  25435  onsucsuccmpi  25441  itg2gt0cn  25495  ibladdnclem  25496  itgaddnclem1  25498  iblabsnclem  25503  iblabsnc  25504  iblmulc2nc  25505  itgmulc2nclem1  25506  bddiblnc  25510  itggt0cn  25512  areacirc  25523  comppfsc  25631  0totbnd  25820  heiborlem6  25863  mzpclall  26128  jm2.20nn  26413  dfacbasgrp  26596  dgraaf  26675  cnmsgngrp  26759  iso0  26859  dvsid  26871  injresinj  27465  usgraexvlem  27568  wlkntrllem4  27704  bnj906  28724  ax12olem4wAUX7  28881  ax12olem4OLD7  29108  isopiN  29440  isolatiN  29475  isomliN  29498  ishlatiN  29614
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