Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1304.1 |
⊢ ( 𝜑 → ∃ 𝑥 𝜓 ) |
2 |
|
bnj1304.2 |
⊢ ( 𝜓 → 𝜒 ) |
3 |
|
bnj1304.3 |
⊢ ( 𝜓 → ¬ 𝜒 ) |
4 |
|
notnotb |
⊢ ( ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) ↔ ¬ ¬ ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) ) |
5 |
|
notnotb |
⊢ ( 𝜒 ↔ ¬ ¬ 𝜒 ) |
6 |
5
|
anbi2i |
⊢ ( ( ¬ 𝜒 ∧ 𝜒 ) ↔ ( ¬ 𝜒 ∧ ¬ ¬ 𝜒 ) ) |
7 |
6
|
exbii |
⊢ ( ∃ 𝑥 ( ¬ 𝜒 ∧ 𝜒 ) ↔ ∃ 𝑥 ( ¬ 𝜒 ∧ ¬ ¬ 𝜒 ) ) |
8 |
|
ioran |
⊢ ( ¬ ( 𝜒 ∨ ¬ 𝜒 ) ↔ ( ¬ 𝜒 ∧ ¬ ¬ 𝜒 ) ) |
9 |
8
|
exbii |
⊢ ( ∃ 𝑥 ¬ ( 𝜒 ∨ ¬ 𝜒 ) ↔ ∃ 𝑥 ( ¬ 𝜒 ∧ ¬ ¬ 𝜒 ) ) |
10 |
|
exnal |
⊢ ( ∃ 𝑥 ¬ ( 𝜒 ∨ ¬ 𝜒 ) ↔ ¬ ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) ) |
11 |
7 9 10
|
3bitr2ri |
⊢ ( ¬ ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) ↔ ∃ 𝑥 ( ¬ 𝜒 ∧ 𝜒 ) ) |
12 |
11
|
notbii |
⊢ ( ¬ ¬ ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) ↔ ¬ ∃ 𝑥 ( ¬ 𝜒 ∧ 𝜒 ) ) |
13 |
|
exancom |
⊢ ( ∃ 𝑥 ( ¬ 𝜒 ∧ 𝜒 ) ↔ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜒 ) ) |
14 |
13
|
notbii |
⊢ ( ¬ ∃ 𝑥 ( ¬ 𝜒 ∧ 𝜒 ) ↔ ¬ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜒 ) ) |
15 |
4 12 14
|
3bitri |
⊢ ( ∀ 𝑥 ( 𝜒 ∨ ¬ 𝜒 ) ↔ ¬ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜒 ) ) |
16 |
|
exmid |
⊢ ( 𝜒 ∨ ¬ 𝜒 ) |
17 |
15 16
|
mpgbi |
⊢ ¬ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜒 ) |
18 |
2 3
|
jca |
⊢ ( 𝜓 → ( 𝜒 ∧ ¬ 𝜒 ) ) |
19 |
1 18
|
bnj593 |
⊢ ( 𝜑 → ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜒 ) ) |
20 |
17 19
|
mto |
⊢ ¬ 𝜑 |