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

Metamath Proof Explorer

Theorem r19.29af

Description: A commonly used pattern based on r19.29 . See r19.29a , r19.29an for a variant when x is disjoint from ph . (Contributed by Thierry Arnoux, 29-Nov-2017)

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

Proof

Step	Hyp	Ref	Expression
1		r19.29af.0	$⊢ Ⅎ x φ$
2		r19.29af.1	$⊢ ((φ \land x \in A) \land ψ) \to χ$
3		r19.29af.2	$⊢ φ \to \exists x \in A ψ$
4		nfv	$⊢ Ⅎ x χ$
5	1 4 2 3	r19.29af2	$⊢ φ \to χ$