Description: Deduction quantifying both antecedent and consequent. (Contributed by Glauco Siliprandi, 23-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ralimda.1 | ⊢ Ⅎ 𝑥 𝜑 | |
ralimda.2 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 → 𝜒 ) ) | ||
Assertion | ralimda | ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 → ∀ 𝑥 ∈ 𝐴 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimda.1 | ⊢ Ⅎ 𝑥 𝜑 | |
2 | ralimda.2 | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 → 𝜒 ) ) | |
3 | nfra1 | ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝜓 | |
4 | 1 3 | nfan | ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) |
5 | id | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ) | |
6 | 5 | adantlr | ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ) |
7 | rspa | ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜓 ∧ 𝑥 ∈ 𝐴 ) → 𝜓 ) | |
8 | 7 | adantll | ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) → 𝜓 ) |
9 | 6 8 2 | sylc | ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) → 𝜒 ) |
10 | 4 9 | ralrimia | ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝜓 ) → ∀ 𝑥 ∈ 𝐴 𝜒 ) |
11 | 10 | ex | ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 → ∀ 𝑥 ∈ 𝐴 𝜒 ) ) |