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 36751
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.)
Hypotheses
Ref Expression
bj-nnfand.1 (𝜑 → Ⅎ'𝑥𝜓)
bj-nnfand.2 (𝜑 → Ⅎ'𝑥𝜒)
Assertion
Ref Expression
bj-nnfand (𝜑 → Ⅎ'𝑥(𝜓𝜒))

Proof of Theorem bj-nnfand
StepHypRef Expression
1 19.40 1885 . . 3 (∃𝑥(𝜓𝜒) → (∃𝑥𝜓 ∧ ∃𝑥𝜒))
2 bj-nnfand.1 . . . . 5 (𝜑 → Ⅎ'𝑥𝜓)
32bj-nnfed 36734 . . . 4 (𝜑 → (∃𝑥𝜓𝜓))
4 bj-nnfand.2 . . . . 5 (𝜑 → Ⅎ'𝑥𝜒)
54bj-nnfed 36734 . . . 4 (𝜑 → (∃𝑥𝜒𝜒))
63, 5anim12d 609 . . 3 (𝜑 → ((∃𝑥𝜓 ∧ ∃𝑥𝜒) → (𝜓𝜒)))
71, 6syl5 34 . 2 (𝜑 → (∃𝑥(𝜓𝜒) → (𝜓𝜒)))
82bj-nnfad 36731 . . . 4 (𝜑 → (𝜓 → ∀𝑥𝜓))
94bj-nnfad 36731 . . . 4 (𝜑 → (𝜒 → ∀𝑥𝜒))
108, 9anim12d 609 . . 3 (𝜑 → ((𝜓𝜒) → (∀𝑥𝜓 ∧ ∀𝑥𝜒)))
11 19.26 1869 . . 3 (∀𝑥(𝜓𝜒) ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒))
1210, 11imbitrrdi 252 . 2 (𝜑 → ((𝜓𝜒) → ∀𝑥(𝜓𝜒)))
13 df-bj-nnf 36726 . 2 (Ⅎ'𝑥(𝜓𝜒) ↔ ((∃𝑥(𝜓𝜒) → (𝜓𝜒)) ∧ ((𝜓𝜒) → ∀𝑥(𝜓𝜒))))
147, 12, 13sylanbrc 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