Theorem mpbir2an

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

	Ref	Expression
Hypotheses	mpbir2an.1	⊢ 𝜓
	mpbir2an.2	⊢ 𝜒
	mpbir2an.maj	⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝜒 ) )
Assertion	mpbir2an	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		mpbir2an.1	⊢ 𝜓
2		mpbir2an.2	⊢ 𝜒
3		mpbir2an.maj	⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝜒 ) )
4	1 3	mpbiran	⊢ ( 𝜑 ↔ 𝜒 )
5	2 4	mpbir	⊢ 𝜑