This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 φ ∧ ψ