Theorem mpbir3an

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

	Ref	Expression
Hypotheses	mpbir3an.1	⊢ 𝜓
	mpbir3an.2	⊢ 𝜒
	mpbir3an.3	⊢ 𝜃
	mpbir3an.4	⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) )
Assertion	mpbir3an	⊢ 𝜑

Proof

Step	Hyp	Ref	Expression
1		mpbir3an.1	⊢ 𝜓
2		mpbir3an.2	⊢ 𝜒
3		mpbir3an.3	⊢ 𝜃
4		mpbir3an.4	⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝜒 ∧ 𝜃 ) )
5	1 2 3	3pm3.2i	⊢ ( 𝜓 ∧ 𝜒 ∧ 𝜃 )
6	5 4	mpbir	⊢ 𝜑