Theorem mpbir2an 849

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

Syntax hints:   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3pm3.2i  1082  euequ1  1995  eqssi  2961  dtruarb  3942  opnzi  3972  so0  4063  we0  4098  ord0  4128  ordon  4212  onsucelsucexmidlem1  4253  regexmidlemm  4257  ordpwsucexmid  4294  reg3exmidlemwe  4303  ordom  4329  funi  4932  funcnvsn  4945  fnresi  5016  fn0  5018  f0  5080  fconst  5082  f10  5160  f1o0  5163  f1oi  5164  f1osn  5166  isoid  5450  acexmidlem2  5509  fo1st  5784  fo2nd  5785  iordsmo  5912  tfrlem7  5933  tfrexlem  5948  1pi  6413  prarloclemcalc  6600  ltsopr  6694  ltsosr  6849  axicn  6939  nnindnn  6967  ltso  7096  nnind  7930  0z  8256  dfuzi  8348  cnref1o  8582  elrpii  8586  xrltso  8717  0e0icopnf  8848  0e0iccpnf  8849  fldiv4p1lem1div2  9147  expcl2lemap  9267  expclzaplem  9279  expge0  9291  expge1  9292  fclim  9815  ex-fl  9895  bj-indint  10055  bj-omord  10085