Metamath Proof Explorer

Theorem bj-nnfim2

Description: A consequence of nonfreeness in the antecedent and the consequent of an implication. (Contributed by BJ, 27-Aug-2023)

Ref Expression
Assertion bj-nnfim2 ⊢ Ⅎ' x φ ∧ Ⅎ' x ψ → ∀ x φ → ∃ x ψ → φ → ψ

Proof

Step Hyp Ref Expression
1 bj-nnfa ⊢ Ⅎ' x φ → φ → ∀ x φ
2 bj-nnfe ⊢ Ⅎ' x ψ → ∃ x ψ → ψ
3 imim12 ⊢ φ → ∀ x φ → ∃ x ψ → ψ → ∀ x φ → ∃ x ψ → φ → ψ
4 3 imp ⊢ φ → ∀ x φ ∧ ∃ x ψ → ψ → ∀ x φ → ∃ x ψ → φ → ψ
5 1 2 4 syl2an ⊢ Ⅎ' x φ ∧ Ⅎ' x ψ → ∀ x φ → ∃ x ψ → φ → ψ