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	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 ) → 𝜒 )