Theorem mpbir2an 950

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.)

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 948	. 2 |- ( ph <-> ch )
5	1, 4	mpbir 146	1 |- ph

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3pm3.2i  1201  euequ1  2175  eqssi  3243  elini  3391  dtruarb  4281  opnzi  4327  so0  4423  we0  4458  ord0  4488  ordon  4584  onsucelsucexmidlem1  4626  regexmidlemm  4630  ordpwsucexmid  4668  reg3exmidlemwe  4677  ordom  4705  funi  5358  funcnvsn  5375  funinsn  5379  fnresi  5450  fn0  5452  f0  5527  fconst  5532  f10  5618  f1o0  5622  f1oi  5623  f1osn  5625  funopsn  5829  isoid  5950  iso0  5957  acexmidlem2  6014  fo1st  6319  fo2nd  6320  iordsmo  6462  tfrlem7  6482  tfrexlem  6499  mapsnf1o2  6864  1domsn  7000  inresflem  7258  0ct  7305  infnninf  7322  infnninfOLD  7323  exmidonfinlem  7403  exmidaclem  7422  pw1on  7443  sucpw1nel3  7450  1pi  7534  prarloclemcalc  7721  ltsopr  7815  ltsosr  7983  cnm  8051  axicn  8082  axaddf  8087  axmulf  8088  nnindnn  8112  mpomulf  8168  ltso  8256  negiso  9134  nnind  9158  0z  9489  dfuzi  9589  cnref1o  9884  elrpii  9890  xrltso  10030  0e0icopnf  10213  0e0iccpnf  10214  fz0to4untppr  10358  fldiv4p1lem1div2  10564  expcl2lemap  10812  expclzaplem  10824  expge0  10836  expge1  10837  xrnegiso  11822  fclim  11854  eff2  12240  reeff1  12260  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  sin01gt0  12322  egt2lt3  12340  halfleoddlt  12454  2prm  12698  3prm  12699  1arith  12939  setsslnid  13133  xpsff1o  13431  isabli  13886  rngmgpf  13949  mgpf  14023  zringnzr  14615  fntopon  14747  istpsi  14762  ismeti  15069  cnfldms  15259  tgqioo  15278  addcncntoplem  15284  divcnap  15288  abscncf  15308  recncf  15309  imcncf  15310  cjcncf  15311  maxcncf  15338  mincncf  15339  dveflem  15449  reeff1o  15496  reefiso  15500  ioocosf1o  15577  lgslem2  15729  lgsfcl2  15734  lgsne0  15766  2lgslem1b  15817  umgrbien  15960  ex-fl  16321  bj-indint  16526  bj-omord  16555  012of  16592  2o01f  16593  0nninf  16606  peano4nninf  16608  taupi  16677