Theorem mpbir2an 884

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 882	. 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  1117  euequ1  2037  eqssi  3016  elini  3157  dtruarb  3970  opnzi  3998  so0  4089  we0  4124  ord0  4154  ordon  4238  onsucelsucexmidlem1  4279  regexmidlemm  4283  ordpwsucexmid  4321  reg3exmidlemwe  4329  ordom  4355  funi  4962  funcnvsn  4975  funinsn  4979  fnresi  5047  fn0  5049  f0  5111  fconst  5113  f10  5191  f1o0  5194  f1oi  5195  f1osn  5197  isoid  5481  acexmidlem2  5540  fo1st  5815  fo2nd  5816  iordsmo  5946  tfrlem7  5966  tfrexlem  5983  1domsn  6363  1pi  6567  prarloclemcalc  6754  ltsopr  6848  ltsosr  7003  axicn  7093  nnindnn  7121  ltso  7256  negiso  8100  nnind  8122  0z  8443  dfuzi  8538  cnref1o  8814  elrpii  8818  xrltso  8947  0e0icopnf  9078  0e0iccpnf  9079  fldiv4p1lem1div2  9387  expcl2lemap  9585  expclzaplem  9597  expge0  9609  expge1  9610  fclim  10271  halfleoddlt  10438  2prm  10653  3prm  10654  ex-fl  10714  bj-indint  10884  bj-omord  10913