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  1883  euequ1  2244  eqssi  3208  dtru  4217  opnzi  4259  so0  4363  we0  4404  ord0  4460  ordon  4590  omssnlim  4686  funi  5300  funcnvsn  5313  fnresi  5377  fn0  5379  f0  5441  fconst  5443  f10  5523  f1o0  5526  f1oi  5527  f1osn  5529  isoid  5842  fo1st  6155  fo2nd  6156  difxp  6169  porpss  6297  iordsmo  6390  tfrlem7  6415  tfr1  6429  frfnom  6463  seqomlem2  6479  oawordeulem  6568  mapsnf1o2  6831  canth2  7030  unfilem2  7138  cantnfvalf  7382  cnfcom3clem  7424  tc2  7443  r111  7463  rankf  7482  cardf2  7592  harcard  7627  r0weon  7656  infxpenc  7661  infxpenc2lem1  7662  alephon  7712  alephf1  7728  alephiso  7741  alephsmo  7745  alephf1ALT  7746  alephfplem4  7750  ackbij1lem17  7878  ackbij1  7880  ackbij2  7885  isfin1-3  8028  fin1a2lem2  8043  fin1a2lem4  8045  axcc2lem  8078  iunfo  8177  smobeth  8224  0tsk  8393  1pi  8523  nqerf  8570  axaddf  8783  axmulf  8784  axicn  8788  mulnzcnopr  9430  negiso  9746  dfnn2  9775  nnind  9780  0z  10051  dfuzi  10118  cnref1o  10365  elrpii  10373  om2uzf1oi  11032  om2uzisoi  11033  uzrdgfni  11037  expcl2lem  11131  expclzlem  11143  expge0  11154  expge1  11155  faclbnd4lem1  11322  hashkf  11355  sqrf  11863  fclim  12043  fsumge0  12269  eff2  12395  reeff1  12416  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  sin01gt0  12486  egt2lt3  12500  qnnen  12508  ruc  12537  divalglem2  12610  divalglem9  12616  bitsf1  12653  sadaddlem  12673  2prm  12790  3prm  12791  1arith  12990  prmlem1a  13124  setsnid  13204  xpsff1o  13486  dmaf  13897  cdaf  13898  coapm  13919  isdrs2  14089  0pos  14104  isposi  14106  islati  14174  isclati  14235  fpwipodrs  14283  letsr  14365  frmdplusg  14492  odf  14868  efgsfo  15064  efgrelexlemb  15075  isabli  15119  mgpf  15368  prdscrngd  15412  xrs1cmn  16427  xrge0subm  16428  rege0subm  16444  zrngunit  16454  zlpir  16460  zzngim  16522  pjpm  16624  istpsi  16698  0cmp  17137  cmpfi  17151  indiscon  17160  kqf  17454  ptcmpfi  17520  fbssfi  17548  zfbas  17607  alexsubALTlem2  17758  alexsubALTlem4  17760  ptcmplem2  17763  ptcmp  17768  prdstmdd  17822  tsmsfbas  17826  ismeti  17906  prdsxmslem2  18091  retpsOLD  18289  cnfldms  18301  cnnrg  18306  tgqioo  18322  xrtgioo  18328  recld2  18336  xrge0gsumle  18354  xrge0tsms  18355  addcnlem  18384  divcn  18388  abscncf  18421  recncf  18422  imcncf  18423  cjcncf  18424  icopnfhmeo  18457  xrhmeo  18460  cnllycmp  18470  cncms  18790  ovolf  18857  ovolicc1  18891  ovolre  18900  ioorf  18944  opnmblALT  18974  itg2const2  19112  itg2splitlem  19119  itg2split  19120  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  itg2cn  19134  iblss  19175  itgle  19180  itgeqa  19184  ibladdlem  19190  itgaddlem1  19193  iblabslem  19198  iblabs  19199  iblabsr  19200  iblmulc2  19201  itgmulc2lem1  19202  bddmulibl  19209  itggt0  19212  itgcn  19213  dveflem  19342  mdegxrf  19470  iaa  19721  dvradcnv  19813  reeff1o  19839  reefiso  19840  reefgim  19842  recosf1o  19913  efifo  19925  logcn  20010  cxpcn3  20104  resqrcn  20105  ressatans  20246  efrlim  20280  efnnfsumcl  20356  efchtdvds  20413  ppiub  20459  lgslem2  20552  lgsfcl2  20557  lgsne0  20588  padicabvf  20796  ex-pss  20831  ex-fl  20850  isgrpoi  20881  grporn  20895  isabloi  20971  issubgoi  20993  ablomul  21038  mulid  21039  cnrngo  21086  smcnlem  21286  lnocoi  21351  cncph  21413  cnbn  21464  cnchl  21511  norm3adifii  21743  hhph  21773  hhhl  21799  hlim0  21831  hlimf  21833  helch  21839  hsn0elch  21843  hhssnv  21857  hhshsslem2  21861  hhssbn  21873  hhsshl  21874  shscli  21912  shintcli  21924  chintcli  21926  shsval2i  21982  pjhthlem2  21987  lejdii  22133  nonbooli  22246  pjrni  22297  pjfoi  22298  pjfi  22299  pjmf1  22311  df0op2  22348  idunop  22574  0cnop  22575  0cnfn  22576  idcnop  22577  idhmop  22578  0hmop  22579  0lnfn  22581  0bdop  22589  lnophsi  22597  lnopcoi  22599  lnopunii  22608  lnophmi  22614  nmcopex  22625  nmcoplb  22626  nmcfnex  22649  nmcfnlb  22650  imaelshi  22654  nlelshi  22656  nlelchi  22657  riesz4i  22659  riesz4  22660  riesz1  22661  cnlnadjlem6  22668  cnlnadjlem9  22671  cnlnadjeui  22673  cnlnadjeu  22674  nmopadji  22686  bdophsi  22692  bdopcoi  22694  nmopcoadji  22697  pjhmopi  22742  pjbdlni  22745  hmopidmchi  22747  mdslj1i  22915  xrge00  23326  xrge0pluscn  23337  xrge0tsmsd  23397  rnlogblem  23416  logb1  23420  esum0  23443  esumpcvgval  23461  esumcvg  23469  measdivcstOLD  23566  measdivcst  23567  indf1ofs  23624  coinfliprv  23698  indispcon  23780  cnllyscon  23791  rellyscon  23797  umgrabi  23922  konigsberg  23926  ghomsn  24010  soseq  24324  wfrlem11  24336  wfr1  24342  frrlem5c  24357  bdayfo  24399  bdayfn  24403  brbigcup  24508  fobigcup  24510  brsingle  24526  fnsingle  24528  brimage  24535  funimage  24537  fnimage  24538  imageval  24539  brcart  24541  brapply  24547  brcup  24548  brcap  24549  funpartfun  24552  axlowdimlem16  24656  axlowdimlem17  24657  onsucconi  24947  onsucsuccmpi  24953  itg2gt0cn  25005  ibladdnclem  25006  itgaddnclem1  25008  iblabsnclem  25013  iblabsnc  25014  iblmulc2nc  25015  itgmulc2nclem1  25016  bddiblnc  25020  itggt0cn  25022  areacirc  25033  vxveqv  25156  zintdom  25540  indcomp  25691  1alg  25824  1ded  25840  0alg  25858  0ded  25859  0catOLD  25860  1cat  25861  pgapspf  26154  comppfsc  26409  0totbnd  26599  heiborlem6  26642  mzpclall  26907  jm2.20nn  27192  dfacbasgrp  27375  dgraaf  27454  cnmsgngrp  27538  iso0  27638  dvsid  27650  injresinj  28214  usgraexvlem  28260  wlkntrllem4  28347  bnj906  29277  ax12olem4wAUX7  29434  ax12olem4OLD7  29661  isopiN  29993  isolatiN  30028  isomliN  30051  ishlatiN  30167
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