Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-nnfand Structured version   Visualization version   GIF version

Theorem bj-nnfand 36732
Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 36731, 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 36731 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 36732 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
StepHypRef Expression
1 19.40 1884 . . 3 (∃𝑥(𝜓𝜒) → (∃𝑥𝜓 ∧ ∃𝑥𝜒))
2 bj-nnfand.1 . . . . 5 (𝜑 → Ⅎ'𝑥𝜓)
32bj-nnfed 36715 . . . 4 (𝜑 → (∃𝑥𝜓𝜓))
4 bj-nnfand.2 . . . . 5 (𝜑 → Ⅎ'𝑥𝜒)
54bj-nnfed 36715 . . . 4 (𝜑 → (∃𝑥𝜒𝜒))
63, 5anim12d 609 . . 3 (𝜑 → ((∃𝑥𝜓 ∧ ∃𝑥𝜒) → (𝜓𝜒)))
71, 6syl5 34 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → (𝜓𝜒)))
82bj-nnfad 36712 . . . 4 (𝜑 → (𝜓 → ∀𝑥𝜓))
94bj-nnfad 36712 . . . 4 (𝜑 → (𝜒 → ∀𝑥𝜒))
108, 9anim12d 609 . . 3 (𝜑 → ((𝜓𝜒) → (∀𝑥𝜓 ∧ ∀𝑥𝜒)))
11 19.26 1868 . . 3 (∀𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒))
1210, 11imbitrrdi 252 . 2 (𝜑 → ((𝜓𝜒) → ∀𝑥(𝜓𝜒)))
13 df-bj-nnf 36707 . 2 (Ⅎ'𝑥(𝜓𝜒) ↔ ((∃𝑥(𝜓𝜒) → (𝜓𝜒)) ∧ ((𝜓𝜒) → ∀𝑥(𝜓𝜒))))
147, 12, 13sylanbrc 583 1 (𝜑 → Ⅎ'𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1535  wex 1776  Ⅎ'wnnf 36706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-bj-nnf 36707
This theorem is referenced by:  bj-nnfbid  36736
  Copyright terms: Public domain W3C validator