Theorem mpbir3an

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011)

	Ref	Expression
Hypotheses	mpbir3an.1	|- ps
	mpbir3an.2	|- ch
	mpbir3an.3	|- th
	mpbir3an.4	|- ( ph <-> ( ps /\ ch /\ th ) )
Assertion	mpbir3an	|- ph

Proof

Step	Hyp	Ref	Expression
1		mpbir3an.1	|- ps
2		mpbir3an.2	|- ch
3		mpbir3an.3	|- th
4		mpbir3an.4	|- ( ph <-> ( ps /\ ch /\ th ) )
5	1 2 3	3pm3.2i	|- ( ps /\ ch /\ th )
6	5 4	mpbir	|- ph