This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \leftrightarrow (ψ \land χ \land θ)$
Assertion	mpbir3an	$⊢ φ$

Step	Hyp	Ref	Expression
1		mpbir3an.1	$⊢ ψ$
2		mpbir3an.2	$⊢ χ$
3		mpbir3an.3	$⊢ θ$
4		mpbir3an.4	$⊢ φ \leftrightarrow (ψ \land χ \land θ)$
5	1 2 3	3pm3.2i	$⊢ (ψ \land χ \land θ)$
6	5 4	mpbir	$⊢ φ$