Metamath Proof Explorer


Theorem bj-nnfim

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

Ref Expression
Assertion bj-nnfim Ⅎ' x φ Ⅎ' x ψ Ⅎ' x φ ψ

Proof

Step Hyp Ref Expression
1 19.35 x φ ψ x φ x ψ
2 bj-nnfim2 Ⅎ' x φ Ⅎ' x ψ x φ x ψ φ ψ
3 1 2 syl5bi Ⅎ' x φ Ⅎ' x ψ x φ ψ φ ψ
4 bj-nnfim1 Ⅎ' x φ Ⅎ' x ψ φ ψ x φ x ψ
5 19.38 x φ x ψ x φ ψ
6 4 5 syl6 Ⅎ' x φ Ⅎ' x ψ φ ψ x φ ψ
7 df-bj-nnf Ⅎ' x φ ψ x φ ψ φ ψ φ ψ x φ ψ
8 3 6 7 sylanbrc Ⅎ' x φ Ⅎ' x ψ Ⅎ' x φ ψ