bnj1019

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

		Ref	Expression
	Assertion	bnj1019	$⊢ \exists p (θ \land χ \land τ \land η) \leftrightarrow (θ \land χ \land η \land \exists p τ)$

Step	Hyp	Ref	Expression
1		19.42v	$⊢ \exists p ((θ \land χ \land η) \land τ) \leftrightarrow ((θ \land χ \land η) \land \exists p τ)$
2		bnj258	$⊢ (θ \land χ \land τ \land η) \leftrightarrow ((θ \land χ \land η) \land τ)$
3	2	exbii	$⊢ \exists p (θ \land χ \land τ \land η) \leftrightarrow \exists p ((θ \land χ \land η) \land τ)$
4		df-bnj17	$⊢ (θ \land χ \land η \land \exists p τ) \leftrightarrow ((θ \land χ \land η) \land \exists p τ)$
5	1 3 4	3bitr4i	$⊢ \exists p (θ \land χ \land τ \land η) \leftrightarrow (θ \land χ \land η \land \exists p τ)$

Metamath Proof Explorer