Metamath Proof Explorer

Theorem r19.29imd

Description: Theorem 19.29 of Margaris p. 90 with an implication in the hypothesis containing the generalization, deduction version. (Contributed by AV, 19-Jan-2019)

		Ref	Expression
	Hypotheses	r19.29imd.1	$⊢ φ \to \exists x \in A ψ$
		r19.29imd.2	$⊢ φ \to \forall x \in A (ψ \to χ)$
	Assertion	r19.29imd	$⊢ φ \to \exists x \in A (ψ \land χ)$

Proof

Step	Hyp	Ref	Expression
1		r19.29imd.1	$⊢ φ \to \exists x \in A ψ$
2		r19.29imd.2	$⊢ φ \to \forall x \in A (ψ \to χ)$
3		r19.29r	$⊢ (\exists x \in A ψ \land \forall x \in A (ψ \to χ)) \to \exists x \in A (ψ \land (ψ \to χ))$
4	1 2 3	syl2anc	$⊢ φ \to \exists x \in A (ψ \land (ψ \to χ))$
5		abai	$⊢ (ψ \land χ) \leftrightarrow (ψ \land (ψ \to χ))$
6	5	rexbii	$⊢ \exists x \in A (ψ \land χ) \leftrightarrow \exists x \in A (ψ \land (ψ \to χ))$
7	4 6	sylibr	$⊢ φ \to \exists x \in A (ψ \land χ)$