Metamath Proof Explorer


Theorem bj-nnfan

Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction. (Contributed by BJ, 19-Nov-2023) In classical logic, there is a proof using the definition of conjunction in terms of implication and negation, so using bj-nnfim , bj-nnfnt and bj-nnfbi , but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 df-bj-nnf Ⅎ' x φ x φ φ φ x φ
2 df-bj-nnf Ⅎ' x ψ x ψ ψ ψ x ψ
3 19.40 x φ ψ x φ x ψ
4 anim12 x φ φ x ψ ψ x φ x ψ φ ψ
5 3 4 syl5 x φ φ x ψ ψ x φ ψ φ ψ
6 anim12 φ x φ ψ x ψ φ ψ x φ x ψ
7 id φ ψ φ ψ
8 7 alanimi x φ x ψ x φ ψ
9 6 8 syl6 φ x φ ψ x ψ φ ψ x φ ψ
10 5 9 anim12i x φ φ x ψ ψ φ x φ ψ x ψ x φ ψ φ ψ φ ψ x φ ψ
11 10 an4s x φ φ φ x φ x ψ ψ ψ x ψ x φ ψ φ ψ φ ψ x φ ψ
12 1 2 11 syl2anb Ⅎ' x φ Ⅎ' x ψ x φ ψ φ ψ φ ψ x φ ψ
13 df-bj-nnf Ⅎ' x φ ψ x φ ψ φ ψ φ ψ x φ ψ
14 12 13 sylibr Ⅎ' x φ Ⅎ' x ψ Ⅎ' x φ ψ