Theorem mpbir2an 888

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3pm3.2i  1121  euequ1  2043  eqssi  3041  elini  3184  dtruarb  4026  opnzi  4062  so0  4153  we0  4188  ord0  4218  ordon  4303  onsucelsucexmidlem1  4344  regexmidlemm  4348  ordpwsucexmid  4386  reg3exmidlemwe  4394  ordom  4421  funi  5046  funcnvsn  5059  funinsn  5063  fnresi  5131  fn0  5133  f0  5201  fconst  5206  f10  5287  f1o0  5290  f1oi  5291  f1osn  5293  isoid  5589  iso0  5596  acexmidlem2  5649  fo1st  5928  fo2nd  5929  iordsmo  6062  tfrlem7  6082  tfrexlem  6099  mapsnf1o2  6451  1domsn  6533  inresflem  6750  infnninf  6803  1pi  6872  prarloclemcalc  7059  ltsopr  7153  ltsosr  7308  axicn  7398  nnindnn  7426  ltso  7561  negiso  8414  nnind  8436  0z  8759  dfuzi  8854  cnref1o  9131  elrpii  9135  xrltso  9264  0e0icopnf  9395  0e0iccpnf  9396  fldiv4p1lem1div2  9708  expcl2lemap  9963  expclzaplem  9975  expge0  9987  expge1  9988  fclim  10678  eff2  10966  reeff1  10987  ef01bndlem  11043  sin01bnd  11044  cos01bnd  11045  sin01gt0  11048  egt2lt3  11063  halfleoddlt  11168  2prm  11383  3prm  11384  setsnidn  11540  fntopon  11575  abscncf  11596  recncf  11597  imcncf  11598  cjcncf  11599  ex-fl  11607  bj-indint  11781  bj-omord  11810  0nninf  11848  peano4nninf  11851