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  3288  sikss1c1c  4267  ins2kss  4279  ins3kss  4280  cokrelk  4284  cnvkexg  4286  ssetkex  4294  sikexg  4296  ins2kexg  4305  ins3kexg  4306  eqtfinrelk  4486  0ceven  4505  xpvv  4843  fnsn  5152  fnresi  5200  fn0  5202  f0  5248  fconst  5250  f10  5316  f1o0  5319  f1oi  5320  f1ovi  5321  f1osn  5322  fvi  5442  isoid  5490  1stfo  5505  2ndfo  5506  swapf1o  5511  xpassen  6057  2p1e3c  6156  fce  6188  0lt1c  6258  nnltp1c  6262  frecxp  6314  scancan  6331