Metamath Proof Explorer

Theorem 2sb6

Description: Equivalence for double substitution. (Contributed by NM, 3-Feb-2005)

Ref Expression
Assertion 2sb6 ⊢ z x w y φ ↔ ∀ x ∀ y x = z ∧ y = w → φ

Proof

Step Hyp Ref Expression
1 sb6 ⊢ z x w y φ ↔ ∀ x x = z → w y φ
2 19.21v ⊢ ∀ y x = z → y = w → φ ↔ x = z → ∀ y y = w → φ
3 impexp ⊢ x = z ∧ y = w → φ ↔ x = z → y = w → φ
4 3 albii ⊢ ∀ y x = z ∧ y = w → φ ↔ ∀ y x = z → y = w → φ
5 sb6 ⊢ w y φ ↔ ∀ y y = w → φ
6 5 imbi2i ⊢ x = z → w y φ ↔ x = z → ∀ y y = w → φ
7 2 4 6 3bitr4ri ⊢ x = z → w y φ ↔ ∀ y x = z ∧ y = w → φ
8 7 albii ⊢ ∀ x x = z → w y φ ↔ ∀ x ∀ y x = z ∧ y = w → φ
9 1 8 bitri ⊢ z x w y φ ↔ ∀ x ∀ y x = z ∧ y = w → φ