Theorem mpbir2an 848

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 846	. 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  1081  euequ1  1992  eqssi  2955  dtruarb  3933  opnzi  3963  so0  4054  ord0  4094  ordon  4178  onsucelsucexmidlem1  4213  regexmidlemm  4217  ordpwsucexmid  4246  ordom  4272  funi  4875  funcnvsn  4888  fnresi  4959  fn0  4961  f0  5023  fconst  5025  f10  5103  f1o0  5106  f1oi  5107  f1osn  5109  isoid  5393  acexmidlem2  5452  fo1st  5726  fo2nd  5727  iordsmo  5853  tfrlem7  5874  tfrexlem  5889  1pi  6299  prarloclemcalc  6485  ltsopr  6570  ltsosr  6692  axicn  6749  ltso  6893  nnind  7711  0z  8032  dfuzi  8124  cnref1o  8357  elrpii  8361  xrltso  8487  0e0icopnf  8618  0e0iccpnf  8619  expcl2lemap  8921  expclzaplem  8933  expge0  8945  expge1  8946  bj-indint  9390  bj-omord  9420