Metamath Proof Explorer

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 ⊢ Ⅎ z φ
cbval2.2 ⊢ Ⅎ w φ
cbval2.3 ⊢ Ⅎ x ψ
cbval2.4 ⊢ Ⅎ y ψ
cbval2.5 ⊢ x = z ∧ y = w → φ ↔ ψ
Assertion cbval2OLD ⊢ ∀ x ∀ y φ ↔ ∀ z ∀ w ψ

Proof

Step Hyp Ref Expression
1 cbval2.1 ⊢ Ⅎ z φ
2 cbval2.2 ⊢ Ⅎ w φ
3 cbval2.3 ⊢ Ⅎ x ψ
4 cbval2.4 ⊢ Ⅎ y ψ
5 cbval2.5 ⊢ x = z ∧ y = w → φ ↔ ψ
6 1 nfal ⊢ Ⅎ z ∀ y φ
7 3 nfal ⊢ Ⅎ x ∀ w ψ
8 nfv ⊢ Ⅎ w x = z
9 8 2 nfim ⊢ Ⅎ w x = z → φ
10 nfv ⊢ Ⅎ y x = z
11 10 4 nfim ⊢ Ⅎ y x = z → ψ
12 5 expcom ⊢ y = w → x = z → φ ↔ ψ
13 12 pm5.74d ⊢ y = w → x = z → φ ↔ x = z → ψ
14 9 11 13 cbval ⊢ ∀ y x = z → φ ↔ ∀ w x = z → ψ
15 19.21v ⊢ ∀ y x = z → φ ↔ x = z → ∀ y φ
16 19.21v ⊢ ∀ w x = z → ψ ↔ x = z → ∀ w ψ
17 14 15 16 3bitr3i ⊢ x = z → ∀ y φ ↔ x = z → ∀ w ψ
18 17 pm5.74ri ⊢ x = z → ∀ y φ ↔ ∀ w ψ
19 6 7 18 cbval ⊢ ∀ x ∀ y φ ↔ ∀ z ∀ w ψ