Description: A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-nnfim1 | ⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → ( ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-nnfe | ⊢ ( Ⅎ' 𝑥 𝜑 → ( ∃ 𝑥 𝜑 → 𝜑 ) ) | |
2 | bj-nnfa | ⊢ ( Ⅎ' 𝑥 𝜓 → ( 𝜓 → ∀ 𝑥 𝜓 ) ) | |
3 | imim12 | ⊢ ( ( ∃ 𝑥 𝜑 → 𝜑 ) → ( ( 𝜓 → ∀ 𝑥 𝜓 ) → ( ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ) ) ) | |
4 | 3 | imp | ⊢ ( ( ( ∃ 𝑥 𝜑 → 𝜑 ) ∧ ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ( ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ) ) |
5 | 1 2 4 | syl2an | ⊢ ( ( Ⅎ' 𝑥 𝜑 ∧ Ⅎ' 𝑥 𝜓 ) → ( ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) ) ) |