|   | Mathbox for BJ | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-nnfand | Structured version Visualization version GIF version | ||
| Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 36750, 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 36750 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 36751 will generally be easier to understand). (Contributed by BJ, 19-Nov-2023.) (Proof modification is discouraged.) | 
| Ref | Expression | 
|---|---|
| bj-nnfand.1 | ⊢ (𝜑 → Ⅎ'𝑥𝜓) | 
| bj-nnfand.2 | ⊢ (𝜑 → Ⅎ'𝑥𝜒) | 
| Ref | Expression | 
|---|---|
| bj-nnfand | ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 19.40 1885 | . . 3 ⊢ (∃𝑥(𝜓 ∧ 𝜒) → (∃𝑥𝜓 ∧ ∃𝑥𝜒)) | |
| 2 | bj-nnfand.1 | . . . . 5 ⊢ (𝜑 → Ⅎ'𝑥𝜓) | |
| 3 | 2 | bj-nnfed 36734 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜓)) | 
| 4 | bj-nnfand.2 | . . . . 5 ⊢ (𝜑 → Ⅎ'𝑥𝜒) | |
| 5 | 4 | bj-nnfed 36734 | . . . 4 ⊢ (𝜑 → (∃𝑥𝜒 → 𝜒)) | 
| 6 | 3, 5 | anim12d 609 | . . 3 ⊢ (𝜑 → ((∃𝑥𝜓 ∧ ∃𝑥𝜒) → (𝜓 ∧ 𝜒))) | 
| 7 | 1, 6 | syl5 34 | . 2 ⊢ (𝜑 → (∃𝑥(𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))) | 
| 8 | 2 | bj-nnfad 36731 | . . . 4 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) | 
| 9 | 4 | bj-nnfad 36731 | . . . 4 ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) | 
| 10 | 8, 9 | anim12d 609 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (∀𝑥𝜓 ∧ ∀𝑥𝜒))) | 
| 11 | 19.26 1869 | . . 3 ⊢ (∀𝑥(𝜓 ∧ 𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒)) | |
| 12 | 10, 11 | imbitrrdi 252 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜒))) | 
| 13 | df-bj-nnf 36726 | . 2 ⊢ (Ⅎ'𝑥(𝜓 ∧ 𝜒) ↔ ((∃𝑥(𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) ∧ ((𝜓 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜒)))) | |
| 14 | 7, 12, 13 | sylanbrc 583 | 1 ⊢ (𝜑 → Ⅎ'𝑥(𝜓 ∧ 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∀wal 1537 ∃wex 1778 Ⅎ'wnnf 36725 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-bj-nnf 36726 | 
| This theorem is referenced by: bj-nnfbid 36755 | 
| Copyright terms: Public domain | W3C validator |