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 36283
Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 36282, 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 36282 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 36283 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 1881 . . 3 (∃𝑥(𝜓𝜒) → (∃𝑥𝜓 ∧ ∃𝑥𝜒))
2 bj-nnfand.1 . . . . 5 (𝜑 → Ⅎ'𝑥𝜓)
32bj-nnfed 36266 . . . 4 (𝜑 → (∃𝑥𝜓𝜓))
4 bj-nnfand.2 . . . . 5 (𝜑 → Ⅎ'𝑥𝜒)
54bj-nnfed 36266 . . . 4 (𝜑 → (∃𝑥𝜒𝜒))
63, 5anim12d 607 . . 3 (𝜑 → ((∃𝑥𝜓 ∧ ∃𝑥𝜒) → (𝜓𝜒)))
71, 6syl5 34 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → (𝜓𝜒)))
82bj-nnfad 36263 . . . 4 (𝜑 → (𝜓 → ∀𝑥𝜓))
94bj-nnfad 36263 . . . 4 (𝜑 → (𝜒 → ∀𝑥𝜒))
108, 9anim12d 607 . . 3 (𝜑 → ((𝜓𝜒) → (∀𝑥𝜓 ∧ ∀𝑥𝜒)))
11 19.26 1865 . . 3 (∀𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒))
1210, 11imbitrrdi 251 . 2 (𝜑 → ((𝜓𝜒) → ∀𝑥(𝜓𝜒)))
13 df-bj-nnf 36258 . 2 (Ⅎ'𝑥(𝜓𝜒) ↔ ((∃𝑥(𝜓𝜒) → (𝜓𝜒)) ∧ ((𝜓𝜒) → ∀𝑥(𝜓𝜒))))
147, 12, 13sylanbrc 581 1 (𝜑 → Ⅎ'𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wal 1531  wex 1773  Ⅎ'wnnf 36257
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-bj-nnf 36258
This theorem is referenced by:  bj-nnfbid  36287
  Copyright terms: Public domain W3C validator