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 36118
Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction, deduction form. Note: compared with the proof of bj-nnfan 36117, 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 36117 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 36118 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 36101 . . . 4 (𝜑 → (∃𝑥𝜓𝜓))
4 bj-nnfand.2 . . . . 5 (𝜑 → Ⅎ'𝑥𝜒)
54bj-nnfed 36101 . . . 4 (𝜑 → (∃𝑥𝜒𝜒))
63, 5anim12d 608 . . 3 (𝜑 → ((∃𝑥𝜓 ∧ ∃𝑥𝜒) → (𝜓𝜒)))
71, 6syl5 34 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → (𝜓𝜒)))
82bj-nnfad 36098 . . . 4 (𝜑 → (𝜓 → ∀𝑥𝜓))
94bj-nnfad 36098 . . . 4 (𝜑 → (𝜒 → ∀𝑥𝜒))
108, 9anim12d 608 . . 3 (𝜑 → ((𝜓𝜒) → (∀𝑥𝜓 ∧ ∀𝑥𝜒)))
11 19.26 1865 . . 3 (∀𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒))
1210, 11imbitrrdi 251 . 2 (𝜑 → ((𝜓𝜒) → ∀𝑥(𝜓𝜒)))
13 df-bj-nnf 36093 . 2 (Ⅎ'𝑥(𝜓𝜒) ↔ ((∃𝑥(𝜓𝜒) → (𝜓𝜒)) ∧ ((𝜓𝜒) → ∀𝑥(𝜓𝜒))))
147, 12, 13sylanbrc 582 1 (𝜑 → Ⅎ'𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1531  wex 1773  Ⅎ'wnnf 36092
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 396  df-ex 1774  df-bj-nnf 36093
This theorem is referenced by:  bj-nnfbid  36122
  Copyright terms: Public domain W3C validator