Metamath Proof Explorer


Theorem bj-nnfim1

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 Ⅎ' x φ Ⅎ' x ψ φ ψ x φ x ψ

Proof

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