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

Metamath Proof Explorer

Theorem r19.29af2

Description: A commonly used pattern based on r19.29 . (Contributed by Thierry Arnoux, 17-Dec-2017) (Proof shortened by OpenAI, 25-Mar-2020)

Step	Hyp	Ref	Expression
1		r19.29af2.p	$⊢ Ⅎ x φ$
2		r19.29af2.c	$⊢ Ⅎ x χ$
3		r19.29af2.1	$⊢ ((φ \land x \in A) \land ψ) \to χ$
4		r19.29af2.2	$⊢ φ \to \exists x \in A ψ$
5	3	exp31	$⊢ φ \to (x \in A \to (ψ \to χ))$
6	1 2 5	rexlimd	$⊢ φ \to (\exists x \in A ψ \to χ)$
7	4 6	mpd	$⊢ φ \to χ$