Theorem bj-nnfand 36998

Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 36997, it has two more essential steps but fewer total steps (since there are fewer intermediate formulas to build) and is easier to follow and understand. This statement is of intermediate complexity: for simpler statements, closed-style proofs like that of bj-nnfan 36997 will generally be shorter than deduction-style proofs while still easy to follow, while for more complex statements, the opposite will be true (and deduction-style proofs like that of bj-nnfand 36998 will generally be easier to understand). (Contributed by BJ, 19-Nov-2023.) (Proof modification is discouraged.)

Hypotheses

Ref	Expression
bj-nnfand.1	⊢ (𝜑 → Ⅎ'𝑥𝜓)
bj-nnfand.2	⊢ (𝜑 → Ⅎ'𝑥𝜒)

Assertion

Ref	Expression
bj-nnfand	⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒))

Proof of Theorem bj-nnfand

Step	Hyp	Ref	Expression
1		19.40 1888	. . 3 ⊢ (∃𝑥(𝜓 ∧ 𝜒) → (∃𝑥𝜓 ∧ ∃𝑥𝜒))
2		bj-nnfand.1	. . . . 5 ⊢ (𝜑 → Ⅎ'𝑥𝜓)
3	2	bj-nnfed 36975	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓))
4		bj-nnfand.2	. . . . 5 ⊢ (𝜑 → Ⅎ'𝑥𝜒)
5	4	bj-nnfed 36975	. . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → 𝜒))
6	3, 5	anim12d 610	. . 3 ⊢ (𝜑 → ((∃𝑥𝜓 ∧ ∃𝑥𝜒) → (𝜓 ∧ 𝜒)))
7	1, 6	syl5 34	. 2 ⊢ (𝜑 → (∃𝑥(𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)))
8	2	bj-nnfad 36972	. . . 4 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
9	4	bj-nnfad 36972	. . . 4 ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))
10	8, 9	anim12d 610	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (∀𝑥𝜓 ∧ ∀𝑥𝜒)))
11		19.26 1872	. . 3 ⊢ (∀𝑥(𝜓 ∧ 𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒))
12	10, 11	imbitrrdi 252	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜒)))
13		df-bj-nnf 36970	. 2 ⊢ (Ⅎ'𝑥(𝜓 ∧ 𝜒) ↔ ((∃𝑥(𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) ∧ ((𝜓 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜒))))
14	7, 12, 13	sylanbrc 584	1 ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540  ∃wex 1781  Ⅎ'wnnf 36969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-bj-nnf 36970

This theorem is referenced by:  bj-nnfbid  37002