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

Metamath Proof Explorer

Theorem spc3gv

Description: Specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008)

Ref Expression
Hypothesis spc3egv.1 ⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
Assertion spc3gv ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ∀ x ∀ y ∀ z φ → ψ

Proof

Step Hyp Ref Expression
1 spc3egv.1 ⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
2 1 notbid ⊢ x = A ∧ y = B ∧ z = C → ¬ φ ↔ ¬ ψ
3 2 spc3egv ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ¬ ψ → ∃ x ∃ y ∃ z ¬ φ
4 exnal ⊢ ∃ z ¬ φ ↔ ¬ ∀ z φ
5 4 exbii ⊢ ∃ y ∃ z ¬ φ ↔ ∃ y ¬ ∀ z φ
6 exnal ⊢ ∃ y ¬ ∀ z φ ↔ ¬ ∀ y ∀ z φ
7 5 6 bitri ⊢ ∃ y ∃ z ¬ φ ↔ ¬ ∀ y ∀ z φ
8 7 exbii ⊢ ∃ x ∃ y ∃ z ¬ φ ↔ ∃ x ¬ ∀ y ∀ z φ
9 exnal ⊢ ∃ x ¬ ∀ y ∀ z φ ↔ ¬ ∀ x ∀ y ∀ z φ
10 8 9 bitr2i ⊢ ¬ ∀ x ∀ y ∀ z φ ↔ ∃ x ∃ y ∃ z ¬ φ
11 3 10 imbitrrdi ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ¬ ψ → ¬ ∀ x ∀ y ∀ z φ
12 11 con4d ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ∀ x ∀ y ∀ z φ → ψ