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 34508
 Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 34507, 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 34507 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 34508 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 1887 . . 3 (∃𝑥(𝜓𝜒) → (∃𝑥𝜓 ∧ ∃𝑥𝜒))
2 bj-nnfand.1 . . . . 5 (𝜑 → Ⅎ'𝑥𝜓)
32bj-nnfed 34493 . . . 4 (𝜑 → (∃𝑥𝜓𝜓))
4 bj-nnfand.2 . . . . 5 (𝜑 → Ⅎ'𝑥𝜒)
54bj-nnfed 34493 . . . 4 (𝜑 → (∃𝑥𝜒𝜒))
63, 5anim12d 611 . . 3 (𝜑 → ((∃𝑥𝜓 ∧ ∃𝑥𝜒) → (𝜓𝜒)))
71, 6syl5 34 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → (𝜓𝜒)))
82bj-nnfad 34491 . . . 4 (𝜑 → (𝜓 → ∀𝑥𝜓))
94bj-nnfad 34491 . . . 4 (𝜑 → (𝜒 → ∀𝑥𝜒))
108, 9anim12d 611 . . 3 (𝜑 → ((𝜓𝜒) → (∀𝑥𝜓 ∧ ∀𝑥𝜒)))
11 19.26 1871 . . 3 (∀𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒))
1210, 11syl6ibr 255 . 2 (𝜑 → ((𝜓𝜒) → ∀𝑥(𝜓𝜒)))
13 df-bj-nnf 34486 . 2 (Ⅎ'𝑥(𝜓𝜒) ↔ ((∃𝑥(𝜓𝜒) → (𝜓𝜒)) ∧ ((𝜓𝜒) → ∀𝑥(𝜓𝜒))))
147, 12, 13sylanbrc 586 1 (𝜑 → Ⅎ'𝑥(𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536  ∃wex 1781  Ⅎ'wnnf 34485 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 210  df-an 400  df-ex 1782  df-bj-nnf 34486 This theorem is referenced by:  bj-nnfbid  34512
 Copyright terms: Public domain W3C validator