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

Metamath Proof Explorer

Theorem r19.29ffa

Description: A commonly used pattern based on r19.29 , version with two restricted quantifiers. (Contributed by Thierry Arnoux, 26-Nov-2017)

Ref Expression
Hypothesis r19.29ffa.3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → 𝜒 )
Assertion r19.29ffa ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ) → 𝜒 )

Proof

Step Hyp Ref Expression
1 r19.29ffa.3 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜓 ) → 𝜒 )
2 1 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝜓 → 𝜒 ) )
3 2 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜒 ) )
4 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜒 ) )
5 4 adantr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝜒 ) )
6 simpr ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 )
7 5 6 r19.29d2r ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( ( 𝜓 → 𝜒 ) ∧ 𝜓 ) )
8 pm3.35 ⊢ ( ( 𝜓 ∧ ( 𝜓 → 𝜒 ) ) → 𝜒 )
9 8 ancoms ⊢ ( ( ( 𝜓 → 𝜒 ) ∧ 𝜓 ) → 𝜒 )
10 9 rexlimivw ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝜓 → 𝜒 ) ∧ 𝜓 ) → 𝜒 )
11 10 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( ( 𝜓 → 𝜒 ) ∧ 𝜓 ) → 𝜒 )
12 7 11 syl ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ) → 𝜒 )