This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1304

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1304.1 ⊢ φ → ∃ x ψ
bnj1304.2 ⊢ ψ → χ
bnj1304.3 ⊢ ψ → ¬ χ
Assertion bnj1304 ⊢ ¬ φ

Proof

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