Theorem mpbiran

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996)

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

Proof

Step	Hyp	Ref	Expression
1		mpbiran.1	|- ps
2		mpbiran.2	|- ( ph <-> ( ps /\ ch ) )
3	1	biantrur	|- ( ch <-> ( ps /\ ch ) )
4	2 3	bitr4i	|- ( ph <-> ch )