Theorem mpbir2an

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

	Ref	Expression
Hypotheses	mpbir2an.1	|- ps
	mpbir2an.2	|- ch
	mpbir2an.maj	|- ( ph <-> ( ps /\ ch ) )
Assertion	mpbir2an	|- ph

Proof

Step	Hyp	Ref	Expression
1		mpbir2an.1	|- ps
2		mpbir2an.2	|- ch
3		mpbir2an.maj	|- ( ph <-> ( ps /\ ch ) )
4	1 3	mpbiran	|- ( ph <-> ch )
5	2 4	mpbir	|- ph