Theorem bj-nnfand 37230

Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 37229, 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 37229 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 37230 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 1906	. . 3 ⊢ (∃𝑥(𝜓 ∧ 𝜒) → (∃𝑥𝜓 ∧ ∃𝑥𝜒))
2		bj-nnfand.1	. . . . 5 ⊢ (𝜑 → Ⅎ'𝑥𝜓)
3	2	bj-nnfed 37207	. . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓))
4		bj-nnfand.2	. . . . 5 ⊢ (𝜑 → Ⅎ'𝑥𝜒)
5	4	bj-nnfed 37207	. . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → 𝜒))
6	3, 5	anim12d 618	. . 3 ⊢ (𝜑 → ((∃𝑥𝜓 ∧ ∃𝑥𝜒) → (𝜓 ∧ 𝜒)))
7	1, 6	syl5 34	. 2 ⊢ (𝜑 → (∃𝑥(𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)))
8	2	bj-nnfad 37204	. . . 4 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))
9	4	bj-nnfad 37204	. . . 4 ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))
10	8, 9	anim12d 618	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (∀𝑥𝜓 ∧ ∀𝑥𝜒)))
11		19.26 1890	. . 3 ⊢ (∀𝑥(𝜓 ∧ 𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒))
12	10, 11	imbitrrdi 254	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜒)))
13		df-bj-nnf 37202	. 2 ⊢ (Ⅎ'𝑥(𝜓 ∧ 𝜒) ↔ ((∃𝑥(𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) ∧ ((𝜓 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜒))))
14	7, 12, 13	sylanbrc 592	1 ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1558  ∃wex 1799  Ⅎ'wnnf 37201

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-bj-nnf 37202

This theorem is referenced by:  bj-nnfbid  37234