Description: The antecedent provides a condition implying the converse of 19.40 . This is to 19.40 what 19.33b is to 19.33 . (Contributed by BJ, 6-May-2019) (Proof shortened by Wolf Lammen, 13-Nov-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 19.40b | ⊢ ( ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) → ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) ↔ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm3.21 | ⊢ ( 𝜓 → ( 𝜑 → ( 𝜑 ∧ 𝜓 ) ) ) | |
| 2 | 1 | aleximi | ⊢ ( ∀ 𝑥 𝜓 → ( ∃ 𝑥 𝜑 → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) |
| 3 | pm3.2 | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) ) | |
| 4 | 3 | aleximi | ⊢ ( ∀ 𝑥 𝜑 → ( ∃ 𝑥 𝜓 → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) |
| 5 | 2 4 | jaoa | ⊢ ( ( ∀ 𝑥 𝜓 ∨ ∀ 𝑥 𝜑 ) → ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) |
| 6 | 5 | orcoms | ⊢ ( ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) → ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) |
| 7 | 19.40 | ⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) → ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) ) | |
| 8 | 6 7 | impbid1 | ⊢ ( ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 𝜓 ) → ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑥 𝜓 ) ↔ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) |