Theorem mpbir2an 886

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)

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

Syntax hints:   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  3pm3.2i  1130  ax12olem4  1930  euequ1  2292  eqssi  3289  sikss1c1c  4268  ins2kss  4280  ins3kss  4281  cokrelk  4285  cnvkexg  4287  ssetkex  4295  sikexg  4297  ins2kexg  4306  ins3kexg  4307  eqtfinrelk  4487  0ceven  4506  xpvv  4844  fnsn  5153  fnresi  5201  fn0  5203  f0  5249  fconst  5251  f10  5317  f1o0  5320  f1oi  5321  f1ovi  5322  f1osn  5323  fvi  5443  isoid  5491  1stfo  5506  2ndfo  5507  swapf1o  5512  xpassen  6058  2p1e3c  6157  fce  6189  0lt1c  6259  nnltp1c  6263  frecxp  6315  scancan  6332