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

Theorem bj-nnfan 36133
Description: Nonfreeness in both conjuncts implies nonfreeness in the conjunction. (Contributed by BJ, 19-Nov-2023.) In classical logic, there is a proof using the definition of conjunction in terms of implication and negation, so using bj-nnfim 36131, bj-nnfnt 36125 and bj-nnfbi 36110, but we want a proof valid in intuitionistic logic. (Proof modification is discouraged.)
Assertion
Ref Expression
bj-nnfan ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑𝜓))

Proof of Theorem bj-nnfan
StepHypRef Expression
1 df-bj-nnf 36109 . . 3 (Ⅎ'𝑥𝜑 ↔ ((∃𝑥𝜑𝜑) ∧ (𝜑 → ∀𝑥𝜑)))
2 df-bj-nnf 36109 . . 3 (Ⅎ'𝑥𝜓 ↔ ((∃𝑥𝜓𝜓) ∧ (𝜓 → ∀𝑥𝜓)))
3 19.40 1881 . . . . . 6 (∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
4 anim12 806 . . . . . 6 (((∃𝑥𝜑𝜑) ∧ (∃𝑥𝜓𝜓)) → ((∃𝑥𝜑 ∧ ∃𝑥𝜓) → (𝜑𝜓)))
53, 4syl5 34 . . . . 5 (((∃𝑥𝜑𝜑) ∧ (∃𝑥𝜓𝜓)) → (∃𝑥(𝜑𝜓) → (𝜑𝜓)))
6 anim12 806 . . . . . 6 (((𝜑 → ∀𝑥𝜑) ∧ (𝜓 → ∀𝑥𝜓)) → ((𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓)))
7 id 22 . . . . . . 7 ((𝜑𝜓) → (𝜑𝜓))
87alanimi 1810 . . . . . 6 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
96, 8syl6 35 . . . . 5 (((𝜑 → ∀𝑥𝜑) ∧ (𝜓 → ∀𝑥𝜓)) → ((𝜑𝜓) → ∀𝑥(𝜑𝜓)))
105, 9anim12i 612 . . . 4 ((((∃𝑥𝜑𝜑) ∧ (∃𝑥𝜓𝜓)) ∧ ((𝜑 → ∀𝑥𝜑) ∧ (𝜓 → ∀𝑥𝜓))) → ((∃𝑥(𝜑𝜓) → (𝜑𝜓)) ∧ ((𝜑𝜓) → ∀𝑥(𝜑𝜓))))
1110an4s 657 . . 3 ((((∃𝑥𝜑𝜑) ∧ (𝜑 → ∀𝑥𝜑)) ∧ ((∃𝑥𝜓𝜓) ∧ (𝜓 → ∀𝑥𝜓))) → ((∃𝑥(𝜑𝜓) → (𝜑𝜓)) ∧ ((𝜑𝜓) → ∀𝑥(𝜑𝜓))))
121, 2, 11syl2anb 597 . 2 ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → ((∃𝑥(𝜑𝜓) → (𝜑𝜓)) ∧ ((𝜑𝜓) → ∀𝑥(𝜑𝜓))))
13 df-bj-nnf 36109 . 2 (Ⅎ'𝑥(𝜑𝜓) ↔ ((∃𝑥(𝜑𝜓) → (𝜑𝜓)) ∧ ((𝜑𝜓) → ∀𝑥(𝜑𝜓))))
1412, 13sylibr 233 1 ((Ⅎ'𝑥𝜑 ∧ Ⅎ'𝑥𝜓) → Ⅎ'𝑥(𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1531  wex 1773  Ⅎ'wnnf 36108
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 36109
This theorem is referenced by:  bj-nnfbit  36137
  Copyright terms: Public domain W3C validator