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