Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-19.41t | Structured version Visualization version GIF version |
Description: Closed form of 19.41 2236 from the same axioms as 19.41v 1949. The same is doable with 19.27 2228, 19.28 2229, 19.31 2235, 19.32 2234, 19.44 2238, 19.45 2239. (Contributed by BJ, 2-Dec-2023.) |
Ref | Expression |
---|---|
bj-19.41t | ⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exancom 1860 | . . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) | |
2 | bj-19.42t 34121 | . . 3 ⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜓 ∧ 𝜑) ↔ (𝜓 ∧ ∃𝑥𝜑))) | |
3 | 1, 2 | syl5bb 285 | . 2 ⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜓 ∧ ∃𝑥𝜑))) |
4 | 3 | biancomd 466 | 1 ⊢ (Ⅎ'𝑥𝜓 → (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∃wex 1779 Ⅎ'wnnf 34074 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1780 df-bj-nnf 34075 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |