Description: Inference from Theorem 19.21 of Margaris p. 90. (Restricted quantifier version with triple quantification.) (Contributed by Mario Carneiro, 9-Jul-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ralrimivvva.1 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) → 𝜓 ) | |
| Assertion | ralrimivvva | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralrimivvva.1 | ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) → 𝜓 ) | |
| 2 | 1 | 3anassrs | ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐶 ) → 𝜓 ) |
| 3 | 2 | ralrimiva | ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑧 ∈ 𝐶 𝜓 ) |
| 4 | 3 | ralrimiva | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 ) |
| 5 | 4 | ralrimiva | ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜓 ) |