Theorem cbval2OLD

Description: Obsolete version of cbval2 as of 11-Sep-2023. (Contributed by NM, 22-Dec-2003) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 22-Apr-2018) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	cbval2.1	⊢ Ⅎ 𝑧 𝜑
	cbval2.2	⊢ Ⅎ 𝑤 𝜑
	cbval2.3	⊢ Ⅎ 𝑥 𝜓
	cbval2.4	⊢ Ⅎ 𝑦 𝜓
	cbval2.5	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbval2OLD	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑧 ∀ 𝑤 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbval2.1	⊢ Ⅎ 𝑧 𝜑
2		cbval2.2	⊢ Ⅎ 𝑤 𝜑
3		cbval2.3	⊢ Ⅎ 𝑥 𝜓
4		cbval2.4	⊢ Ⅎ 𝑦 𝜓
5		cbval2.5	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝜑 ↔ 𝜓 ) )
6	1	nfal	⊢ Ⅎ 𝑧 ∀ 𝑦 𝜑
7	3	nfal	⊢ Ⅎ 𝑥 ∀ 𝑤 𝜓
8		nfv	⊢ Ⅎ 𝑤 𝑥 = 𝑧
9	8 2	nfim	⊢ Ⅎ 𝑤 ( 𝑥 = 𝑧 → 𝜑 )
10		nfv	⊢ Ⅎ 𝑦 𝑥 = 𝑧
11	10 4	nfim	⊢ Ⅎ 𝑦 ( 𝑥 = 𝑧 → 𝜓 )
12	5	expcom	⊢ ( 𝑦 = 𝑤 → ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) ) )
13	12	pm5.74d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑥 = 𝑧 → 𝜑 ) ↔ ( 𝑥 = 𝑧 → 𝜓 ) ) )
14	9 11 13	cbval	⊢ ( ∀ 𝑦 ( 𝑥 = 𝑧 → 𝜑 ) ↔ ∀ 𝑤 ( 𝑥 = 𝑧 → 𝜓 ) )
15		19.21v	⊢ ( ∀ 𝑦 ( 𝑥 = 𝑧 → 𝜑 ) ↔ ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) )
16		19.21v	⊢ ( ∀ 𝑤 ( 𝑥 = 𝑧 → 𝜓 ) ↔ ( 𝑥 = 𝑧 → ∀ 𝑤 𝜓 ) )
17	14 15 16	3bitr3i	⊢ ( ( 𝑥 = 𝑧 → ∀ 𝑦 𝜑 ) ↔ ( 𝑥 = 𝑧 → ∀ 𝑤 𝜓 ) )
18	17	pm5.74ri	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 𝜑 ↔ ∀ 𝑤 𝜓 ) )
19	6 7 18	cbval	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 ↔ ∀ 𝑧 ∀ 𝑤 𝜓 )