Description: Theorem *10.56 in WhiteheadRussell p. 156. (Contributed by Andrew Salmon, 24-May-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | pm10.56 | ⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ) → ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.45 | ⊢ ( ( 𝜑 → 𝜓 ) → ( ( 𝜑 ∧ 𝜒 ) → ( 𝜓 ∧ 𝜒 ) ) ) | |
2 | 1 | aleximi | ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) → ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) ) |
3 | 2 | imp | ⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜒 ) ) → ∃ 𝑥 ( 𝜓 ∧ 𝜒 ) ) |