Proof of Theorem r19.26
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝜑) |
2 | 1 | ralimi 2936 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜑) |
3 | | simpr 476 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝜓) |
4 | 3 | ralimi 2936 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜓) |
5 | 2, 4 | jca 553 |
. 2
⊢
(∀𝑥 ∈
𝐴 (𝜑 ∧ 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |
6 | | pm3.2 462 |
. . . 4
⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) |
7 | 6 | ral2imi 2931 |
. . 3
⊢
(∀𝑥 ∈
𝐴 𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))) |
8 | 7 | imp 444 |
. 2
⊢
((∀𝑥 ∈
𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)) |
9 | 5, 8 | impbii 198 |
1
⊢
(∀𝑥 ∈
𝐴 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |