Metamath Proof Explorer

Theorem moantr

Description: Sufficient condition for transitivity of conjunctions inside existential quantifiers. (Contributed by Peter Mazsa, 2-Oct-2018)

		Ref	Expression
	Assertion	moantr	$⊢ \exists^{*} x ψ \to ((\exists x (φ \land ψ) \land \exists x (ψ \land χ)) \to \exists x (φ \land χ))$

Proof

Step	Hyp	Ref	Expression
1		exancom	$⊢ \exists x (φ \land ψ) \leftrightarrow \exists x (ψ \land φ)$
2	1	anbi1i	$⊢ (\exists x (φ \land ψ) \land \exists x (ψ \land χ)) \leftrightarrow (\exists x (ψ \land φ) \land \exists x (ψ \land χ))$
3	2	anbi2i	$⊢ (\exists^{} x ψ \land (\exists x (φ \land ψ) \land \exists x (ψ \land χ))) \leftrightarrow (\exists^{} x ψ \land (\exists x (ψ \land φ) \land \exists x (ψ \land χ)))$
4		3anass	$⊢ (\exists^{} x ψ \land \exists x (ψ \land φ) \land \exists x (ψ \land χ)) \leftrightarrow (\exists^{} x ψ \land (\exists x (ψ \land φ) \land \exists x (ψ \land χ)))$
5	3 4	bitr4i	$⊢ (\exists^{} x ψ \land (\exists x (φ \land ψ) \land \exists x (ψ \land χ))) \leftrightarrow (\exists^{} x ψ \land \exists x (ψ \land φ) \land \exists x (ψ \land χ))$
6		mopick2	$⊢ (\exists^{*} x ψ \land \exists x (ψ \land φ) \land \exists x (ψ \land χ)) \to \exists x (ψ \land φ \land χ)$
7	5 6	sylbi	$⊢ (\exists^{*} x ψ \land (\exists x (φ \land ψ) \land \exists x (ψ \land χ))) \to \exists x (ψ \land φ \land χ)$
8		3anass	$⊢ (ψ \land φ \land χ) \leftrightarrow (ψ \land (φ \land χ))$
9	8	exbii	$⊢ \exists x (ψ \land φ \land χ) \leftrightarrow \exists x (ψ \land (φ \land χ))$
10		exsimpr	$⊢ \exists x (ψ \land (φ \land χ)) \to \exists x (φ \land χ)$
11	9 10	sylbi	$⊢ \exists x (ψ \land φ \land χ) \to \exists x (φ \land χ)$
12	7 11	syl	$⊢ (\exists^{*} x ψ \land (\exists x (φ \land ψ) \land \exists x (ψ \land χ))) \to \exists x (φ \land χ)$
13		impexp	$⊢ ((\exists^{} x ψ \land (\exists x (φ \land ψ) \land \exists x (ψ \land χ))) \to \exists x (φ \land χ)) \leftrightarrow (\exists^{} x ψ \to ((\exists x (φ \land ψ) \land \exists x (ψ \land χ)) \to \exists x (φ \land χ)))$
14	12 13	mpbi	$⊢ \exists^{*} x ψ \to ((\exists x (φ \land ψ) \land \exists x (ψ \land χ)) \to \exists x (φ \land χ))$