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)

Ref Expression
Hypotheses r19.29af2.p ⊢ Ⅎ 𝑥 𝜑
r19.29af2.c ⊢ Ⅎ 𝑥 𝜒
r19.29af2.1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
r19.29af2.2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )
Assertion r19.29af2 ( 𝜑 → 𝜒 )

Proof

Step Hyp Ref Expression
1 r19.29af2.p ⊢ Ⅎ 𝑥 𝜑
2 r19.29af2.c ⊢ Ⅎ 𝑥 𝜒
3 r19.29af2.1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝜓 ) → 𝜒 )
4 r19.29af2.2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )
5 3 exp31 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜒 ) ) )
6 1 2 5 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) )
7 4 6 mpd ⊢ ( 𝜑 → 𝜒 )