Theorem mpbir2an 927

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3pm3.2i  1160  euequ1  2095  eqssi  3118  elini  3265  dtruarb  4123  opnzi  4165  so0  4256  we0  4291  ord0  4321  ordon  4410  onsucelsucexmidlem1  4451  regexmidlemm  4455  ordpwsucexmid  4493  reg3exmidlemwe  4501  ordom  4528  funi  5163  funcnvsn  5176  funinsn  5180  fnresi  5248  fn0  5250  f0  5321  fconst  5326  f10  5409  f1o0  5412  f1oi  5413  f1osn  5415  isoid  5719  iso0  5726  acexmidlem2  5779  fo1st  6063  fo2nd  6064  iordsmo  6202  tfrlem7  6222  tfrexlem  6239  mapsnf1o2  6598  1domsn  6721  inresflem  6953  0ct  7000  infnninf  7030  exmidonfinlem  7066  exmidaclem  7081  1pi  7147  prarloclemcalc  7334  ltsopr  7428  ltsosr  7596  cnm  7664  axicn  7695  axaddf  7700  axmulf  7701  nnindnn  7725  ltso  7866  negiso  8737  nnind  8760  0z  9089  dfuzi  9185  cnref1o  9469  elrpii  9473  xrltso  9612  0e0icopnf  9792  0e0iccpnf  9793  fldiv4p1lem1div2  10109  expcl2lemap  10336  expclzaplem  10348  expge0  10360  expge1  10361  xrnegiso  11063  fclim  11095  eff2  11423  reeff1  11443  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  sin01gt0  11504  egt2lt3  11522  halfleoddlt  11627  2prm  11844  3prm  11845  setsslnid  12049  fntopon  12230  istpsi  12245  ismeti  12554  tgqioo  12755  addcncntoplem  12759  divcnap  12763  abscncf  12780  recncf  12781  imcncf  12782  cjcncf  12783  dveflem  12895  reeff1o  12902  reefiso  12906  ioocosf1o  12983  ex-fl  13108  bj-indint  13300  bj-omord  13329  012of  13363  2o01f  13364  0nninf  13372  peano4nninf  13375  taupi  13430