Theorem mpbir2an 955

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

Step	Hyp	Ref	Expression
1		mpbir2an.2	. 2 |- ch
2		mpbir2an.1	. . 3 |- ps
3		mpbiran2an.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
4	2, 3	mpbiran 953	. 2 |- ( ph <-> ch )
5	1, 4	mpbir 221	1 |- ph

Syntax hints:   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  3pm3.2i  1239  eqssi  3619  elini  3797  dtru  4857  opnzi  4943  so0  5068  we0  5109  difxp  5558  ord0  5777  dfiota4  5879  funi  5920  funcnvsn  5936  fnresi  6008  fn0  6011  f0  6086  fconst  6091  f10  6169  f1o0  6173  f1oi  6174  f1osn  6176  isoid  6579  porpss  6941  ordon  6982  omssnlim  7079  fo1st  7188  fo2nd  7189  wfrfun  7425  wfr1  7433  iordsmo  7454  tfrlem7  7479  tfr1  7493  frfnom  7530  seqomlem2  7546  oawordeulem  7634  mapsnf1o2  7905  canth2  8113  unfilem2  8225  cantnfvalf  8562  cnfcom3clem  8602  tc2  8618  r111  8638  rankf  8657  cardf2  8769  harcard  8804  r0weon  8835  infxpenc  8841  infxpenc2lem1  8842  alephon  8892  alephf1  8908  alephiso  8921  alephsmo  8925  alephf1ALT  8926  alephfplem4  8930  ackbij1lem17  9058  ackbij1  9060  ackbij2  9065  isfin1-3  9208  fin1a2lem2  9223  fin1a2lem4  9225  axcc2lem  9258  iunfo  9361  smobeth  9408  0tsk  9577  1pi  9705  nqerf  9752  axaddf  9966  axmulf  9967  axicn  9971  mulnzcnopr  10673  negiso  11003  dfnn2  11033  nnind  11038  0z  11388  dfuzi  11468  cnref1o  11827  elrpii  11835  0e0icopnf  12282  0e0iccpnf  12283  fz0to4untppr  12442  fldiv4p1lem1div2  12636  om2uzf1oi  12752  om2uzisoi  12753  uzrdgfni  12757  expcl2lem  12872  expclzlem  12884  expge0  12896  expge1  12897  faclbnd4lem1  13080  hashkf  13119  wwlktovf1  13700  sqrtf  14103  fclim  14284  eff2  14829  reeff1  14850  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  sin01gt0  14920  egt2lt3  14934  qnnen  14942  ruc  14972  halfleoddlt  15086  divalglem2  15118  divalglem9  15124  bitsf1  15168  sadaddlem  15188  2prm  15405  3prm  15406  1arith  15631  prmlem1a  15813  setsnid  15915  xpsff1o  16228  dmaf  16699  cdaf  16700  coapm  16721  isdrs2  16939  0pos  16954  isposi  16956  fpwipodrs  17164  letsr  17227  sgrp0b  17292  frmdplusg  17391  symg2bas  17818  pmtrsn  17939  odf  17956  efgsfo  18152  efgrelexlemb  18163  isabli  18207  mgpf  18559  prdscrngd  18613  xrsmgmdifsgrp  19783  xrs1cmn  19786  cnmgpid  19808  zringnzr  19830  zringunit  19836  zringlpir  19837  zringndrg  19838  zzngim  19901  cnmsgngrp  19925  psgninv  19928  zrhpsgnmhm  19930  retos  19964  refld  19965  pjpm  20052  fntopon  20728  istpsi  20746  0cmp  21197  cmpfi  21211  indisconn  21221  comppfsc  21335  kqf  21550  ptcmpfi  21616  fbssfi  21641  zfbas  21700  alexsubALTlem2  21852  alexsubALTlem4  21854  ptcmplem2  21857  ptcmp  21862  prdstmdd  21927  tsmsfbas  21931  ismeti  22130  prdsxmslem2  22334  cnfldms  22579  cnnrg  22584  tgqioo  22603  xrtgioo  22609  recld2  22617  xrge0gsumle  22636  xrge0tsms  22637  addcnlem  22667  divcn  22671  abscncf  22704  recncf  22705  imcncf  22706  cjcncf  22707  icopnfhmeo  22742  xrhmeo  22745  cnllycmp  22755  isclmi0  22898  iscvsi  22929  cnstrcvs  22941  cncvs  22945  cncms  23151  ovolf  23250  ovolicc1  23284  ovolre  23293  ioorf  23341  opnmblALT  23371  dveflem  23742  mdegxrf  23828  iaa  24080  ulmdm  24147  dvradcnv  24175  reeff1o  24201  reefiso  24202  reefgim  24204  recosf1o  24281  efifo  24293  rzgrp  24300  logcn  24393  cxpcn3  24489  resqrtcn  24490  logb1  24507  logbmpt  24526  ressatans  24661  lgamcvg2  24781  lgam1  24790  gam1  24791  efnnfsumcl  24829  efchtdvds  24885  ppiub  24929  lgslem2  25023  lgsfcl2  25028  lgsne0  25060  2lgslem1b  25117  padicabvf  25320  istrkg3ld  25360  axlowdimlem16  25837  upgrbi  25988  umgrbi  25996  lfuhgr1v0e  26146  cusgr0  26322  wlk2v2elem2  27016  upgr4cycl4dv4e  27045  konigsberglem4  27117  frgr0  27128  ex-pss  27285  ex-fl  27304  isgrpoi  27352  grporn  27375  isabloi  27405  smcnlem  27552  lnocoi  27612  cncph  27674  cnbn  27725  cnchl  27772  norm3adifii  28005  hhph  28035  hhhl  28061  hlim0  28092  hlimf  28094  helch  28100  hsn0elch  28105  hhssabloilem  28118  hhssnv  28121  hhshsslem2  28125  hhssbn  28137  hhsshl  28138  shscli  28176  shintcli  28188  chintcli  28190  shsval2i  28246  pjhthlem2  28251  lejdii  28397  nonbooli  28510  pjrni  28561  pjfoi  28562  pjfi  28563  pjmf1  28575  df0op2  28611  idunop  28837  0cnop  28838  0cnfn  28839  idcnop  28840  idhmop  28841  0hmop  28842  0lnfn  28844  0bdop  28852  lnophsi  28860  lnopcoi  28862  lnopunii  28871  lnophmi  28877  nmcopex  28888  nmcoplb  28889  nmcfnex  28912  nmcfnlb  28913  imaelshi  28917  nlelshi  28919  nlelchi  28920  riesz4i  28922  riesz4  28923  riesz1  28924  cnlnadjlem6  28931  cnlnadjlem9  28934  cnlnadjeui  28936  cnlnadjeu  28937  nmopadji  28949  bdophsi  28955  bdopcoi  28957  nmopcoadji  28960  pjhmopi  29005  pjbdlni  29008  hmopidmchi  29010  mdslj1i  29178  rinvf1o  29432  nnindf  29565  rpdp2cl  29589  dp2ltc  29594  dpmul4  29622  xrstos  29679  xrsclat  29680  xrge0omnd  29711  xrge0tsmsd  29785  reofld  29840  nn0archi  29843  xrge0iifmhm  29985  xrge0pluscn  29986  cnzh  30014  rezh  30015  qqhval2lem  30025  esum0  30111  esumcst  30125  esumpcvgval  30140  esumcvg  30148  dmvlsiga  30192  measdivcstOLD  30287  eulerpartlemt  30433  coinfliprv  30544  ballotlem2  30550  signswmnd  30634  logdivsqrle  30728  hgt750lem  30729  bnj906  31000  indispconn  31216  cnllysconn  31227  rellysconn  31233  msrf  31439  soseq  31751  frrlem5c  31786  bdayfo  31828  scutf  31919  brbigcup  32005  fobigcup  32007  brsingle  32024  fnsingle  32026  brimage  32033  funimage  32035  fnimage  32036  imageval  32037  brcart  32039  brapply  32045  brcup  32046  brcap  32047  funpartfun  32050  brub  32061  onsucconni  32436  onsucsuccmpi  32442  dnicn  32482  bj-dtru  32797  bj-rabtr  32926  bj-rabtrALTALT  32928  taupilem2  33168  taupi  33169  f1omptsnlem  33183  icoreresf  33200  relowlpssretop  33212  finxpreclem3  33230  matunitlindf  33407  mblfinlem2  33447  areacirc  33505  0totbnd  33572  heiborlem6  33615  isolatiN  34503  isomliN  34526  ishlatiN  34642  mzpclall  37290  jm2.20nn  37564  dfacbasgrp  37678  dgraaf  37717  ifpim3  37841  ifpim4  37843  ifpbi1b  37848  iso0  38506  dvsid  38530  halffl  39510  resincncf  40088  0cnf  40090  iblempty  40181  dirkeritg  40319  fourierdlem62  40385  fourierdlem76  40399  fourierdlem103  40426  etransclem18  40469  etransclem46  40497  abnotbtaxb  41082  fmtnof1  41447  fmtno4prm  41487  prmdvdsfmtnof1  41499  31prm  41512  0evenALTV  41599  1oddALTV  41601  2evenALTV  41603  6even  41620  8even  41622  6gbe  41659  7gbow  41660  8gbe  41661  9gbo  41662  11gbo  41663  sprsymrelf1  41746  uspgrsprf1  41755  1odd  41811  nnsgrp  41817  0even  41931  2even  41933  2zrngamgm  41939  2zrngasgrp  41940  2zrngamnd  41941  2zrngagrp  41943  2zrngmsgrp  41947  zlmodzxzldeplem3  42291  lvecpsslmod  42296  ldepsnlinc  42297  blennngt2o2  42386  blennn0e2  42388  setrec2lem2  42441  aacllem  42547