Metamath Proof Explorer

Theorem wl-2spsbbi

Description: spsbbi applied twice. (Contributed by Wolf Lammen, 5-Aug-2023)

Ref Expression
Assertion wl-2spsbbi ⊢ ∀ a ∀ b φ ↔ ψ → y b x a φ ↔ y b x a ψ

Proof

Step Hyp Ref Expression
1 alcom ⊢ ∀ a ∀ b φ ↔ ψ ↔ ∀ b ∀ a φ ↔ ψ
2 nfa1 ⊢ Ⅎ b ∀ b ∀ a φ ↔ ψ
3 nfa1 ⊢ Ⅎ a ∀ a φ ↔ ψ
4 sp ⊢ ∀ a φ ↔ ψ → φ ↔ ψ
5 3 4 sbbid ⊢ ∀ a φ ↔ ψ → x a φ ↔ x a ψ
6 5 sps ⊢ ∀ b ∀ a φ ↔ ψ → x a φ ↔ x a ψ
7 2 6 sbbid ⊢ ∀ b ∀ a φ ↔ ψ → y b x a φ ↔ y b x a ψ
8 1 7 sylbi ⊢ ∀ a ∀ b φ ↔ ψ → y b x a φ ↔ y b x a ψ