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 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion spc3gv ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 𝜑 → 𝜓 ) )

Proof

Step Hyp Ref Expression
1 spc3egv.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( 𝜑 ↔ 𝜓 ) )
2 1 notbid ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3 2 spc3egv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ¬ 𝜓 → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ¬ 𝜑 ) )
4 exnal ⊢ ( ∃ 𝑧 ¬ 𝜑 ↔ ¬ ∀ 𝑧 𝜑 )
5 4 exbii ⊢ ( ∃ 𝑦 ∃ 𝑧 ¬ 𝜑 ↔ ∃ 𝑦 ¬ ∀ 𝑧 𝜑 )
6 exnal ⊢ ( ∃ 𝑦 ¬ ∀ 𝑧 𝜑 ↔ ¬ ∀ 𝑦 ∀ 𝑧 𝜑 )
7 5 6 bitri ⊢ ( ∃ 𝑦 ∃ 𝑧 ¬ 𝜑 ↔ ¬ ∀ 𝑦 ∀ 𝑧 𝜑 )
8 7 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ¬ 𝜑 ↔ ∃ 𝑥 ¬ ∀ 𝑦 ∀ 𝑧 𝜑 )
9 exnal ⊢ ( ∃ 𝑥 ¬ ∀ 𝑦 ∀ 𝑧 𝜑 ↔ ¬ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 𝜑 )
10 8 9 bitr2i ⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ¬ 𝜑 )
11 3 10 imbitrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ¬ 𝜓 → ¬ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 𝜑 ) )
12 11 con4d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 𝜑 → 𝜓 ) )